Theorem ssfi 4521

Description: A subset of a finite set is finite. Corollary 6G of [Enderton] p. 138.

Assertion

Ref	Expression
ssfi	|- ((E.x e. om A ~~ x /\ B (_ A) -> E.x e. om B ~~ x)

Distinct variable groups:   x,A   x,B

Proof of Theorem ssfi

Step	Hyp	Ref	Expression
1		breng 4363	. . . . 5 |- (x e. om -> (A ~~ x <-> E.z z:A-1-1-onto->x))
2		ssnn 4520	. . . . . . . . . 10 |- ((x e. om /\ (z"B) (_ x) -> E.y e. om (z"B) ~~ y)
3		f1ofo 3686	. . . . . . . . . . 11 |- (z:A-1-1-onto->x -> z:A-onto->x)
4		imassrn 3407	. . . . . . . . . . . 12 |- (z"B) (_ ran z
5		forn 3665	. . . . . . . . . . . . 13 |- (z:A-onto->x -> ran z = x)
6	5	sseq2d 2085	. . . . . . . . . . . 12 |- (z:A-onto->x -> ((z"B) (_ ran z <-> (z"B) (_ x))
7	4, 6	mpbii 193	. . . . . . . . . . 11 |- (z:A-onto->x -> (z"B) (_ x)
8	3, 7	syl 10	. . . . . . . . . 10 |- (z:A-1-1-onto->x -> (z"B) (_ x)
9	2, 8	sylan2 451	. . . . . . . . 9 |- ((x e. om /\ z:A-1-1-onto->x) -> E.y e. om (z"B) ~~ y)
10	9	adantrr 395	. . . . . . . 8 |- ((x e. om /\ (z:A-1-1-onto->x /\ B (_ A)) -> E.y e. om (z"B) ~~ y)
11		entrt 4401	. . . . . . . . . . . . 13 |- ((B ~~ (z"B) /\ (z"B) ~~ y) -> B ~~ y)
12		visset 1809	. . . . . . . . . . . . . . . 16 |- z e. V
13		resexg 3386	. . . . . . . . . . . . . . . 16 |- (z e. V -> (z |` B) e. V)
14	12, 13	ax-mp 7	. . . . . . . . . . . . . . 15 |- (z |` B) e. V
15		f1oeq1 3675	. . . . . . . . . . . . . . 15 |- (x = (z |` B) -> (x:B-1-1-onto->(z"B) <-> (z |` B):B-1-1-onto->(z"B)))
16	14, 15	cla4ev 1865	. . . . . . . . . . . . . 14 |- ((z |` B):B-1-1-onto->(z"B) -> E.x x:B-1-1-onto->(z"B))
17		imaexg 3408	. . . . . . . . . . . . . . . 16 |- (z e. V -> (z"B) e. V)
18	12, 17	ax-mp 7	. . . . . . . . . . . . . . 15 |- (z"B) e. V
19	18	bren 4365	. . . . . . . . . . . . . 14 |- (B ~~ (z"B) <-> E.x x:B-1-1-onto->(z"B))
20	16, 19	sylibr 200	. . . . . . . . . . . . 13 |- ((z |` B):B-1-1-onto->(z"B) -> B ~~ (z"B))
21	11, 20	sylan 448	. . . . . . . . . . . 12 |- (((z |` B):B-1-1-onto->(z"B) /\ (z"B) ~~ y) -> B ~~ y)
22		f1ores 3694	. . . . . . . . . . . . 13 |- ((z:A-1-1->x /\ B (_ A) -> (z |` B):B-1-1-onto->(z"B))
23		f1of1 3679	. . . . . . . . . . . . 13 |- (z:A-1-1-onto->x -> z:A-1-1->x)
24	22, 23	sylan 448	. . . . . . . . . . . 12 |- ((z:A-1-1-onto->x /\ B (_ A) -> (z |` B):B-1-1-onto->(z"B))
25	21, 24	sylan 448	. . . . . . . . . . 11 |- (((z:A-1-1-onto->x /\ B (_ A) /\ (z"B) ~~ y) -> B ~~ y)
26	25	ex 373	. . . . . . . . . 10 |- ((z:A-1-1-onto->x /\ B (_ A) -> ((z"B) ~~ y -> B ~~ y))
27	26	r19.22sdv 1735	. . . . . . . . 9 |- ((z:A-1-1-onto->x /\ B (_ A) -> (E.y e. om (z"B) ~~ y -> E.y e. om B ~~ y))
28	27	adantl 388	. . . . . . . 8 |- ((x e. om /\ (z:A-1-1-onto->x /\ B (_ A)) -> (E.y e. om (z"B) ~~ y -> E.y e. om B ~~ y))
29	10, 28	mpd 26	. . . . . . 7 |- ((x e. om /\ (z:A-1-1-onto->x /\ B (_ A)) -> E.y e. om B ~~ y)
30	29	exp32 377	. . . . . 6 |- (x e. om -> (z:A-1-1-onto->x -> (B (_ A -> E.y e. om B ~~ y)))
31	30	19.23adv 1212	. . . . 5 |- (x e. om -> (E.z z:A-1-1-onto->x -> (B (_ A -> E.y e. om B ~~ y)))
32	1, 31	sylbid 203	. . . 4 |- (x e. om -> (A ~~ x -> (B (_ A -> E.y e. om B ~~ y)))
33	32	r19.23aiv 1740	. . 3 |- (E.x e. om A ~~ x -> (B (_ A -> E.y e. om B ~~ y))
34	33	imp 350	. 2 |- ((E.x e. om A ~~ x /\ B (_ A) -> E.y e. om B ~~ y)
35		breq2 2618	. . 3 |- (y = x -> (B ~~ y <-> B ~~ x))
36	35	cbvrexv 1797	. 2 |- (E.y e. om B ~~ y <-> E.x e. om B ~~ x)
37	34, 36	sylib 198	1 |- ((E.x e. om A ~~ x /\ B (_ A) -> E.x e. om B ~~ x)

Syntax hints:   -> wi 3   /\ wa 223   e. wcel 956  E.wex 978  E.wrex 1643  Vcvv 1807   (_ wss 2043   class class class wbr 2614  omcom 3126  ran crn 3166   |` cres 3167  "cima 3168  -1-1->wf1 3174  -onto->wfo 3175  -1-1-onto->wf1o 3176   ~~ cen 4354

This theorem is referenced by:  domfi 4522  unfi 4534  fctop 7600  cnfilca 10487

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-9 963  ax-10 964  ax-11 965  ax-12 966  ax-13 967  ax-14 968  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457  ax-rep 2688  ax-sep 2698  ax-nul 2705  ax-pow 2737  ax-pr 2774  ax-un 2861

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 775  df-3an 776  df-ex 979  df-sb 1170  df-eu 1380  df-mo 1381  df-clab 1462  df-cleq 1467  df-clel 1470  df-ne 1584  df-ral 1646  df-rex 1647  df-v 1808  df-dif 2045  df-un 2046  df-in 2047  df-ss 2049  df-pss 2051  df-nul 2277  df-if 2358  df-pw 2398  df-sn 2408  df-pr 2409  df-tp 2411  df-op 2412  df-uni 2499  df-br 2615  df-opab 2662  df-tr 2676  df-eprel 2827  df-id 2830  df-po 2835  df-so 2845  df-fr 2912  df-we 2929  df-ord 2946  df-on 2947  df-lim 2948  df-suc 2949  df-om 3127  df-xp 3179  df-rel 3180  df-cnv 3181  df-co 3182  df-dm 3183  df-rn 3184  df-res 3185  df-ima 3186  df-fun 3187  df-fn 3188  df-f 3189  df-f1 3190  df-fo 3191  df-f1o 3192  df-er 4251  df-en 4357

Copyright terms: Public domain