Theorem isinf 8461

Description: Any set that is not finite is literally infinite, in the sense that it contains subsets of arbitrarily large finite cardinality. (It cannot be proven that the set has countably infinite subsets unless AC is invoked.) The proof does not require the Axiom of Infinity. (Contributed by Mario Carneiro, 15-Jan-2013.)

Assertion

Ref	Expression
isinf	⊢ (¬ 𝐴 ∈ Fin → ∀𝑛 ∈ ω ∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑛))

Distinct variable group:   𝑥,𝐴,𝑛

Proof of Theorem isinf

Dummy variables 𝑓 𝑚 𝑦 𝑧 𝑔 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		breq2 4890	. . . . . 6 ⊢ (𝑛 = ∅ → (𝑥 ≈ 𝑛 ↔ 𝑥 ≈ ∅))
2	1	anbi2d 622	. . . . 5 ⊢ (𝑛 = ∅ → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑛) ↔ (𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ ∅)))
3	2	exbidv 1964	. . . 4 ⊢ (𝑛 = ∅ → (∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑛) ↔ ∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ ∅)))
4		breq2 4890	. . . . . 6 ⊢ (𝑛 = 𝑚 → (𝑥 ≈ 𝑛 ↔ 𝑥 ≈ 𝑚))
5	4	anbi2d 622	. . . . 5 ⊢ (𝑛 = 𝑚 → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑛) ↔ (𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑚)))
6	5	exbidv 1964	. . . 4 ⊢ (𝑛 = 𝑚 → (∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑛) ↔ ∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑚)))
7		sseq1 3845	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑥 ⊆ 𝐴 ↔ 𝑦 ⊆ 𝐴))
8	7	adantl 475	. . . . . 6 ⊢ ((𝑛 = suc 𝑚 ∧ 𝑥 = 𝑦) → (𝑥 ⊆ 𝐴 ↔ 𝑦 ⊆ 𝐴))
9		breq1 4889	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑥 ≈ 𝑛 ↔ 𝑦 ≈ 𝑛))
10		breq2 4890	. . . . . . 7 ⊢ (𝑛 = suc 𝑚 → (𝑦 ≈ 𝑛 ↔ 𝑦 ≈ suc 𝑚))
11	9, 10	sylan9bbr 506	. . . . . 6 ⊢ ((𝑛 = suc 𝑚 ∧ 𝑥 = 𝑦) → (𝑥 ≈ 𝑛 ↔ 𝑦 ≈ suc 𝑚))
12	8, 11	anbi12d 624	. . . . 5 ⊢ ((𝑛 = suc 𝑚 ∧ 𝑥 = 𝑦) → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑛) ↔ (𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚)))
13	12	cbvexdva 2377	. . . 4 ⊢ (𝑛 = suc 𝑚 → (∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑛) ↔ ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚)))
14		0ss 4198	. . . . . 6 ⊢ ∅ ⊆ 𝐴
15		0ex 5026	. . . . . . 7 ⊢ ∅ ∈ V
16	15	enref 8274	. . . . . 6 ⊢ ∅ ≈ ∅
17		sseq1 3845	. . . . . . . 8 ⊢ (𝑥 = ∅ → (𝑥 ⊆ 𝐴 ↔ ∅ ⊆ 𝐴))
18		breq1 4889	. . . . . . . 8 ⊢ (𝑥 = ∅ → (𝑥 ≈ ∅ ↔ ∅ ≈ ∅))
19	17, 18	anbi12d 624	. . . . . . 7 ⊢ (𝑥 = ∅ → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ ∅) ↔ (∅ ⊆ 𝐴 ∧ ∅ ≈ ∅)))
20	15, 19	spcev 3502	. . . . . 6 ⊢ ((∅ ⊆ 𝐴 ∧ ∅ ≈ ∅) → ∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ ∅))
21	14, 16, 20	mp2an 682	. . . . 5 ⊢ ∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ ∅)
22	21	a1i 11	. . . 4 ⊢ (¬ 𝐴 ∈ Fin → ∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ ∅))
23		ssdif0 4172	. . . . . . . . . . . . 13 ⊢ (𝐴 ⊆ 𝑥 ↔ (𝐴 ∖ 𝑥) = ∅)
24		eqss 3836	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝐴 ↔ (𝑥 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝑥))
25		breq1 4889	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝐴 → (𝑥 ≈ 𝑚 ↔ 𝐴 ≈ 𝑚))
26	25	biimpa 470	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 = 𝐴 ∧ 𝑥 ≈ 𝑚) → 𝐴 ≈ 𝑚)
27		rspe 3184	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑚 ∈ ω ∧ 𝐴 ≈ 𝑚) → ∃𝑚 ∈ ω 𝐴 ≈ 𝑚)
28	26, 27	sylan2 586	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑚 ∈ ω ∧ (𝑥 = 𝐴 ∧ 𝑥 ≈ 𝑚)) → ∃𝑚 ∈ ω 𝐴 ≈ 𝑚)
29		isfi 8265	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ Fin ↔ ∃𝑚 ∈ ω 𝐴 ≈ 𝑚)
30	28, 29	sylibr 226	. . . . . . . . . . . . . . . 16 ⊢ ((𝑚 ∈ ω ∧ (𝑥 = 𝐴 ∧ 𝑥 ≈ 𝑚)) → 𝐴 ∈ Fin)
31	30	expcom 404	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 = 𝐴 ∧ 𝑥 ≈ 𝑚) → (𝑚 ∈ ω → 𝐴 ∈ Fin))
32	24, 31	sylanbr 577	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝑥) ∧ 𝑥 ≈ 𝑚) → (𝑚 ∈ ω → 𝐴 ∈ Fin))
33	32	ex 403	. . . . . . . . . . . . 13 ⊢ ((𝑥 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝑥) → (𝑥 ≈ 𝑚 → (𝑚 ∈ ω → 𝐴 ∈ Fin)))
34	23, 33	sylan2br 588	. . . . . . . . . . . 12 ⊢ ((𝑥 ⊆ 𝐴 ∧ (𝐴 ∖ 𝑥) = ∅) → (𝑥 ≈ 𝑚 → (𝑚 ∈ ω → 𝐴 ∈ Fin)))
35	34	expcom 404	. . . . . . . . . . 11 ⊢ ((𝐴 ∖ 𝑥) = ∅ → (𝑥 ⊆ 𝐴 → (𝑥 ≈ 𝑚 → (𝑚 ∈ ω → 𝐴 ∈ Fin))))
36	35	3impd 1410	. . . . . . . . . 10 ⊢ ((𝐴 ∖ 𝑥) = ∅ → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑚 ∧ 𝑚 ∈ ω) → 𝐴 ∈ Fin))
37	36	com12 32	. . . . . . . . 9 ⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑚 ∧ 𝑚 ∈ ω) → ((𝐴 ∖ 𝑥) = ∅ → 𝐴 ∈ Fin))
38	37	con3d 150	. . . . . . . 8 ⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑚 ∧ 𝑚 ∈ ω) → (¬ 𝐴 ∈ Fin → ¬ (𝐴 ∖ 𝑥) = ∅))
39		bren 8250	. . . . . . . . . 10 ⊢ (𝑥 ≈ 𝑚 ↔ ∃𝑓 𝑓:𝑥–1-1-onto→𝑚)
40		neq0 4158	. . . . . . . . . . . . . 14 ⊢ (¬ (𝐴 ∖ 𝑥) = ∅ ↔ ∃𝑧 𝑧 ∈ (𝐴 ∖ 𝑥))
41		eldifi 3955	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 ∈ (𝐴 ∖ 𝑥) → 𝑧 ∈ 𝐴)
42	41	snssd 4571	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ (𝐴 ∖ 𝑥) → {𝑧} ⊆ 𝐴)
43		unss 4010	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ⊆ 𝐴 ∧ {𝑧} ⊆ 𝐴) ↔ (𝑥 ∪ {𝑧}) ⊆ 𝐴)
44	43	biimpi 208	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ⊆ 𝐴 ∧ {𝑧} ⊆ 𝐴) → (𝑥 ∪ {𝑧}) ⊆ 𝐴)
45	42, 44	sylan2 586	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑥)) → (𝑥 ∪ {𝑧}) ⊆ 𝐴)
46	45	ad2ant2r 737	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑥 ⊆ 𝐴 ∧ 𝑓:𝑥–1-1-onto→𝑚) ∧ (𝑧 ∈ (𝐴 ∖ 𝑥) ∧ 𝑚 ∈ ω)) → (𝑥 ∪ {𝑧}) ⊆ 𝐴)
47		vex 3401	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑧 ∈ V
48		vex 3401	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑚 ∈ V
49	47, 48	f1osn 6430	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ {⟨𝑧, 𝑚⟩}:{𝑧}–1-1-onto→{𝑚}
50	49	jctr 520	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓:𝑥–1-1-onto→𝑚 → (𝑓:𝑥–1-1-onto→𝑚 ∧ {⟨𝑧, 𝑚⟩}:{𝑧}–1-1-onto→{𝑚}))
51		eldifn 3956	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧 ∈ (𝐴 ∖ 𝑥) → ¬ 𝑧 ∈ 𝑥)
52		disjsn 4478	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑥 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ 𝑥)
53	51, 52	sylibr 226	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 ∈ (𝐴 ∖ 𝑥) → (𝑥 ∩ {𝑧}) = ∅)
54		nnord 7351	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑚 ∈ ω → Ord 𝑚)
55		orddisj 6014	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (Ord 𝑚 → (𝑚 ∩ {𝑚}) = ∅)
56	54, 55	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑚 ∈ ω → (𝑚 ∩ {𝑚}) = ∅)
57	53, 56	anim12i 606	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑧 ∈ (𝐴 ∖ 𝑥) ∧ 𝑚 ∈ ω) → ((𝑥 ∩ {𝑧}) = ∅ ∧ (𝑚 ∩ {𝑚}) = ∅))
58		f1oun 6410	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑓:𝑥–1-1-onto→𝑚 ∧ {⟨𝑧, 𝑚⟩}:{𝑧}–1-1-onto→{𝑚}) ∧ ((𝑥 ∩ {𝑧}) = ∅ ∧ (𝑚 ∩ {𝑚}) = ∅)) → (𝑓 ∪ {⟨𝑧, 𝑚⟩}):(𝑥 ∪ {𝑧})–1-1-onto→(𝑚 ∪ {𝑚}))
59	50, 57, 58	syl2an 589	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑓:𝑥–1-1-onto→𝑚 ∧ (𝑧 ∈ (𝐴 ∖ 𝑥) ∧ 𝑚 ∈ ω)) → (𝑓 ∪ {⟨𝑧, 𝑚⟩}):(𝑥 ∪ {𝑧})–1-1-onto→(𝑚 ∪ {𝑚}))
60		df-suc 5982	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ suc 𝑚 = (𝑚 ∪ {𝑚})
61		f1oeq3 6382	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (suc 𝑚 = (𝑚 ∪ {𝑚}) → ((𝑓 ∪ {⟨𝑧, 𝑚⟩}):(𝑥 ∪ {𝑧})–1-1-onto→suc 𝑚 ↔ (𝑓 ∪ {⟨𝑧, 𝑚⟩}):(𝑥 ∪ {𝑧})–1-1-onto→(𝑚 ∪ {𝑚})))
62	60, 61	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑓 ∪ {⟨𝑧, 𝑚⟩}):(𝑥 ∪ {𝑧})–1-1-onto→suc 𝑚 ↔ (𝑓 ∪ {⟨𝑧, 𝑚⟩}):(𝑥 ∪ {𝑧})–1-1-onto→(𝑚 ∪ {𝑚}))
63		vex 3401	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 𝑓 ∈ V
64		snex 5140	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ {⟨𝑧, 𝑚⟩} ∈ V
65	63, 64	unex 7233	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓 ∪ {⟨𝑧, 𝑚⟩}) ∈ V
66		f1oeq1 6380	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑔 = (𝑓 ∪ {⟨𝑧, 𝑚⟩}) → (𝑔:(𝑥 ∪ {𝑧})–1-1-onto→suc 𝑚 ↔ (𝑓 ∪ {⟨𝑧, 𝑚⟩}):(𝑥 ∪ {𝑧})–1-1-onto→suc 𝑚))
67	65, 66	spcev 3502	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑓 ∪ {⟨𝑧, 𝑚⟩}):(𝑥 ∪ {𝑧})–1-1-onto→suc 𝑚 → ∃𝑔 𝑔:(𝑥 ∪ {𝑧})–1-1-onto→suc 𝑚)
68		bren 8250	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 ∪ {𝑧}) ≈ suc 𝑚 ↔ ∃𝑔 𝑔:(𝑥 ∪ {𝑧})–1-1-onto→suc 𝑚)
69	67, 68	sylibr 226	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑓 ∪ {⟨𝑧, 𝑚⟩}):(𝑥 ∪ {𝑧})–1-1-onto→suc 𝑚 → (𝑥 ∪ {𝑧}) ≈ suc 𝑚)
70	62, 69	sylbir 227	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑓 ∪ {⟨𝑧, 𝑚⟩}):(𝑥 ∪ {𝑧})–1-1-onto→(𝑚 ∪ {𝑚}) → (𝑥 ∪ {𝑧}) ≈ suc 𝑚)
71	59, 70	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓:𝑥–1-1-onto→𝑚 ∧ (𝑧 ∈ (𝐴 ∖ 𝑥) ∧ 𝑚 ∈ ω)) → (𝑥 ∪ {𝑧}) ≈ suc 𝑚)
72	71	adantll 704	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑥 ⊆ 𝐴 ∧ 𝑓:𝑥–1-1-onto→𝑚) ∧ (𝑧 ∈ (𝐴 ∖ 𝑥) ∧ 𝑚 ∈ ω)) → (𝑥 ∪ {𝑧}) ≈ suc 𝑚)
73		vex 3401	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑥 ∈ V
74		snex 5140	. . . . . . . . . . . . . . . . . . . 20 ⊢ {𝑧} ∈ V
75	73, 74	unex 7233	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∪ {𝑧}) ∈ V
76		sseq1 3845	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = (𝑥 ∪ {𝑧}) → (𝑦 ⊆ 𝐴 ↔ (𝑥 ∪ {𝑧}) ⊆ 𝐴))
77		breq1 4889	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = (𝑥 ∪ {𝑧}) → (𝑦 ≈ suc 𝑚 ↔ (𝑥 ∪ {𝑧}) ≈ suc 𝑚))
78	76, 77	anbi12d 624	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = (𝑥 ∪ {𝑧}) → ((𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚) ↔ ((𝑥 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝑥 ∪ {𝑧}) ≈ suc 𝑚)))
79	75, 78	spcev 3502	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑥 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝑥 ∪ {𝑧}) ≈ suc 𝑚) → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚))
80	46, 72, 79	syl2anc 579	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑥 ⊆ 𝐴 ∧ 𝑓:𝑥–1-1-onto→𝑚) ∧ (𝑧 ∈ (𝐴 ∖ 𝑥) ∧ 𝑚 ∈ ω)) → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚))
81	80	expcom 404	. . . . . . . . . . . . . . . 16 ⊢ ((𝑧 ∈ (𝐴 ∖ 𝑥) ∧ 𝑚 ∈ ω) → ((𝑥 ⊆ 𝐴 ∧ 𝑓:𝑥–1-1-onto→𝑚) → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚)))
82	81	ex 403	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ (𝐴 ∖ 𝑥) → (𝑚 ∈ ω → ((𝑥 ⊆ 𝐴 ∧ 𝑓:𝑥–1-1-onto→𝑚) → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚))))
83	82	exlimiv 1973	. . . . . . . . . . . . . 14 ⊢ (∃𝑧 𝑧 ∈ (𝐴 ∖ 𝑥) → (𝑚 ∈ ω → ((𝑥 ⊆ 𝐴 ∧ 𝑓:𝑥–1-1-onto→𝑚) → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚))))
84	40, 83	sylbi 209	. . . . . . . . . . . . 13 ⊢ (¬ (𝐴 ∖ 𝑥) = ∅ → (𝑚 ∈ ω → ((𝑥 ⊆ 𝐴 ∧ 𝑓:𝑥–1-1-onto→𝑚) → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚))))
85	84	com13 88	. . . . . . . . . . . 12 ⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑓:𝑥–1-1-onto→𝑚) → (𝑚 ∈ ω → (¬ (𝐴 ∖ 𝑥) = ∅ → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚))))
86	85	expcom 404	. . . . . . . . . . 11 ⊢ (𝑓:𝑥–1-1-onto→𝑚 → (𝑥 ⊆ 𝐴 → (𝑚 ∈ ω → (¬ (𝐴 ∖ 𝑥) = ∅ → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚)))))
87	86	exlimiv 1973	. . . . . . . . . 10 ⊢ (∃𝑓 𝑓:𝑥–1-1-onto→𝑚 → (𝑥 ⊆ 𝐴 → (𝑚 ∈ ω → (¬ (𝐴 ∖ 𝑥) = ∅ → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚)))))
88	39, 87	sylbi 209	. . . . . . . . 9 ⊢ (𝑥 ≈ 𝑚 → (𝑥 ⊆ 𝐴 → (𝑚 ∈ ω → (¬ (𝐴 ∖ 𝑥) = ∅ → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚)))))
89	88	3imp21 1102	. . . . . . . 8 ⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑚 ∧ 𝑚 ∈ ω) → (¬ (𝐴 ∖ 𝑥) = ∅ → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚)))
90	38, 89	syld 47	. . . . . . 7 ⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑚 ∧ 𝑚 ∈ ω) → (¬ 𝐴 ∈ Fin → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚)))
91	90	3expia 1111	. . . . . 6 ⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑚) → (𝑚 ∈ ω → (¬ 𝐴 ∈ Fin → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚))))
92	91	exlimiv 1973	. . . . 5 ⊢ (∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑚) → (𝑚 ∈ ω → (¬ 𝐴 ∈ Fin → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚))))
93	92	com3l 89	. . . 4 ⊢ (𝑚 ∈ ω → (¬ 𝐴 ∈ Fin → (∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑚) → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚))))
94	3, 6, 13, 22, 93	finds2 7372	. . 3 ⊢ (𝑛 ∈ ω → (¬ 𝐴 ∈ Fin → ∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑛)))
95	94	com12 32	. 2 ⊢ (¬ 𝐴 ∈ Fin → (𝑛 ∈ ω → ∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑛)))
96	95	ralrimiv 3147	1 ⊢ (¬ 𝐴 ∈ Fin → ∀𝑛 ∈ ω ∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑛))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 198   ∧ wa 386   ∧ w3a 1071   = wceq 1601  ∃wex 1823   ∈ wcel 2107  ∀wral 3090  ∃wrex 3091   ∖ cdif 3789   ∪ cun 3790   ∩ cin 3791   ⊆ wss 3792  ∅c0 4141  {csn 4398  ⟨cop 4404   class class class wbr 4886  Ord word 5975  suc csuc 5978  –1-1-onto→wf1o 6134  ωcom 7343   ≈ cen 8238  Fincfn 8241

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-sep 5017  ax-nul 5025  ax-pow 5077  ax-pr 5138  ax-un 7226

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-ral 3095  df-rex 3096  df-rab 3099  df-v 3400  df-sbc 3653  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-pss 3808  df-nul 4142  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-tp 4403  df-op 4405  df-uni 4672  df-br 4887  df-opab 4949  df-tr 4988  df-id 5261  df-eprel 5266  df-po 5274  df-so 5275  df-fr 5314  df-we 5316  df-xp 5361  df-rel 5362  df-cnv 5363  df-co 5364  df-dm 5365  df-rn 5366  df-res 5367  df-ima 5368  df-ord 5979  df-on 5980  df-lim 5981  df-suc 5982  df-fun 6137  df-fn 6138  df-f 6139  df-f1 6140  df-fo 6141  df-f1o 6142  df-om 7344  df-en 8242  df-fin 8245

This theorem is referenced by:  fineqvlem  8462  isinffi  9151  domtriomlem  9599  ishashinf  13561