Theorem ssfin 4471

Description: A subset of a finite set is itself finite. Theorem X.1.21 of [Rosser] p. 527. (Contributed by SF, 19-Jan-2015.)

Assertion

Ref	Expression
ssfin	|- ((A e. V /\ B e. Fin /\ A C_ B) -> A e. Fin )

Proof of Theorem ssfin

Dummy variables a b c d k m n x t are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		sseq1 3293	. . . . 5 |- (a = A -> (a C_ B <-> A C_ B))
2		eleq1 2413	. . . . 5 |- (a = A -> (a e. Fin <-> A e. Fin ))
3	1, 2	imbi12d 311	. . . 4 |- (a = A -> ((a C_ B -> a e. Fin ) <-> (A C_ B -> A e. Fin )))
4	3	imbi2d 307	. . 3 |- (a = A -> ((B e. Fin -> (a C_ B -> a e. Fin )) <-> (B e. Fin -> (A C_ B -> A e. Fin ))))
5		sseq2 3294	. . . . 5 |- (b = B -> (a C_ b <-> a C_ B))
6	5	imbi1d 308	. . . 4 |- (b = B -> ((a C_ b -> a e. Fin ) <-> (a C_ B -> a e. Fin )))
7		elfin 4421	. . . . 5 |- (b e. Fin <-> E.n e. Nn b e. n)
8		vex 2863	. . . . . . . . . . . . 13 |- m e. _V
9	8	elcompl 3226	. . . . . . . . . . . 12 |- (m e. ∼ (( Sk i^i (~P1 ( Sk "k ∼ Fin ) X.k _V))"k1c) <-> -. m e. (( Sk i^i (~P1 ( Sk "k ∼ Fin ) X.k _V))"k1c))
10		alcom 1737	. . . . . . . . . . . . 13 |- (A.aA.b((b e. m /\ a C_ b) -> a e. Fin ) <-> A.bA.a((b e. m /\ a C_ b) -> a e. Fin ))
11		impexp 433	. . . . . . . . . . . . . . . 16 |- (((b e. m /\ a C_ b) -> a e. Fin ) <-> (b e. m -> (a C_ b -> a e. Fin )))
12	11	albii 1566	. . . . . . . . . . . . . . 15 |- (A.a((b e. m /\ a C_ b) -> a e. Fin ) <-> A.a(b e. m -> (a C_ b -> a e. Fin )))
13		19.21v 1890	. . . . . . . . . . . . . . 15 |- (A.a(b e. m -> (a C_ b -> a e. Fin )) <-> (b e. m -> A.a(a C_ b -> a e. Fin )))
14	12, 13	bitri 240	. . . . . . . . . . . . . 14 |- (A.a((b e. m /\ a C_ b) -> a e. Fin ) <-> (b e. m -> A.a(a C_ b -> a e. Fin )))
15	14	albii 1566	. . . . . . . . . . . . 13 |- (A.bA.a((b e. m /\ a C_ b) -> a e. Fin ) <-> A.b(b e. m -> A.a(a C_ b -> a e. Fin )))
16	8	elimak 4260	. . . . . . . . . . . . . . 15 |- (m e. (( Sk i^i (~P1 ( Sk "k ∼ Fin ) X.k _V))"k1c) <-> E.t e. 1c <<t, m>> e. ( Sk i^i (~P1 ( Sk "k ∼ Fin ) X.k _V)))
17		df-rex 2621	. . . . . . . . . . . . . . . 16 |- (E.t e. 1c <<t, m>> e. ( Sk i^i (~P1 ( Sk "k ∼ Fin ) X.k _V)) <-> E.t(t e. 1c /\ <<t, m>> e. ( Sk i^i (~P1 ( Sk "k ∼ Fin ) X.k _V))))
18		el1c 4140	. . . . . . . . . . . . . . . . . . . 20 |- (t e. 1c <-> E.b t = {b})
19	18	anbi1i 676	. . . . . . . . . . . . . . . . . . 19 |- ((t e. 1c /\ <<t, m>> e. ( Sk i^i (~P1 ( Sk "k ∼ Fin ) X.k _V))) <-> (E.b t = {b} /\ <<t, m>> e. ( Sk i^i (~P1 ( Sk "k ∼ Fin ) X.k _V))))
20		19.41v 1901	. . . . . . . . . . . . . . . . . . 19 |- (E.b(t = {b} /\ <<t, m>> e. ( Sk i^i (~P1 ( Sk "k ∼ Fin ) X.k _V))) <-> (E.b t = {b} /\ <<t, m>> e. ( Sk i^i (~P1 ( Sk "k ∼ Fin ) X.k _V))))
21	19, 20	bitr4i 243	. . . . . . . . . . . . . . . . . 18 |- ((t e. 1c /\ <<t, m>> e. ( Sk i^i (~P1 ( Sk "k ∼ Fin ) X.k _V))) <-> E.b(t = {b} /\ <<t, m>> e. ( Sk i^i (~P1 ( Sk "k ∼ Fin ) X.k _V))))
22	21	exbii 1582	. . . . . . . . . . . . . . . . 17 |- (E.t(t e. 1c /\ <<t, m>> e. ( Sk i^i (~P1 ( Sk "k ∼ Fin ) X.k _V))) <-> E.tE.b(t = {b} /\ <<t, m>> e. ( Sk i^i (~P1 ( Sk "k ∼ Fin ) X.k _V))))
23		excom 1741	. . . . . . . . . . . . . . . . 17 |- (E.bE.t(t = {b} /\ <<t, m>> e. ( Sk i^i (~P1 ( Sk "k ∼ Fin ) X.k _V))) <-> E.tE.b(t = {b} /\ <<t, m>> e. ( Sk i^i (~P1 ( Sk "k ∼ Fin ) X.k _V))))
24	22, 23	bitr4i 243	. . . . . . . . . . . . . . . 16 |- (E.t(t e. 1c /\ <<t, m>> e. ( Sk i^i (~P1 ( Sk "k ∼ Fin ) X.k _V))) <-> E.bE.t(t = {b} /\ <<t, m>> e. ( Sk i^i (~P1 ( Sk "k ∼ Fin ) X.k _V))))
25		snex 4112	. . . . . . . . . . . . . . . . . . 19 |- {b} e. _V
26		opkeq1 4060	. . . . . . . . . . . . . . . . . . . 20 |- (t = {b} -> <<t, m>> = <<{b}, m>>)
27	26	eleq1d 2419	. . . . . . . . . . . . . . . . . . 19 |- (t = {b} -> (<<t, m>> e. ( Sk i^i (~P1 ( Sk "k ∼ Fin ) X.k _V)) <-> <<{b}, m>> e. ( Sk i^i (~P1 ( Sk "k ∼ Fin ) X.k _V))))
28	25, 27	ceqsexv 2895	. . . . . . . . . . . . . . . . . 18 |- (E.t(t = {b} /\ <<t, m>> e. ( Sk i^i (~P1 ( Sk "k ∼ Fin ) X.k _V))) <-> <<{b}, m>> e. ( Sk i^i (~P1 ( Sk "k ∼ Fin ) X.k _V)))
29		elin 3220	. . . . . . . . . . . . . . . . . 18 |- (<<{b}, m>> e. ( Sk i^i (~P1 ( Sk "k ∼ Fin ) X.k _V)) <-> (<<{b}, m>> e. Sk /\ <<{b}, m>> e. (~P1 ( Sk "k ∼ Fin ) X.k _V)))
30		vex 2863	. . . . . . . . . . . . . . . . . . . 20 |- b e. _V
31	30, 8	elssetk 4271	. . . . . . . . . . . . . . . . . . 19 |- (<<{b}, m>> e. Sk <-> b e. m)
32	25, 8	opkelxpk 4249	. . . . . . . . . . . . . . . . . . . . 21 |- (<<{b}, m>> e. (~P1 ( Sk "k ∼ Fin ) X.k _V) <-> ({b} e. ~P1 ( Sk "k ∼ Fin ) /\ m e. _V))
33	8, 32	mpbiran2 885	. . . . . . . . . . . . . . . . . . . 20 |- (<<{b}, m>> e. (~P1 ( Sk "k ∼ Fin ) X.k _V) <-> {b} e. ~P1 ( Sk "k ∼ Fin ))
34		snelpw1 4147	. . . . . . . . . . . . . . . . . . . 20 |- ({b} e. ~P1 ( Sk "k ∼ Fin ) <-> b e. ( Sk "k ∼ Fin ))
35	30	elimak 4260	. . . . . . . . . . . . . . . . . . . . 21 |- (b e. ( Sk "k ∼ Fin ) <-> E.a e. ∼ Fin <<a, b>> e. Sk )
36		df-rex 2621	. . . . . . . . . . . . . . . . . . . . . 22 |- (E.a e. ∼ Fin <<a, b>> e. Sk <-> E.a(a e. ∼ Fin /\ <<a, b>> e. Sk ))
37		ancom 437	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((a e. ∼ Fin /\ <<a, b>> e. Sk ) <-> (<<a, b>> e. Sk /\ a e. ∼ Fin ))
38		vex 2863	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- a e. _V
39		opkelssetkg 4269	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((a e. _V /\ b e. _V) -> (<<a, b>> e. Sk <-> a C_ b))
40	38, 30, 39	mp2an 653	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (<<a, b>> e. Sk <-> a C_ b)
41	38	elcompl 3226	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (a e. ∼ Fin <-> -. a e. Fin )
42	40, 41	anbi12i 678	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((<<a, b>> e. Sk /\ a e. ∼ Fin ) <-> (a C_ b /\ -. a e. Fin ))
43	37, 42	bitri 240	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((a e. ∼ Fin /\ <<a, b>> e. Sk ) <-> (a C_ b /\ -. a e. Fin ))
44	43	exbii 1582	. . . . . . . . . . . . . . . . . . . . . 22 |- (E.a(a e. ∼ Fin /\ <<a, b>> e. Sk ) <-> E.a(a C_ b /\ -. a e. Fin ))
45	36, 44	bitri 240	. . . . . . . . . . . . . . . . . . . . 21 |- (E.a e. ∼ Fin <<a, b>> e. Sk <-> E.a(a C_ b /\ -. a e. Fin ))
46		exanali 1585	. . . . . . . . . . . . . . . . . . . . 21 |- (E.a(a C_ b /\ -. a e. Fin ) <-> -. A.a(a C_ b -> a e. Fin ))
47	35, 45, 46	3bitri 262	. . . . . . . . . . . . . . . . . . . 20 |- (b e. ( Sk "k ∼ Fin ) <-> -. A.a(a C_ b -> a e. Fin ))
48	33, 34, 47	3bitri 262	. . . . . . . . . . . . . . . . . . 19 |- (<<{b}, m>> e. (~P1 ( Sk "k ∼ Fin ) X.k _V) <-> -. A.a(a C_ b -> a e. Fin ))
49	31, 48	anbi12i 678	. . . . . . . . . . . . . . . . . 18 |- ((<<{b}, m>> e. Sk /\ <<{b}, m>> e. (~P1 ( Sk "k ∼ Fin ) X.k _V)) <-> (b e. m /\ -. A.a(a C_ b -> a e. Fin )))
50	28, 29, 49	3bitri 262	. . . . . . . . . . . . . . . . 17 |- (E.t(t = {b} /\ <<t, m>> e. ( Sk i^i (~P1 ( Sk "k ∼ Fin ) X.k _V))) <-> (b e. m /\ -. A.a(a C_ b -> a e. Fin )))
51	50	exbii 1582	. . . . . . . . . . . . . . . 16 |- (E.bE.t(t = {b} /\ <<t, m>> e. ( Sk i^i (~P1 ( Sk "k ∼ Fin ) X.k _V))) <-> E.b(b e. m /\ -. A.a(a C_ b -> a e. Fin )))
52	17, 24, 51	3bitri 262	. . . . . . . . . . . . . . 15 |- (E.t e. 1c <<t, m>> e. ( Sk i^i (~P1 ( Sk "k ∼ Fin ) X.k _V)) <-> E.b(b e. m /\ -. A.a(a C_ b -> a e. Fin )))
53		exanali 1585	. . . . . . . . . . . . . . 15 |- (E.b(b e. m /\ -. A.a(a C_ b -> a e. Fin )) <-> -. A.b(b e. m -> A.a(a C_ b -> a e. Fin )))
54	16, 52, 53	3bitri 262	. . . . . . . . . . . . . 14 |- (m e. (( Sk i^i (~P1 ( Sk "k ∼ Fin ) X.k _V))"k1c) <-> -. A.b(b e. m -> A.a(a C_ b -> a e. Fin )))
55	54	con2bii 322	. . . . . . . . . . . . 13 |- (A.b(b e. m -> A.a(a C_ b -> a e. Fin )) <-> -. m e. (( Sk i^i (~P1 ( Sk "k ∼ Fin ) X.k _V))"k1c))
56	10, 15, 55	3bitri 262	. . . . . . . . . . . 12 |- (A.aA.b((b e. m /\ a C_ b) -> a e. Fin ) <-> -. m e. (( Sk i^i (~P1 ( Sk "k ∼ Fin ) X.k _V))"k1c))
57	9, 56	bitr4i 243	. . . . . . . . . . 11 |- (m e. ∼ (( Sk i^i (~P1 ( Sk "k ∼ Fin ) X.k _V))"k1c) <-> A.aA.b((b e. m /\ a C_ b) -> a e. Fin ))
58	57	eqabi 2465	. . . . . . . . . 10 |- ∼ (( Sk i^i (~P1 ( Sk "k ∼ Fin ) X.k _V))"k1c) = {m | A.aA.b((b e. m /\ a C_ b) -> a e. Fin )}
59		ssetkex 4295	. . . . . . . . . . . . 13 |- Sk e. _V
60		finex 4398	. . . . . . . . . . . . . . . . 17 |- Fin e. _V
61	60	complex 4105	. . . . . . . . . . . . . . . 16 |- ∼ Fin e. _V
62	59, 61	imakex 4301	. . . . . . . . . . . . . . 15 |- ( Sk "k ∼ Fin ) e. _V
63	62	pw1ex 4304	. . . . . . . . . . . . . 14 |- ~P1 ( Sk "k ∼ Fin ) e. _V
64		vvex 4110	. . . . . . . . . . . . . 14 |- _V e. _V
65	63, 64	xpkex 4290	. . . . . . . . . . . . 13 |- (~P1 ( Sk "k ∼ Fin ) X.k _V) e. _V
66	59, 65	inex 4106	. . . . . . . . . . . 12 |- ( Sk i^i (~P1 ( Sk "k ∼ Fin ) X.k _V)) e. _V
67		1cex 4143	. . . . . . . . . . . 12 |- 1c e. _V
68	66, 67	imakex 4301	. . . . . . . . . . 11 |- (( Sk i^i (~P1 ( Sk "k ∼ Fin ) X.k _V))"k1c) e. _V
69	68	complex 4105	. . . . . . . . . 10 |- ∼ (( Sk i^i (~P1 ( Sk "k ∼ Fin ) X.k _V))"k1c) e. _V
70	58, 69	eqeltrri 2424	. . . . . . . . 9 |- {m | A.aA.b((b e. m /\ a C_ b) -> a e. Fin )} e. _V
71		eleq2 2414	. . . . . . . . . . . . 13 |- (m = 0c -> (b e. m <-> b e. 0c))
72		df-0c 4378	. . . . . . . . . . . . . . 15 |- 0c = {(/)}
73	72	eleq2i 2417	. . . . . . . . . . . . . 14 |- (b e. 0c <-> b e. {(/)})
74	30	elsnc 3757	. . . . . . . . . . . . . 14 |- (b e. {(/)} <-> b = (/))
75	73, 74	bitri 240	. . . . . . . . . . . . 13 |- (b e. 0c <-> b = (/))
76	71, 75	syl6bb 252	. . . . . . . . . . . 12 |- (m = 0c -> (b e. m <-> b = (/)))
77	76	anbi1d 685	. . . . . . . . . . 11 |- (m = 0c -> ((b e. m /\ a C_ b) <-> (b = (/) /\ a C_ b)))
78	77	imbi1d 308	. . . . . . . . . 10 |- (m = 0c -> (((b e. m /\ a C_ b) -> a e. Fin ) <-> ((b = (/) /\ a C_ b) -> a e. Fin )))
79	78	2albidv 1627	. . . . . . . . 9 |- (m = 0c -> (A.aA.b((b e. m /\ a C_ b) -> a e. Fin ) <-> A.aA.b((b = (/) /\ a C_ b) -> a e. Fin )))
80		elequ2 1715	. . . . . . . . . . . . 13 |- (m = k -> (b e. m <-> b e. k))
81	80	anbi1d 685	. . . . . . . . . . . 12 |- (m = k -> ((b e. m /\ a C_ b) <-> (b e. k /\ a C_ b)))
82	81	imbi1d 308	. . . . . . . . . . 11 |- (m = k -> (((b e. m /\ a C_ b) -> a e. Fin ) <-> ((b e. k /\ a C_ b) -> a e. Fin )))
83	82	2albidv 1627	. . . . . . . . . 10 |- (m = k -> (A.aA.b((b e. m /\ a C_ b) -> a e. Fin ) <-> A.aA.b((b e. k /\ a C_ b) -> a e. Fin )))
84		eleq1 2413	. . . . . . . . . . . . . 14 |- (b = d -> (b e. k <-> d e. k))
85	84	adantl 452	. . . . . . . . . . . . 13 |- ((a = c /\ b = d) -> (b e. k <-> d e. k))
86		sseq12 3295	. . . . . . . . . . . . 13 |- ((a = c /\ b = d) -> (a C_ b <-> c C_ d))
87	85, 86	anbi12d 691	. . . . . . . . . . . 12 |- ((a = c /\ b = d) -> ((b e. k /\ a C_ b) <-> (d e. k /\ c C_ d)))
88		eleq1 2413	. . . . . . . . . . . . 13 |- (a = c -> (a e. Fin <-> c e. Fin ))
89	88	adantr 451	. . . . . . . . . . . 12 |- ((a = c /\ b = d) -> (a e. Fin <-> c e. Fin ))
90	87, 89	imbi12d 311	. . . . . . . . . . 11 |- ((a = c /\ b = d) -> (((b e. k /\ a C_ b) -> a e. Fin ) <-> ((d e. k /\ c C_ d) -> c e. Fin )))
91	90	cbval2v 2006	. . . . . . . . . 10 |- (A.aA.b((b e. k /\ a C_ b) -> a e. Fin ) <-> A.cA.d((d e. k /\ c C_ d) -> c e. Fin ))
92	83, 91	syl6bb 252	. . . . . . . . 9 |- (m = k -> (A.aA.b((b e. m /\ a C_ b) -> a e. Fin ) <-> A.cA.d((d e. k /\ c C_ d) -> c e. Fin )))
93		eleq2 2414	. . . . . . . . . . . 12 |- (m = (k +o 1c) -> (b e. m <-> b e. (k +o 1c)))
94	93	anbi1d 685	. . . . . . . . . . 11 |- (m = (k +o 1c) -> ((b e. m /\ a C_ b) <-> (b e. (k +o 1c) /\ a C_ b)))
95	94	imbi1d 308	. . . . . . . . . 10 |- (m = (k +o 1c) -> (((b e. m /\ a C_ b) -> a e. Fin ) <-> ((b e. (k +o 1c) /\ a C_ b) -> a e. Fin )))
96	95	2albidv 1627	. . . . . . . . 9 |- (m = (k +o 1c) -> (A.aA.b((b e. m /\ a C_ b) -> a e. Fin ) <-> A.aA.b((b e. (k +o 1c) /\ a C_ b) -> a e. Fin )))
97		elequ2 1715	. . . . . . . . . . . 12 |- (m = n -> (b e. m <-> b e. n))
98	97	anbi1d 685	. . . . . . . . . . 11 |- (m = n -> ((b e. m /\ a C_ b) <-> (b e. n /\ a C_ b)))
99	98	imbi1d 308	. . . . . . . . . 10 |- (m = n -> (((b e. m /\ a C_ b) -> a e. Fin ) <-> ((b e. n /\ a C_ b) -> a e. Fin )))
100	99	2albidv 1627	. . . . . . . . 9 |- (m = n -> (A.aA.b((b e. m /\ a C_ b) -> a e. Fin ) <-> A.aA.b((b e. n /\ a C_ b) -> a e. Fin )))
101		sseq2 3294	. . . . . . . . . . . . 13 |- (b = (/) -> (a C_ b <-> a C_ (/)))
102	101	biimpa 470	. . . . . . . . . . . 12 |- ((b = (/) /\ a C_ b) -> a C_ (/))
103		ss0b 3581	. . . . . . . . . . . 12 |- (a C_ (/) <-> a = (/))
104	102, 103	sylib 188	. . . . . . . . . . 11 |- ((b = (/) /\ a C_ b) -> a = (/))
105		0fin 4424	. . . . . . . . . . 11 |- (/) e. Fin
106	104, 105	syl6eqel 2441	. . . . . . . . . 10 |- ((b = (/) /\ a C_ b) -> a e. Fin )
107	106	gen2 1547	. . . . . . . . 9 |- A.aA.b((b = (/) /\ a C_ b) -> a e. Fin )
108		sspss 3369	. . . . . . . . . . . . . . 15 |- (a C_ b <-> (a C. b \/ a = b))
109		dfpss4 3889	. . . . . . . . . . . . . . . 16 |- (a C. b <-> (a C_ b /\ E.x e. b -. x e. a))
110	109	orbi1i 506	. . . . . . . . . . . . . . 15 |- ((a C. b \/ a = b) <-> ((a C_ b /\ E.x e. b -. x e. a) \/ a = b))
111	108, 110	bitri 240	. . . . . . . . . . . . . 14 |- (a C_ b <-> ((a C_ b /\ E.x e. b -. x e. a) \/ a = b))
112		simp1 955	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((k e. Nn /\ (x e. b /\ -. x e. a) /\ (a C_ b /\ b e. (k +o 1c))) -> k e. Nn )
113		vex 2863	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- x e. _V
114	113	snid 3761	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- x e. {x}
115		eldif 3222	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (x e. (b \ {x}) <-> (x e. b /\ -. x e. {x}))
116	115	simprbi 450	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (x e. (b \ {x}) -> -. x e. {x})
117	114, 116	mt2 170	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- -. x e. (b \ {x})
118	117	a1i 10	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((k e. Nn /\ (x e. b /\ -. x e. a) /\ (a C_ b /\ b e. (k +o 1c))) -> -. x e. (b \ {x}))
119		undif1 3626	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((b \ {x}) u. {x}) = (b u. {x})
120		snssi 3853	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (x e. b -> {x} C_ b)
121		ssequn2 3437	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ({x} C_ b <-> (b u. {x}) = b)
122	120, 121	sylib 188	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (x e. b -> (b u. {x}) = b)
123	122	adantr 451	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((x e. b /\ -. x e. a) -> (b u. {x}) = b)
124	123	3ad2ant2 977	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((k e. Nn /\ (x e. b /\ -. x e. a) /\ (a C_ b /\ b e. (k +o 1c))) -> (b u. {x}) = b)
125	119, 124	syl5eq 2397	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((k e. Nn /\ (x e. b /\ -. x e. a) /\ (a C_ b /\ b e. (k +o 1c))) -> ((b \ {x}) u. {x}) = b)
126		simp3r 984	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((k e. Nn /\ (x e. b /\ -. x e. a) /\ (a C_ b /\ b e. (k +o 1c))) -> b e. (k +o 1c))
127	125, 126	eqeltrd 2427	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((k e. Nn /\ (x e. b /\ -. x e. a) /\ (a C_ b /\ b e. (k +o 1c))) -> ((b \ {x}) u. {x}) e. (k +o 1c))
128		snex 4112	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- {x} e. _V
129	30, 128	difex 4108	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (b \ {x}) e. _V
130	129, 113	nnsucelr 4429	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((k e. Nn /\ (-. x e. (b \ {x}) /\ ((b \ {x}) u. {x}) e. (k +o 1c))) -> (b \ {x}) e. k)
131	112, 118, 127, 130	syl12anc 1180	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((k e. Nn /\ (x e. b /\ -. x e. a) /\ (a C_ b /\ b e. (k +o 1c))) -> (b \ {x}) e. k)
132		inass 3466	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((a i^i b) i^i ∼ {x}) = (a i^i (b i^i ∼ {x}))
133		df-dif 3216	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((a i^i b) \ {x}) = ((a i^i b) i^i ∼ {x})
134		df-dif 3216	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (b \ {x}) = (b i^i ∼ {x})
135	134	ineq2i 3455	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (a i^i (b \ {x})) = (a i^i (b i^i ∼ {x}))
136	132, 133, 135	3eqtr4ri 2384	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (a i^i (b \ {x})) = ((a i^i b) \ {x})
137		df-ss 3260	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (a C_ b <-> (a i^i b) = a)
138	137	biimpi 186	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (a C_ b -> (a i^i b) = a)
139	138	adantr 451	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((a C_ b /\ b e. (k +o 1c)) -> (a i^i b) = a)
140	139	3ad2ant3 978	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((k e. Nn /\ (x e. b /\ -. x e. a) /\ (a C_ b /\ b e. (k +o 1c))) -> (a i^i b) = a)
141	140	difeq1d 3385	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((k e. Nn /\ (x e. b /\ -. x e. a) /\ (a C_ b /\ b e. (k +o 1c))) -> ((a i^i b) \ {x}) = (a \ {x}))
142		difsn 3846	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (-. x e. a -> (a \ {x}) = a)
143	142	adantl 452	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((x e. b /\ -. x e. a) -> (a \ {x}) = a)
144	143	3ad2ant2 977	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((k e. Nn /\ (x e. b /\ -. x e. a) /\ (a C_ b /\ b e. (k +o 1c))) -> (a \ {x}) = a)
145	141, 144	eqtrd 2385	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((k e. Nn /\ (x e. b /\ -. x e. a) /\ (a C_ b /\ b e. (k +o 1c))) -> ((a i^i b) \ {x}) = a)
146	136, 145	syl5eq 2397	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((k e. Nn /\ (x e. b /\ -. x e. a) /\ (a C_ b /\ b e. (k +o 1c))) -> (a i^i (b \ {x})) = a)
147		df-ss 3260	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (a C_ (b \ {x}) <-> (a i^i (b \ {x})) = a)
148	146, 147	sylibr 203	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((k e. Nn /\ (x e. b /\ -. x e. a) /\ (a C_ b /\ b e. (k +o 1c))) -> a C_ (b \ {x}))
149	131, 148	jca 518	. . . . . . . . . . . . . . . . . . . . . 22 |- ((k e. Nn /\ (x e. b /\ -. x e. a) /\ (a C_ b /\ b e. (k +o 1c))) -> ((b \ {x}) e. k /\ a C_ (b \ {x})))
150	149	3adant1r 1175	. . . . . . . . . . . . . . . . . . . . 21 |- (((k e. Nn /\ A.cA.d((d e. k /\ c C_ d) -> c e. Fin )) /\ (x e. b /\ -. x e. a) /\ (a C_ b /\ b e. (k +o 1c))) -> ((b \ {x}) e. k /\ a C_ (b \ {x})))
151		eleq1 2413	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (d = (b \ {x}) -> (d e. k <-> (b \ {x}) e. k))
152	151	adantl 452	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((c = a /\ d = (b \ {x})) -> (d e. k <-> (b \ {x}) e. k))
153		sseq12 3295	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((c = a /\ d = (b \ {x})) -> (c C_ d <-> a C_ (b \ {x})))
154	152, 153	anbi12d 691	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((c = a /\ d = (b \ {x})) -> ((d e. k /\ c C_ d) <-> ((b \ {x}) e. k /\ a C_ (b \ {x}))))
155		eleq1 2413	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (c = a -> (c e. Fin <-> a e. Fin ))
156	155	adantr 451	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((c = a /\ d = (b \ {x})) -> (c e. Fin <-> a e. Fin ))
157	154, 156	imbi12d 311	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((c = a /\ d = (b \ {x})) -> (((d e. k /\ c C_ d) -> c e. Fin ) <-> (((b \ {x}) e. k /\ a C_ (b \ {x})) -> a e. Fin )))
158	157	spc2gv 2943	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((a e. _V /\ (b \ {x}) e. _V) -> (A.cA.d((d e. k /\ c C_ d) -> c e. Fin ) -> (((b \ {x}) e. k /\ a C_ (b \ {x})) -> a e. Fin )))
159	38, 129, 158	mp2an 653	. . . . . . . . . . . . . . . . . . . . . . 23 |- (A.cA.d((d e. k /\ c C_ d) -> c e. Fin ) -> (((b \ {x}) e. k /\ a C_ (b \ {x})) -> a e. Fin ))
160	159	adantl 452	. . . . . . . . . . . . . . . . . . . . . 22 |- ((k e. Nn /\ A.cA.d((d e. k /\ c C_ d) -> c e. Fin )) -> (((b \ {x}) e. k /\ a C_ (b \ {x})) -> a e. Fin ))
161	160	3ad2ant1 976	. . . . . . . . . . . . . . . . . . . . 21 |- (((k e. Nn /\ A.cA.d((d e. k /\ c C_ d) -> c e. Fin )) /\ (x e. b /\ -. x e. a) /\ (a C_ b /\ b e. (k +o 1c))) -> (((b \ {x}) e. k /\ a C_ (b \ {x})) -> a e. Fin ))
162	150, 161	mpd 14	. . . . . . . . . . . . . . . . . . . 20 |- (((k e. Nn /\ A.cA.d((d e. k /\ c C_ d) -> c e. Fin )) /\ (x e. b /\ -. x e. a) /\ (a C_ b /\ b e. (k +o 1c))) -> a e. Fin )
163	162	3exp 1150	. . . . . . . . . . . . . . . . . . 19 |- ((k e. Nn /\ A.cA.d((d e. k /\ c C_ d) -> c e. Fin )) -> ((x e. b /\ -. x e. a) -> ((a C_ b /\ b e. (k +o 1c)) -> a e. Fin )))
164	163	exp5c 599	. . . . . . . . . . . . . . . . . 18 |- ((k e. Nn /\ A.cA.d((d e. k /\ c C_ d) -> c e. Fin )) -> (x e. b -> (-. x e. a -> (a C_ b -> (b e. (k +o 1c) -> a e. Fin )))))
165	164	rexlimdv 2738	. . . . . . . . . . . . . . . . 17 |- ((k e. Nn /\ A.cA.d((d e. k /\ c C_ d) -> c e. Fin )) -> (E.x e. b -. x e. a -> (a C_ b -> (b e. (k +o 1c) -> a e. Fin ))))
166	165	com23 72	. . . . . . . . . . . . . . . 16 |- ((k e. Nn /\ A.cA.d((d e. k /\ c C_ d) -> c e. Fin )) -> (a C_ b -> (E.x e. b -. x e. a -> (b e. (k +o 1c) -> a e. Fin ))))
167	166	imp3a 420	. . . . . . . . . . . . . . 15 |- ((k e. Nn /\ A.cA.d((d e. k /\ c C_ d) -> c e. Fin )) -> ((a C_ b /\ E.x e. b -. x e. a) -> (b e. (k +o 1c) -> a e. Fin )))
168		peano2 4404	. . . . . . . . . . . . . . . . . 18 |- (k e. Nn -> (k +o 1c) e. Nn )
169		eleq2 2414	. . . . . . . . . . . . . . . . . . . . 21 |- (x = (k +o 1c) -> (b e. x <-> b e. (k +o 1c)))
170	169	rspcev 2956	. . . . . . . . . . . . . . . . . . . 20 |- (((k +o 1c) e. Nn /\ b e. (k +o 1c)) -> E.x e. Nn b e. x)
171		elfin 4421	. . . . . . . . . . . . . . . . . . . 20 |- (b e. Fin <-> E.x e. Nn b e. x)
172	170, 171	sylibr 203	. . . . . . . . . . . . . . . . . . 19 |- (((k +o 1c) e. Nn /\ b e. (k +o 1c)) -> b e. Fin )
173	172	ex 423	. . . . . . . . . . . . . . . . . 18 |- ((k +o 1c) e. Nn -> (b e. (k +o 1c) -> b e. Fin ))
174	168, 173	syl 15	. . . . . . . . . . . . . . . . 17 |- (k e. Nn -> (b e. (k +o 1c) -> b e. Fin ))
175		eleq1 2413	. . . . . . . . . . . . . . . . . 18 |- (a = b -> (a e. Fin <-> b e. Fin ))
176	175	biimprd 214	. . . . . . . . . . . . . . . . 17 |- (a = b -> (b e. Fin -> a e. Fin ))
177	174, 176	syl9 66	. . . . . . . . . . . . . . . 16 |- (k e. Nn -> (a = b -> (b e. (k +o 1c) -> a e. Fin )))
178	177	adantr 451	. . . . . . . . . . . . . . 15 |- ((k e. Nn /\ A.cA.d((d e. k /\ c C_ d) -> c e. Fin )) -> (a = b -> (b e. (k +o 1c) -> a e. Fin )))
179	167, 178	jaod 369	. . . . . . . . . . . . . 14 |- ((k e. Nn /\ A.cA.d((d e. k /\ c C_ d) -> c e. Fin )) -> (((a C_ b /\ E.x e. b -. x e. a) \/ a = b) -> (b e. (k +o 1c) -> a e. Fin )))
180	111, 179	syl5bi 208	. . . . . . . . . . . . 13 |- ((k e. Nn /\ A.cA.d((d e. k /\ c C_ d) -> c e. Fin )) -> (a C_ b -> (b e. (k +o 1c) -> a e. Fin )))
181	180	com23 72	. . . . . . . . . . . 12 |- ((k e. Nn /\ A.cA.d((d e. k /\ c C_ d) -> c e. Fin )) -> (b e. (k +o 1c) -> (a C_ b -> a e. Fin )))
182	181	imp3a 420	. . . . . . . . . . 11 |- ((k e. Nn /\ A.cA.d((d e. k /\ c C_ d) -> c e. Fin )) -> ((b e. (k +o 1c) /\ a C_ b) -> a e. Fin ))
183	182	alrimivv 1632	. . . . . . . . . 10 |- ((k e. Nn /\ A.cA.d((d e. k /\ c C_ d) -> c e. Fin )) -> A.aA.b((b e. (k +o 1c) /\ a C_ b) -> a e. Fin ))
184	183	ex 423	. . . . . . . . 9 |- (k e. Nn -> (A.cA.d((d e. k /\ c C_ d) -> c e. Fin ) -> A.aA.b((b e. (k +o 1c) /\ a C_ b) -> a e. Fin )))
185	70, 79, 92, 96, 100, 107, 184	finds 4412	. . . . . . . 8 |- (n e. Nn -> A.aA.b((b e. n /\ a C_ b) -> a e. Fin ))
186	185	19.21bbi 1865	. . . . . . 7 |- (n e. Nn -> ((b e. n /\ a C_ b) -> a e. Fin ))
187	186	exp3a 425	. . . . . 6 |- (n e. Nn -> (b e. n -> (a C_ b -> a e. Fin )))
188	187	rexlimiv 2733	. . . . 5 |- (E.n e. Nn b e. n -> (a C_ b -> a e. Fin ))
189	7, 188	sylbi 187	. . . 4 |- (b e. Fin -> (a C_ b -> a e. Fin ))
190	6, 189	vtoclga 2921	. . 3 |- (B e. Fin -> (a C_ B -> a e. Fin ))
191	4, 190	vtoclg 2915	. 2 |- (A e. V -> (B e. Fin -> (A C_ B -> A e. Fin )))
192	191	3imp 1145	1 |- ((A e. V /\ B e. Fin /\ A C_ B) -> A e. Fin )

Syntax hints:  -. wn 3   -> wi 4   <-> wb 176   \/ wo 357   /\ wa 358   /\ w3a 934  A.wal 1540  E.wex 1541   = wceq 1642   e. wcel 1710  {cab 2339  E.wrex 2616  _Vcvv 2860   ∼ ccompl 3206   \ cdif 3207   u. cun 3208   i^i cin 3209   C_ wss 3258   C. wpss 3259  (/)c0 3551  {csn 3738  <<copk 4058  1_cc1c 4135  ~P₁ cpw1 4136   X._k cxpk 4175  "_kcimak 4180   S_k cssetk 4184   Nn cnnc 4374  0_cc0c 4375   +o cplc 4376   Fin cfin 4377

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334  ax-nin 4079  ax-xp 4080  ax-cnv 4081  ax-1c 4082  ax-sset 4083  ax-si 4084  ax-ins2 4085  ax-ins3 4086  ax-typlower 4087  ax-sn 4088

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2479  df-ne 2519  df-ral 2620  df-rex 2621  df-v 2862  df-sbc 3048  df-nin 3212  df-compl 3213  df-in 3214  df-un 3215  df-dif 3216  df-symdif 3217  df-ss 3260  df-pss 3262  df-nul 3552  df-if 3664  df-pw 3725  df-sn 3742  df-pr 3743  df-uni 3893  df-int 3928  df-opk 4059  df-1c 4137  df-pw1 4138  df-uni1 4139  df-xpk 4186  df-cnvk 4187  df-ins2k 4188  df-ins3k 4189  df-imak 4190  df-cok 4191  df-p6 4192  df-sik 4193  df-ssetk 4194  df-imagek 4195  df-idk 4196  df-0c 4378  df-addc 4379  df-nnc 4380  df-fin 4381

This theorem is referenced by:  vfinnc  4472  sfinltfin  4536