Theorem isinf 8715

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 5034	. . . . . 6 ⊢ (𝑛 = ∅ → (𝑥 ≈ 𝑛 ↔ 𝑥 ≈ ∅))
2	1	anbi2d 631	. . . . 5 ⊢ (𝑛 = ∅ → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑛) ↔ (𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ ∅)))
3	2	exbidv 1922	. . . 4 ⊢ (𝑛 = ∅ → (∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑛) ↔ ∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ ∅)))
4		breq2 5034	. . . . . 6 ⊢ (𝑛 = 𝑚 → (𝑥 ≈ 𝑛 ↔ 𝑥 ≈ 𝑚))
5	4	anbi2d 631	. . . . 5 ⊢ (𝑛 = 𝑚 → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑛) ↔ (𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑚)))
6	5	exbidv 1922	. . . 4 ⊢ (𝑛 = 𝑚 → (∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑛) ↔ ∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑚)))
7		sseq1 3940	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑥 ⊆ 𝐴 ↔ 𝑦 ⊆ 𝐴))
8	7	adantl 485	. . . . . 6 ⊢ ((𝑛 = suc 𝑚 ∧ 𝑥 = 𝑦) → (𝑥 ⊆ 𝐴 ↔ 𝑦 ⊆ 𝐴))
9		breq1 5033	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑥 ≈ 𝑛 ↔ 𝑦 ≈ 𝑛))
10		breq2 5034	. . . . . . 7 ⊢ (𝑛 = suc 𝑚 → (𝑦 ≈ 𝑛 ↔ 𝑦 ≈ suc 𝑚))
11	9, 10	sylan9bbr 514	. . . . . 6 ⊢ ((𝑛 = suc 𝑚 ∧ 𝑥 = 𝑦) → (𝑥 ≈ 𝑛 ↔ 𝑦 ≈ suc 𝑚))
12	8, 11	anbi12d 633	. . . . 5 ⊢ ((𝑛 = suc 𝑚 ∧ 𝑥 = 𝑦) → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑛) ↔ (𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚)))
13	12	cbvexdvaw 2046	. . . 4 ⊢ (𝑛 = suc 𝑚 → (∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑛) ↔ ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚)))
14		0ss 4304	. . . . . 6 ⊢ ∅ ⊆ 𝐴
15		0ex 5175	. . . . . . 7 ⊢ ∅ ∈ V
16	15	enref 8525	. . . . . 6 ⊢ ∅ ≈ ∅
17		sseq1 3940	. . . . . . . 8 ⊢ (𝑥 = ∅ → (𝑥 ⊆ 𝐴 ↔ ∅ ⊆ 𝐴))
18		breq1 5033	. . . . . . . 8 ⊢ (𝑥 = ∅ → (𝑥 ≈ ∅ ↔ ∅ ≈ ∅))
19	17, 18	anbi12d 633	. . . . . . 7 ⊢ (𝑥 = ∅ → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ ∅) ↔ (∅ ⊆ 𝐴 ∧ ∅ ≈ ∅)))
20	15, 19	spcev 3555	. . . . . 6 ⊢ ((∅ ⊆ 𝐴 ∧ ∅ ≈ ∅) → ∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ ∅))
21	14, 16, 20	mp2an 691	. . . . 5 ⊢ ∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ ∅)
22	21	a1i 11	. . . 4 ⊢ (¬ 𝐴 ∈ Fin → ∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ ∅))
23		ssdif0 4277	. . . . . . . . . . . . 13 ⊢ (𝐴 ⊆ 𝑥 ↔ (𝐴 ∖ 𝑥) = ∅)
24		eqss 3930	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝐴 ↔ (𝑥 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝑥))
25		breq1 5033	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝐴 → (𝑥 ≈ 𝑚 ↔ 𝐴 ≈ 𝑚))
26	25	biimpa 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 = 𝐴 ∧ 𝑥 ≈ 𝑚) → 𝐴 ≈ 𝑚)
27		rspe 3263	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑚 ∈ ω ∧ 𝐴 ≈ 𝑚) → ∃𝑚 ∈ ω 𝐴 ≈ 𝑚)
28	26, 27	sylan2 595	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑚 ∈ ω ∧ (𝑥 = 𝐴 ∧ 𝑥 ≈ 𝑚)) → ∃𝑚 ∈ ω 𝐴 ≈ 𝑚)
29		isfi 8516	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ Fin ↔ ∃𝑚 ∈ ω 𝐴 ≈ 𝑚)
30	28, 29	sylibr 237	. . . . . . . . . . . . . . . 16 ⊢ ((𝑚 ∈ ω ∧ (𝑥 = 𝐴 ∧ 𝑥 ≈ 𝑚)) → 𝐴 ∈ Fin)
31	30	expcom 417	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 = 𝐴 ∧ 𝑥 ≈ 𝑚) → (𝑚 ∈ ω → 𝐴 ∈ Fin))
32	24, 31	sylanbr 585	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝑥) ∧ 𝑥 ≈ 𝑚) → (𝑚 ∈ ω → 𝐴 ∈ Fin))
33	32	ex 416	. . . . . . . . . . . . 13 ⊢ ((𝑥 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝑥) → (𝑥 ≈ 𝑚 → (𝑚 ∈ ω → 𝐴 ∈ Fin)))
34	23, 33	sylan2br 597	. . . . . . . . . . . 12 ⊢ ((𝑥 ⊆ 𝐴 ∧ (𝐴 ∖ 𝑥) = ∅) → (𝑥 ≈ 𝑚 → (𝑚 ∈ ω → 𝐴 ∈ Fin)))
35	34	expcom 417	. . . . . . . . . . 11 ⊢ ((𝐴 ∖ 𝑥) = ∅ → (𝑥 ⊆ 𝐴 → (𝑥 ≈ 𝑚 → (𝑚 ∈ ω → 𝐴 ∈ Fin))))
36	35	3impd 1345	. . . . . . . . . 10 ⊢ ((𝐴 ∖ 𝑥) = ∅ → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑚 ∧ 𝑚 ∈ ω) → 𝐴 ∈ Fin))
37	36	com12 32	. . . . . . . . 9 ⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑚 ∧ 𝑚 ∈ ω) → ((𝐴 ∖ 𝑥) = ∅ → 𝐴 ∈ Fin))
38	37	con3d 155	. . . . . . . 8 ⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑚 ∧ 𝑚 ∈ ω) → (¬ 𝐴 ∈ Fin → ¬ (𝐴 ∖ 𝑥) = ∅))
39		bren 8501	. . . . . . . . . 10 ⊢ (𝑥 ≈ 𝑚 ↔ ∃𝑓 𝑓:𝑥–1-1-onto→𝑚)
40		neq0 4259	. . . . . . . . . . . . . 14 ⊢ (¬ (𝐴 ∖ 𝑥) = ∅ ↔ ∃𝑧 𝑧 ∈ (𝐴 ∖ 𝑥))
41		eldifi 4054	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 ∈ (𝐴 ∖ 𝑥) → 𝑧 ∈ 𝐴)
42	41	snssd 4702	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ (𝐴 ∖ 𝑥) → {𝑧} ⊆ 𝐴)
43		unss 4111	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ⊆ 𝐴 ∧ {𝑧} ⊆ 𝐴) ↔ (𝑥 ∪ {𝑧}) ⊆ 𝐴)
44	43	biimpi 219	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ⊆ 𝐴 ∧ {𝑧} ⊆ 𝐴) → (𝑥 ∪ {𝑧}) ⊆ 𝐴)
45	42, 44	sylan2 595	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑥)) → (𝑥 ∪ {𝑧}) ⊆ 𝐴)
46	45	ad2ant2r 746	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑥 ⊆ 𝐴 ∧ 𝑓:𝑥–1-1-onto→𝑚) ∧ (𝑧 ∈ (𝐴 ∖ 𝑥) ∧ 𝑚 ∈ ω)) → (𝑥 ∪ {𝑧}) ⊆ 𝐴)
47		vex 3444	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑧 ∈ V
48		vex 3444	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑚 ∈ V
49	47, 48	f1osn 6629	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ {⟨𝑧, 𝑚⟩}:{𝑧}–1-1-onto→{𝑚}
50	49	jctr 528	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓:𝑥–1-1-onto→𝑚 → (𝑓:𝑥–1-1-onto→𝑚 ∧ {⟨𝑧, 𝑚⟩}:{𝑧}–1-1-onto→{𝑚}))
51		eldifn 4055	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧 ∈ (𝐴 ∖ 𝑥) → ¬ 𝑧 ∈ 𝑥)
52		disjsn 4607	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑥 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ 𝑥)
53	51, 52	sylibr 237	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 ∈ (𝐴 ∖ 𝑥) → (𝑥 ∩ {𝑧}) = ∅)
54		nnord 7568	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑚 ∈ ω → Ord 𝑚)
55		orddisj 6197	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (Ord 𝑚 → (𝑚 ∩ {𝑚}) = ∅)
56	54, 55	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑚 ∈ ω → (𝑚 ∩ {𝑚}) = ∅)
57	53, 56	anim12i 615	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑧 ∈ (𝐴 ∖ 𝑥) ∧ 𝑚 ∈ ω) → ((𝑥 ∩ {𝑧}) = ∅ ∧ (𝑚 ∩ {𝑚}) = ∅))
58		f1oun 6609	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑓:𝑥–1-1-onto→𝑚 ∧ {⟨𝑧, 𝑚⟩}:{𝑧}–1-1-onto→{𝑚}) ∧ ((𝑥 ∩ {𝑧}) = ∅ ∧ (𝑚 ∩ {𝑚}) = ∅)) → (𝑓 ∪ {⟨𝑧, 𝑚⟩}):(𝑥 ∪ {𝑧})–1-1-onto→(𝑚 ∪ {𝑚}))
59	50, 57, 58	syl2an 598	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑓:𝑥–1-1-onto→𝑚 ∧ (𝑧 ∈ (𝐴 ∖ 𝑥) ∧ 𝑚 ∈ ω)) → (𝑓 ∪ {⟨𝑧, 𝑚⟩}):(𝑥 ∪ {𝑧})–1-1-onto→(𝑚 ∪ {𝑚}))
60		df-suc 6165	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ suc 𝑚 = (𝑚 ∪ {𝑚})
61		f1oeq3 6581	. . . . . . . . . . . . . . . . . . . . . 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 3444	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 𝑓 ∈ V
64		snex 5297	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ {⟨𝑧, 𝑚⟩} ∈ V
65	63, 64	unex 7449	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓 ∪ {⟨𝑧, 𝑚⟩}) ∈ V
66		f1oeq1 6579	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑔 = (𝑓 ∪ {⟨𝑧, 𝑚⟩}) → (𝑔:(𝑥 ∪ {𝑧})–1-1-onto→suc 𝑚 ↔ (𝑓 ∪ {⟨𝑧, 𝑚⟩}):(𝑥 ∪ {𝑧})–1-1-onto→suc 𝑚))
67	65, 66	spcev 3555	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑓 ∪ {⟨𝑧, 𝑚⟩}):(𝑥 ∪ {𝑧})–1-1-onto→suc 𝑚 → ∃𝑔 𝑔:(𝑥 ∪ {𝑧})–1-1-onto→suc 𝑚)
68		bren 8501	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 ∪ {𝑧}) ≈ suc 𝑚 ↔ ∃𝑔 𝑔:(𝑥 ∪ {𝑧})–1-1-onto→suc 𝑚)
69	67, 68	sylibr 237	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑓 ∪ {⟨𝑧, 𝑚⟩}):(𝑥 ∪ {𝑧})–1-1-onto→suc 𝑚 → (𝑥 ∪ {𝑧}) ≈ suc 𝑚)
70	62, 69	sylbir 238	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑓 ∪ {⟨𝑧, 𝑚⟩}):(𝑥 ∪ {𝑧})–1-1-onto→(𝑚 ∪ {𝑚}) → (𝑥 ∪ {𝑧}) ≈ suc 𝑚)
71	59, 70	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓:𝑥–1-1-onto→𝑚 ∧ (𝑧 ∈ (𝐴 ∖ 𝑥) ∧ 𝑚 ∈ ω)) → (𝑥 ∪ {𝑧}) ≈ suc 𝑚)
72	71	adantll 713	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑥 ⊆ 𝐴 ∧ 𝑓:𝑥–1-1-onto→𝑚) ∧ (𝑧 ∈ (𝐴 ∖ 𝑥) ∧ 𝑚 ∈ ω)) → (𝑥 ∪ {𝑧}) ≈ suc 𝑚)
73		vex 3444	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑥 ∈ V
74		snex 5297	. . . . . . . . . . . . . . . . . . . 20 ⊢ {𝑧} ∈ V
75	73, 74	unex 7449	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∪ {𝑧}) ∈ V
76		sseq1 3940	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = (𝑥 ∪ {𝑧}) → (𝑦 ⊆ 𝐴 ↔ (𝑥 ∪ {𝑧}) ⊆ 𝐴))
77		breq1 5033	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = (𝑥 ∪ {𝑧}) → (𝑦 ≈ suc 𝑚 ↔ (𝑥 ∪ {𝑧}) ≈ suc 𝑚))
78	76, 77	anbi12d 633	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = (𝑥 ∪ {𝑧}) → ((𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚) ↔ ((𝑥 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝑥 ∪ {𝑧}) ≈ suc 𝑚)))
79	75, 78	spcev 3555	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑥 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝑥 ∪ {𝑧}) ≈ suc 𝑚) → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚))
80	46, 72, 79	syl2anc 587	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑥 ⊆ 𝐴 ∧ 𝑓:𝑥–1-1-onto→𝑚) ∧ (𝑧 ∈ (𝐴 ∖ 𝑥) ∧ 𝑚 ∈ ω)) → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚))
81	80	expcom 417	. . . . . . . . . . . . . . . 16 ⊢ ((𝑧 ∈ (𝐴 ∖ 𝑥) ∧ 𝑚 ∈ ω) → ((𝑥 ⊆ 𝐴 ∧ 𝑓:𝑥–1-1-onto→𝑚) → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚)))
82	81	ex 416	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ (𝐴 ∖ 𝑥) → (𝑚 ∈ ω → ((𝑥 ⊆ 𝐴 ∧ 𝑓:𝑥–1-1-onto→𝑚) → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚))))
83	82	exlimiv 1931	. . . . . . . . . . . . . 14 ⊢ (∃𝑧 𝑧 ∈ (𝐴 ∖ 𝑥) → (𝑚 ∈ ω → ((𝑥 ⊆ 𝐴 ∧ 𝑓:𝑥–1-1-onto→𝑚) → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚))))
84	40, 83	sylbi 220	. . . . . . . . . . . . 13 ⊢ (¬ (𝐴 ∖ 𝑥) = ∅ → (𝑚 ∈ ω → ((𝑥 ⊆ 𝐴 ∧ 𝑓:𝑥–1-1-onto→𝑚) → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚))))
85	84	com13 88	. . . . . . . . . . . 12 ⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑓:𝑥–1-1-onto→𝑚) → (𝑚 ∈ ω → (¬ (𝐴 ∖ 𝑥) = ∅ → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚))))
86	85	expcom 417	. . . . . . . . . . 11 ⊢ (𝑓:𝑥–1-1-onto→𝑚 → (𝑥 ⊆ 𝐴 → (𝑚 ∈ ω → (¬ (𝐴 ∖ 𝑥) = ∅ → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚)))))
87	86	exlimiv 1931	. . . . . . . . . 10 ⊢ (∃𝑓 𝑓:𝑥–1-1-onto→𝑚 → (𝑥 ⊆ 𝐴 → (𝑚 ∈ ω → (¬ (𝐴 ∖ 𝑥) = ∅ → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚)))))
88	39, 87	sylbi 220	. . . . . . . . 9 ⊢ (𝑥 ≈ 𝑚 → (𝑥 ⊆ 𝐴 → (𝑚 ∈ ω → (¬ (𝐴 ∖ 𝑥) = ∅ → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚)))))
89	88	3imp21 1111	. . . . . . . 8 ⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑚 ∧ 𝑚 ∈ ω) → (¬ (𝐴 ∖ 𝑥) = ∅ → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚)))
90	38, 89	syld 47	. . . . . . 7 ⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑚 ∧ 𝑚 ∈ ω) → (¬ 𝐴 ∈ Fin → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚)))
91	90	3expia 1118	. . . . . 6 ⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑚) → (𝑚 ∈ ω → (¬ 𝐴 ∈ Fin → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚))))
92	91	exlimiv 1931	. . . . 5 ⊢ (∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑚) → (𝑚 ∈ ω → (¬ 𝐴 ∈ Fin → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚))))
93	92	com3l 89	. . . 4 ⊢ (𝑚 ∈ ω → (¬ 𝐴 ∈ Fin → (∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑚) → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚))))
94	3, 6, 13, 22, 93	finds2 7591	. . 3 ⊢ (𝑛 ∈ ω → (¬ 𝐴 ∈ Fin → ∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑛)))
95	94	com12 32	. 2 ⊢ (¬ 𝐴 ∈ Fin → (𝑛 ∈ ω → ∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑛)))
96	95	ralrimiv 3148	1 ⊢ (¬ 𝐴 ∈ Fin → ∀𝑛 ∈ ω ∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑛))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538  ∃wex 1781   ∈ wcel 2111  ∀wral 3106  ∃wrex 3107   ∖ cdif 3878   ∪ cun 3879   ∩ cin 3880   ⊆ wss 3881  ∅c0 4243  {csn 4525  ⟨cop 4531   class class class wbr 5030  Ord word 6158  suc csuc 6161  –1-1-onto→wf1o 6323  ωcom 7560   ≈ cen 8489  Fincfn 8492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-rab 3115  df-v 3443  df-sbc 3721  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4801  df-br 5031  df-opab 5093  df-tr 5137  df-id 5425  df-eprel 5430  df-po 5438  df-so 5439  df-fr 5478  df-we 5480  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-ord 6162  df-on 6163  df-lim 6164  df-suc 6165  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-om 7561  df-en 8493  df-fin 8496

This theorem is referenced by:  fineqvlem  8716  isinffi  9405  domtriomlem  9853  ishashinf  13817  ctbssinf  34823