Theorem ssfi 3430

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 group(s):   x,A   x,B

Proof of Theorem ssfi

Step	Hyp	Ref	Expression
1		breng 3280	. . . . 5 |- (x e. om -> (A ~~ x <-> E.z z:A-1-1-onto->x))
2		ssnn 3429	. . . . . . . . . 10 |- ((x e. om /\ (z"B) (_ x) -> E.y e. om (z"B) ~~ y)
3		df-f1o 2437	. . . . . . . . . . . 12 |- (z:A-1-1-onto->x <-> (z:A-1-1->x /\ z:A-onto->x))
4	3	pm3.27bd 263	. . . . . . . . . . 11 |- (z:A-1-1-onto->x -> z:A-onto->x)
5		imassrn 2611	. . . . . . . . . . . 12 |- (z"B) (_ ran z
6		forn 2789	. . . . . . . . . . . . 13 |- (z:A-onto->x -> ran z = x)
7	6	sseq2d 1528	. . . . . . . . . . . 12 |- (z:A-onto->x -> ((z"B) (_ ran z <-> (z"B) (_ x))
8	5, 7	mpbii 168	. . . . . . . . . . 11 |- (z:A-onto->x -> (z"B) (_ x)
9	4, 8	syl 12	. . . . . . . . . 10 |- (z:A-1-1-onto->x -> (z"B) (_ x)
10	2, 9	sylan2 346	. . . . . . . . 9 |- ((x e. om /\ z:A-1-1-onto->x) -> E.y e. om (z"B) ~~ y)
11	10	adantrr 312	. . . . . . . 8 |- ((x e. om /\ (z:A-1-1-onto->x /\ B (_ A)) -> E.y e. om (z"B) ~~ y)
12		entrt 3319	. . . . . . . . . . . . 13 |- ((B ~~ (z"B) /\ (z"B) ~~ y) -> B ~~ y)
13		visset 1350	. . . . . . . . . . . . . . . 16 |- z e. V
14		resexg 2597	. . . . . . . . . . . . . . . 16 |- (z e. V -> (z |` B) e. V)
15	13, 14	ax-mp 6	. . . . . . . . . . . . . . 15 |- (z |` B) e. V
16		f1oeq1 2795	. . . . . . . . . . . . . . 15 |- (x = (z |` B) -> (x:B-1-1-onto->(z"B) <-> (z |` B):B-1-1-onto->(z"B)))
17	15, 16	cla4ev 1401	. . . . . . . . . . . . . 14 |- ((z |` B):B-1-1-onto->(z"B) -> E.x x:B-1-1-onto->(z"B))
18		imaexg 2612	. . . . . . . . . . . . . . . 16 |- (z e. V -> (z"B) e. V)
19	13, 18	ax-mp 6	. . . . . . . . . . . . . . 15 |- (z"B) e. V
20	19	bren 3282	. . . . . . . . . . . . . 14 |- (B ~~ (z"B) <-> E.x x:B-1-1-onto->(z"B))
21	17, 20	sylibr 175	. . . . . . . . . . . . 13 |- ((z |` B):B-1-1-onto->(z"B) -> B ~~ (z"B))
22	12, 21	sylan 343	. . . . . . . . . . . 12 |- (((z |` B):B-1-1-onto->(z"B) /\ (z"B) ~~ y) -> B ~~ y)
23		f1ores 2813	. . . . . . . . . . . . 13 |- ((z:A-1-1->x /\ B (_ A) -> (z |` B):B-1-1-onto->(z"B))
24		f1of1 2799	. . . . . . . . . . . . 13 |- (z:A-1-1-onto->x -> z:A-1-1->x)
25	23, 24	sylan 343	. . . . . . . . . . . 12 |- ((z:A-1-1-onto->x /\ B (_ A) -> (z |` B):B-1-1-onto->(z"B))
26	22, 25	sylan 343	. . . . . . . . . . 11 |- (((z:A-1-1-onto->x /\ B (_ A) /\ (z"B) ~~ y) -> B ~~ y)
27	26	exp 291	. . . . . . . . . 10 |- ((z:A-1-1-onto->x /\ B (_ A) -> ((z"B) ~~ y -> B ~~ y))
28	27	r19.22sdv 1279	. . . . . . . . 9 |- ((z:A-1-1-onto->x /\ B (_ A) -> (E.y e. om (z"B) ~~ y -> E.y e. om B ~~ y))
29	28	adantl 305	. . . . . . . 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))
30	11, 29	mpd 46	. . . . . . 7 |- ((x e. om /\ (z:A-1-1-onto->x /\ B (_ A)) -> E.y e. om B ~~ y)
31	30	exp32 294	. . . . . 6 |- (x e. om -> (z:A-1-1-onto->x -> (B (_ A -> E.y e. om B ~~ y)))
32	31	19.23adv 954	. . . . 5 |- (x e. om -> (E.z z:A-1-1-onto->x -> (B (_ A -> E.y e. om B ~~ y)))
33	1, 32	sylbid 178	. . . 4 |- (x e. om -> (A ~~ x -> (B (_ A -> E.y e. om B ~~ y)))
34	33	r19.23aiv 1284	. . 3 |- (E.x e. om A ~~ x -> (B (_ A -> E.y e. om B ~~ y))
35	34	imp 277	. 2 |- ((E.x e. om A ~~ x /\ B (_ A) -> E.y e. om B ~~ y)
36		breq2 2066	. . 3 |- (y = x -> (B ~~ y <-> B ~~ x))
37	36	cbvrexv 1334	. 2 |- (E.y e. om B ~~ y <-> E.x e. om B ~~ x)
38	35, 37	sylib 173	1 |- ((E.x e. om A ~~ x /\ B (_ A) -> E.x e. om B ~~ x)

Syntax hints:   -> wi 2   /\ wa 196  E.wex 678   e. wcel 1092  E.wrex 1202  Vcvv 1348   (_ wss 1487   class class class wbr 2054  omcom 2372  ran crn 2411   |` cres 2412  "cima 2413  -1-1->wf1 2419  -onto->wfo 2420  -1-1-onto->wf1o 2421   ~~ cen 3271

This theorem is referenced by:  unfi 3441

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-13 804  ax-14 805  ax-16 922  ax-17 925  ax-ext 1074  ax-rep 1075  ax-un 1076  ax-pow 1077

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-3or 582  df-3an 583  df-ex 679  df-sb 853  df-eu 1009  df-mo 1010  df-clab 1093  df-cleq 1097  df-clel 1099  df-ne 1192  df-ral 1205  df-rex 1206  df-v 1349  df-dif 1489  df-un 1490  df-in 1491  df-ss 1492  df-pss 1494  df-nul 1708  df-if 1777  df-pw 1799  df-sn 1811  df-pr 1812  df-tp 1814  df-op 1815  df-uni 1920  df-tr 2042  df-br 2063  df-opab 2098  df-eprel 2122  df-id 2125  df-po 2128  df-so 2138  df-fr 2169  df-we 2186  df-ord 2202  df-on 2203  df-lim 2204  df-suc 2205  df-om 2373  df-xp 2424  df-rel 2425  df-cnv 2426  df-co 2427  df-dm 2428  df-rn 2429  df-res 2430  df-ima 2431  df-fun 2432  df-fn 2433  df-f 2434  df-f1 2435  df-fo 2436  df-f1o 2437  df-er 3200  df-en 3274

metamath.org