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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 176   ∨ wo 357   ∧ wa 358   ∧ w3a 934  ∀wal 1540  ∃wex 1541   = wceq 1642   ∈ wcel 1710  {cab 2339  ∃wrex 2616  Vcvv 2860   ∼ ccompl 3206   ∖ cdif 3207   ∪ cun 3208   ∩ cin 3209   ⊆ wss 3258   ⊊ wpss 3259  ∅c0 3551  {csn 3738  ⟪copk 4058  1_cc1c 4135  ℘₁cpw1 4136   ×_k cxpk 4175   “_k cimak 4180   S_k cssetk 4184   Nn cnnc 4374  0_cc0c 4375   +_c 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