Theorem isinf 8058

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 4587	. . . . . 6 ⊢ (𝑛 = ∅ → (𝑥 ≈ 𝑛 ↔ 𝑥 ≈ ∅))
2	1	anbi2d 736	. . . . 5 ⊢ (𝑛 = ∅ → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑛) ↔ (𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ ∅)))
3	2	exbidv 1837	. . . 4 ⊢ (𝑛 = ∅ → (∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑛) ↔ ∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ ∅)))
4		breq2 4587	. . . . . 6 ⊢ (𝑛 = 𝑚 → (𝑥 ≈ 𝑛 ↔ 𝑥 ≈ 𝑚))
5	4	anbi2d 736	. . . . 5 ⊢ (𝑛 = 𝑚 → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑛) ↔ (𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑚)))
6	5	exbidv 1837	. . . 4 ⊢ (𝑛 = 𝑚 → (∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑛) ↔ ∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑚)))
7		sseq1 3589	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑥 ⊆ 𝐴 ↔ 𝑦 ⊆ 𝐴))
8	7	adantl 481	. . . . . 6 ⊢ ((𝑛 = suc 𝑚 ∧ 𝑥 = 𝑦) → (𝑥 ⊆ 𝐴 ↔ 𝑦 ⊆ 𝐴))
9		breq1 4586	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑥 ≈ 𝑛 ↔ 𝑦 ≈ 𝑛))
10		breq2 4587	. . . . . . 7 ⊢ (𝑛 = suc 𝑚 → (𝑦 ≈ 𝑛 ↔ 𝑦 ≈ suc 𝑚))
11	9, 10	sylan9bbr 733	. . . . . 6 ⊢ ((𝑛 = suc 𝑚 ∧ 𝑥 = 𝑦) → (𝑥 ≈ 𝑛 ↔ 𝑦 ≈ suc 𝑚))
12	8, 11	anbi12d 743	. . . . 5 ⊢ ((𝑛 = suc 𝑚 ∧ 𝑥 = 𝑦) → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑛) ↔ (𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚)))
13	12	cbvexdva 2271	. . . 4 ⊢ (𝑛 = suc 𝑚 → (∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑛) ↔ ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚)))
14		0ss 3924	. . . . . 6 ⊢ ∅ ⊆ 𝐴
15		0ex 4718	. . . . . . 7 ⊢ ∅ ∈ V
16	15	enref 7874	. . . . . 6 ⊢ ∅ ≈ ∅
17		sseq1 3589	. . . . . . . 8 ⊢ (𝑥 = ∅ → (𝑥 ⊆ 𝐴 ↔ ∅ ⊆ 𝐴))
18		breq1 4586	. . . . . . . 8 ⊢ (𝑥 = ∅ → (𝑥 ≈ ∅ ↔ ∅ ≈ ∅))
19	17, 18	anbi12d 743	. . . . . . 7 ⊢ (𝑥 = ∅ → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ ∅) ↔ (∅ ⊆ 𝐴 ∧ ∅ ≈ ∅)))
20	15, 19	spcev 3273	. . . . . 6 ⊢ ((∅ ⊆ 𝐴 ∧ ∅ ≈ ∅) → ∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ ∅))
21	14, 16, 20	mp2an 704	. . . . 5 ⊢ ∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ ∅)
22	21	a1i 11	. . . 4 ⊢ (¬ 𝐴 ∈ Fin → ∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ ∅))
23		ssdif0 3896	. . . . . . . . . . . . 13 ⊢ (𝐴 ⊆ 𝑥 ↔ (𝐴 ∖ 𝑥) = ∅)
24		eqss 3583	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝐴 ↔ (𝑥 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝑥))
25		breq1 4586	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝐴 → (𝑥 ≈ 𝑚 ↔ 𝐴 ≈ 𝑚))
26	25	biimpa 500	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 = 𝐴 ∧ 𝑥 ≈ 𝑚) → 𝐴 ≈ 𝑚)
27		rspe 2986	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑚 ∈ ω ∧ 𝐴 ≈ 𝑚) → ∃𝑚 ∈ ω 𝐴 ≈ 𝑚)
28	26, 27	sylan2 490	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑚 ∈ ω ∧ (𝑥 = 𝐴 ∧ 𝑥 ≈ 𝑚)) → ∃𝑚 ∈ ω 𝐴 ≈ 𝑚)
29		isfi 7865	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ Fin ↔ ∃𝑚 ∈ ω 𝐴 ≈ 𝑚)
30	28, 29	sylibr 223	. . . . . . . . . . . . . . . 16 ⊢ ((𝑚 ∈ ω ∧ (𝑥 = 𝐴 ∧ 𝑥 ≈ 𝑚)) → 𝐴 ∈ Fin)
31	30	expcom 450	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 = 𝐴 ∧ 𝑥 ≈ 𝑚) → (𝑚 ∈ ω → 𝐴 ∈ Fin))
32	24, 31	sylanbr 489	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝑥) ∧ 𝑥 ≈ 𝑚) → (𝑚 ∈ ω → 𝐴 ∈ Fin))
33	32	ex 449	. . . . . . . . . . . . 13 ⊢ ((𝑥 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝑥) → (𝑥 ≈ 𝑚 → (𝑚 ∈ ω → 𝐴 ∈ Fin)))
34	23, 33	sylan2br 492	. . . . . . . . . . . 12 ⊢ ((𝑥 ⊆ 𝐴 ∧ (𝐴 ∖ 𝑥) = ∅) → (𝑥 ≈ 𝑚 → (𝑚 ∈ ω → 𝐴 ∈ Fin)))
35	34	expcom 450	. . . . . . . . . . 11 ⊢ ((𝐴 ∖ 𝑥) = ∅ → (𝑥 ⊆ 𝐴 → (𝑥 ≈ 𝑚 → (𝑚 ∈ ω → 𝐴 ∈ Fin))))
36	35	3impd 1273	. . . . . . . . . 10 ⊢ ((𝐴 ∖ 𝑥) = ∅ → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑚 ∧ 𝑚 ∈ ω) → 𝐴 ∈ Fin))
37	36	com12 32	. . . . . . . . 9 ⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑚 ∧ 𝑚 ∈ ω) → ((𝐴 ∖ 𝑥) = ∅ → 𝐴 ∈ Fin))
38	37	con3d 147	. . . . . . . 8 ⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑚 ∧ 𝑚 ∈ ω) → (¬ 𝐴 ∈ Fin → ¬ (𝐴 ∖ 𝑥) = ∅))
39		bren 7850	. . . . . . . . . . 11 ⊢ (𝑥 ≈ 𝑚 ↔ ∃𝑓 𝑓:𝑥–1-1-onto→𝑚)
40		neq0 3889	. . . . . . . . . . . . . . 15 ⊢ (¬ (𝐴 ∖ 𝑥) = ∅ ↔ ∃𝑧 𝑧 ∈ (𝐴 ∖ 𝑥))
41		eldifi 3694	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 ∈ (𝐴 ∖ 𝑥) → 𝑧 ∈ 𝐴)
42	41	snssd 4281	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 ∈ (𝐴 ∖ 𝑥) → {𝑧} ⊆ 𝐴)
43		unss 3749	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 ⊆ 𝐴 ∧ {𝑧} ⊆ 𝐴) ↔ (𝑥 ∪ {𝑧}) ⊆ 𝐴)
44	43	biimpi 205	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ⊆ 𝐴 ∧ {𝑧} ⊆ 𝐴) → (𝑥 ∪ {𝑧}) ⊆ 𝐴)
45	42, 44	sylan2 490	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑥)) → (𝑥 ∪ {𝑧}) ⊆ 𝐴)
46	45	ad2ant2r 779	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑥 ⊆ 𝐴 ∧ 𝑓:𝑥–1-1-onto→𝑚) ∧ (𝑧 ∈ (𝐴 ∖ 𝑥) ∧ 𝑚 ∈ ω)) → (𝑥 ∪ {𝑧}) ⊆ 𝐴)
47		vex 3176	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 𝑧 ∈ V
48		vex 3176	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 𝑚 ∈ V
49	47, 48	f1osn 6088	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ {⟨𝑧, 𝑚⟩}:{𝑧}–1-1-onto→{𝑚}
50	49	jctr 563	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑓:𝑥–1-1-onto→𝑚 → (𝑓:𝑥–1-1-onto→𝑚 ∧ {⟨𝑧, 𝑚⟩}:{𝑧}–1-1-onto→{𝑚}))
51		eldifn 3695	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑧 ∈ (𝐴 ∖ 𝑥) → ¬ 𝑧 ∈ 𝑥)
52		disjsn 4192	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑥 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ 𝑥)
53	51, 52	sylibr 223	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧 ∈ (𝐴 ∖ 𝑥) → (𝑥 ∩ {𝑧}) = ∅)
54		nnord 6965	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑚 ∈ ω → Ord 𝑚)
55		orddisj 5679	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (Ord 𝑚 → (𝑚 ∩ {𝑚}) = ∅)
56	54, 55	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑚 ∈ ω → (𝑚 ∩ {𝑚}) = ∅)
57	53, 56	anim12i 588	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑧 ∈ (𝐴 ∖ 𝑥) ∧ 𝑚 ∈ ω) → ((𝑥 ∩ {𝑧}) = ∅ ∧ (𝑚 ∩ {𝑚}) = ∅))
58		f1oun 6069	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑓:𝑥–1-1-onto→𝑚 ∧ {⟨𝑧, 𝑚⟩}:{𝑧}–1-1-onto→{𝑚}) ∧ ((𝑥 ∩ {𝑧}) = ∅ ∧ (𝑚 ∩ {𝑚}) = ∅)) → (𝑓 ∪ {⟨𝑧, 𝑚⟩}):(𝑥 ∪ {𝑧})–1-1-onto→(𝑚 ∪ {𝑚}))
59	50, 57, 58	syl2an 493	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑓:𝑥–1-1-onto→𝑚 ∧ (𝑧 ∈ (𝐴 ∖ 𝑥) ∧ 𝑚 ∈ ω)) → (𝑓 ∪ {⟨𝑧, 𝑚⟩}):(𝑥 ∪ {𝑧})–1-1-onto→(𝑚 ∪ {𝑚}))
60		df-suc 5646	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ suc 𝑚 = (𝑚 ∪ {𝑚})
61		f1oeq3 6042	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (suc 𝑚 = (𝑚 ∪ {𝑚}) → ((𝑓 ∪ {⟨𝑧, 𝑚⟩}):(𝑥 ∪ {𝑧})–1-1-onto→suc 𝑚 ↔ (𝑓 ∪ {⟨𝑧, 𝑚⟩}):(𝑥 ∪ {𝑧})–1-1-onto→(𝑚 ∪ {𝑚})))
62	60, 61	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑓 ∪ {⟨𝑧, 𝑚⟩}):(𝑥 ∪ {𝑧})–1-1-onto→suc 𝑚 ↔ (𝑓 ∪ {⟨𝑧, 𝑚⟩}):(𝑥 ∪ {𝑧})–1-1-onto→(𝑚 ∪ {𝑚}))
63		vex 3176	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 𝑓 ∈ V
64		snex 4835	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ {⟨𝑧, 𝑚⟩} ∈ V
65	63, 64	unex 6854	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑓 ∪ {⟨𝑧, 𝑚⟩}) ∈ V
66		f1oeq1 6040	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑔 = (𝑓 ∪ {⟨𝑧, 𝑚⟩}) → (𝑔:(𝑥 ∪ {𝑧})–1-1-onto→suc 𝑚 ↔ (𝑓 ∪ {⟨𝑧, 𝑚⟩}):(𝑥 ∪ {𝑧})–1-1-onto→suc 𝑚))
67	65, 66	spcev 3273	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑓 ∪ {⟨𝑧, 𝑚⟩}):(𝑥 ∪ {𝑧})–1-1-onto→suc 𝑚 → ∃𝑔 𝑔:(𝑥 ∪ {𝑧})–1-1-onto→suc 𝑚)
68		bren 7850	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑥 ∪ {𝑧}) ≈ suc 𝑚 ↔ ∃𝑔 𝑔:(𝑥 ∪ {𝑧})–1-1-onto→suc 𝑚)
69	67, 68	sylibr 223	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑓 ∪ {⟨𝑧, 𝑚⟩}):(𝑥 ∪ {𝑧})–1-1-onto→suc 𝑚 → (𝑥 ∪ {𝑧}) ≈ suc 𝑚)
70	62, 69	sylbir 224	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑓 ∪ {⟨𝑧, 𝑚⟩}):(𝑥 ∪ {𝑧})–1-1-onto→(𝑚 ∪ {𝑚}) → (𝑥 ∪ {𝑧}) ≈ suc 𝑚)
71	59, 70	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑓:𝑥–1-1-onto→𝑚 ∧ (𝑧 ∈ (𝐴 ∖ 𝑥) ∧ 𝑚 ∈ ω)) → (𝑥 ∪ {𝑧}) ≈ suc 𝑚)
72	71	adantll 746	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑥 ⊆ 𝐴 ∧ 𝑓:𝑥–1-1-onto→𝑚) ∧ (𝑧 ∈ (𝐴 ∖ 𝑥) ∧ 𝑚 ∈ ω)) → (𝑥 ∪ {𝑧}) ≈ suc 𝑚)
73		vex 3176	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑥 ∈ V
74		snex 4835	. . . . . . . . . . . . . . . . . . . . 21 ⊢ {𝑧} ∈ V
75	73, 74	unex 6854	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∪ {𝑧}) ∈ V
76		sseq1 3589	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = (𝑥 ∪ {𝑧}) → (𝑦 ⊆ 𝐴 ↔ (𝑥 ∪ {𝑧}) ⊆ 𝐴))
77		breq1 4586	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = (𝑥 ∪ {𝑧}) → (𝑦 ≈ suc 𝑚 ↔ (𝑥 ∪ {𝑧}) ≈ suc 𝑚))
78	76, 77	anbi12d 743	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = (𝑥 ∪ {𝑧}) → ((𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚) ↔ ((𝑥 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝑥 ∪ {𝑧}) ≈ suc 𝑚)))
79	75, 78	spcev 3273	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑥 ∪ {𝑧}) ⊆ 𝐴 ∧ (𝑥 ∪ {𝑧}) ≈ suc 𝑚) → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚))
80	46, 72, 79	syl2anc 691	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑥 ⊆ 𝐴 ∧ 𝑓:𝑥–1-1-onto→𝑚) ∧ (𝑧 ∈ (𝐴 ∖ 𝑥) ∧ 𝑚 ∈ ω)) → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚))
81	80	expcom 450	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑧 ∈ (𝐴 ∖ 𝑥) ∧ 𝑚 ∈ ω) → ((𝑥 ⊆ 𝐴 ∧ 𝑓:𝑥–1-1-onto→𝑚) → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚)))
82	81	ex 449	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ (𝐴 ∖ 𝑥) → (𝑚 ∈ ω → ((𝑥 ⊆ 𝐴 ∧ 𝑓:𝑥–1-1-onto→𝑚) → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚))))
83	82	exlimiv 1845	. . . . . . . . . . . . . . 15 ⊢ (∃𝑧 𝑧 ∈ (𝐴 ∖ 𝑥) → (𝑚 ∈ ω → ((𝑥 ⊆ 𝐴 ∧ 𝑓:𝑥–1-1-onto→𝑚) → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚))))
84	40, 83	sylbi 206	. . . . . . . . . . . . . 14 ⊢ (¬ (𝐴 ∖ 𝑥) = ∅ → (𝑚 ∈ ω → ((𝑥 ⊆ 𝐴 ∧ 𝑓:𝑥–1-1-onto→𝑚) → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚))))
85	84	com13 86	. . . . . . . . . . . . 13 ⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑓:𝑥–1-1-onto→𝑚) → (𝑚 ∈ ω → (¬ (𝐴 ∖ 𝑥) = ∅ → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚))))
86	85	expcom 450	. . . . . . . . . . . 12 ⊢ (𝑓:𝑥–1-1-onto→𝑚 → (𝑥 ⊆ 𝐴 → (𝑚 ∈ ω → (¬ (𝐴 ∖ 𝑥) = ∅ → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚)))))
87	86	exlimiv 1845	. . . . . . . . . . 11 ⊢ (∃𝑓 𝑓:𝑥–1-1-onto→𝑚 → (𝑥 ⊆ 𝐴 → (𝑚 ∈ ω → (¬ (𝐴 ∖ 𝑥) = ∅ → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚)))))
88	39, 87	sylbi 206	. . . . . . . . . 10 ⊢ (𝑥 ≈ 𝑚 → (𝑥 ⊆ 𝐴 → (𝑚 ∈ ω → (¬ (𝐴 ∖ 𝑥) = ∅ → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚)))))
89	88	com12 32	. . . . . . . . 9 ⊢ (𝑥 ⊆ 𝐴 → (𝑥 ≈ 𝑚 → (𝑚 ∈ ω → (¬ (𝐴 ∖ 𝑥) = ∅ → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚)))))
90	89	3imp 1249	. . . . . . . 8 ⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑚 ∧ 𝑚 ∈ ω) → (¬ (𝐴 ∖ 𝑥) = ∅ → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚)))
91	38, 90	syld 46	. . . . . . 7 ⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑚 ∧ 𝑚 ∈ ω) → (¬ 𝐴 ∈ Fin → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚)))
92	91	3expia 1259	. . . . . 6 ⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑚) → (𝑚 ∈ ω → (¬ 𝐴 ∈ Fin → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚))))
93	92	exlimiv 1845	. . . . 5 ⊢ (∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑚) → (𝑚 ∈ ω → (¬ 𝐴 ∈ Fin → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚))))
94	93	com3l 87	. . . 4 ⊢ (𝑚 ∈ ω → (¬ 𝐴 ∈ Fin → (∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑚) → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚))))
95	3, 6, 13, 22, 94	finds2 6986	. . 3 ⊢ (𝑛 ∈ ω → (¬ 𝐴 ∈ Fin → ∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑛)))
96	95	com12 32	. 2 ⊢ (¬ 𝐴 ∈ Fin → (𝑛 ∈ ω → ∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑛)))
97	96	ralrimiv 2948	1 ⊢ (¬ 𝐴 ∈ Fin → ∀𝑛 ∈ ω ∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑛))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∧ wa 383   ∧ w3a 1031   = wceq 1475  ∃wex 1695   ∈ wcel 1977  ∀wral 2896  ∃wrex 2897   ∖ cdif 3537   ∪ cun 3538   ∩ cin 3539   ⊆ wss 3540  ∅c0 3874  {csn 4125  ⟨cop 4131   class class class wbr 4583  Ord word 5639  suc csuc 5642  –1-1-onto→wf1o 5803  ωcom 6957   ≈ cen 7838  Fincfn 7841

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-om 6958  df-en 7842  df-fin 7845

This theorem is referenced by:  fineqvlem  8059  isinffi  8701  domtriomlem  9147  ishashinf  13104