Metamath Proof Explorer

Theorem isinf

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 hascountably infinite subsets unless AC is invoked.) The proof does not require the Axiom of Infinity. (Contributed by Mario Carneiro, 15-Jan-2013) Avoid ax-pow . (Revised by BTernaryTau, 2-Jan-2025)

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

Proof

Step Hyp Ref Expression
1 breq2 ⊢ ( 𝑛 = ∅ → ( 𝑥 ≈ 𝑛 ↔ 𝑥 ≈ ∅ ) )
2 1 anbi2d ⊢ ( 𝑛 = ∅ → ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑛 ) ↔ ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ ∅ ) ) )
3 2 exbidv ⊢ ( 𝑛 = ∅ → ( ∃ 𝑥 ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑛 ) ↔ ∃ 𝑥 ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ ∅ ) ) )
4 breq2 ⊢ ( 𝑛 = 𝑚 → ( 𝑥 ≈ 𝑛 ↔ 𝑥 ≈ 𝑚 ) )
5 4 anbi2d ⊢ ( 𝑛 = 𝑚 → ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑛 ) ↔ ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑚 ) ) )
6 5 exbidv ⊢ ( 𝑛 = 𝑚 → ( ∃ 𝑥 ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑛 ) ↔ ∃ 𝑥 ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑚 ) ) )
7 sseq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ⊆ 𝐴 ↔ 𝑦 ⊆ 𝐴 ) )
8 7 adantl ⊢ ( ( 𝑛 = suc 𝑚 ∧ 𝑥 = 𝑦 ) → ( 𝑥 ⊆ 𝐴 ↔ 𝑦 ⊆ 𝐴 ) )
9 breq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ≈ 𝑛 ↔ 𝑦 ≈ 𝑛 ) )
10 breq2 ⊢ ( 𝑛 = suc 𝑚 → ( 𝑦 ≈ 𝑛 ↔ 𝑦 ≈ suc 𝑚 ) )
11 9 10 sylan9bbr ⊢ ( ( 𝑛 = suc 𝑚 ∧ 𝑥 = 𝑦 ) → ( 𝑥 ≈ 𝑛 ↔ 𝑦 ≈ suc 𝑚 ) )
12 8 11 anbi12d ⊢ ( ( 𝑛 = suc 𝑚 ∧ 𝑥 = 𝑦 ) → ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑛 ) ↔ ( 𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚 ) ) )
13 12 cbvexdvaw ⊢ ( 𝑛 = suc 𝑚 → ( ∃ 𝑥 ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑛 ) ↔ ∃ 𝑦 ( 𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚 ) ) )
14 0ss ⊢ ∅ ⊆ 𝐴
15 peano1 ⊢ ∅ ∈ ω
16 enrefnn ⊢ ( ∅ ∈ ω → ∅ ≈ ∅ )
17 15 16 ax-mp ⊢ ∅ ≈ ∅
18 0ex ⊢ ∅ ∈ V
19 sseq1 ⊢ ( 𝑥 = ∅ → ( 𝑥 ⊆ 𝐴 ↔ ∅ ⊆ 𝐴 ) )
20 breq1 ⊢ ( 𝑥 = ∅ → ( 𝑥 ≈ ∅ ↔ ∅ ≈ ∅ ) )
21 19 20 anbi12d ⊢ ( 𝑥 = ∅ → ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ ∅ ) ↔ ( ∅ ⊆ 𝐴 ∧ ∅ ≈ ∅ ) ) )
22 18 21 spcev ⊢ ( ( ∅ ⊆ 𝐴 ∧ ∅ ≈ ∅ ) → ∃ 𝑥 ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ ∅ ) )
23 14 17 22 mp2an ⊢ ∃ 𝑥 ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ ∅ )
24 23 a1i ⊢ ( ¬ 𝐴 ∈ Fin → ∃ 𝑥 ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ ∅ ) )
25 ssdif0 ⊢ ( 𝐴 ⊆ 𝑥 ↔ ( 𝐴 ∖ 𝑥 ) = ∅ )
26 eqss ⊢ ( 𝑥 = 𝐴 ↔ ( 𝑥 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝑥 ) )
27 breq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 ≈ 𝑚 ↔ 𝐴 ≈ 𝑚 ) )
28 27 biimpa ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑥 ≈ 𝑚 ) → 𝐴 ≈ 𝑚 )
29 rspe ⊢ ( ( 𝑚 ∈ ω ∧ 𝐴 ≈ 𝑚 ) → ∃ 𝑚 ∈ ω 𝐴 ≈ 𝑚 )
30 28 29 sylan2 ⊢ ( ( 𝑚 ∈ ω ∧ ( 𝑥 = 𝐴 ∧ 𝑥 ≈ 𝑚 ) ) → ∃ 𝑚 ∈ ω 𝐴 ≈ 𝑚 )
31 isfi ⊢ ( 𝐴 ∈ Fin ↔ ∃ 𝑚 ∈ ω 𝐴 ≈ 𝑚 )
32 30 31 sylibr ⊢ ( ( 𝑚 ∈ ω ∧ ( 𝑥 = 𝐴 ∧ 𝑥 ≈ 𝑚 ) ) → 𝐴 ∈ Fin )
33 32 expcom ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑥 ≈ 𝑚 ) → ( 𝑚 ∈ ω → 𝐴 ∈ Fin ) )
34 26 33 sylanbr ⊢ ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝑥 ) ∧ 𝑥 ≈ 𝑚 ) → ( 𝑚 ∈ ω → 𝐴 ∈ Fin ) )
35 34 ex ⊢ ( ( 𝑥 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝑥 ) → ( 𝑥 ≈ 𝑚 → ( 𝑚 ∈ ω → 𝐴 ∈ Fin ) ) )
36 25 35 sylan2br ⊢ ( ( 𝑥 ⊆ 𝐴 ∧ ( 𝐴 ∖ 𝑥 ) = ∅ ) → ( 𝑥 ≈ 𝑚 → ( 𝑚 ∈ ω → 𝐴 ∈ Fin ) ) )
37 36 expcom ⊢ ( ( 𝐴 ∖ 𝑥 ) = ∅ → ( 𝑥 ⊆ 𝐴 → ( 𝑥 ≈ 𝑚 → ( 𝑚 ∈ ω → 𝐴 ∈ Fin ) ) ) )
38 37 3impd ⊢ ( ( 𝐴 ∖ 𝑥 ) = ∅ → ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑚 ∧ 𝑚 ∈ ω ) → 𝐴 ∈ Fin ) )
39 38 com12 ⊢ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑚 ∧ 𝑚 ∈ ω ) → ( ( 𝐴 ∖ 𝑥 ) = ∅ → 𝐴 ∈ Fin ) )
40 39 con3d ⊢ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑚 ∧ 𝑚 ∈ ω ) → ( ¬ 𝐴 ∈ Fin → ¬ ( 𝐴 ∖ 𝑥 ) = ∅ ) )
41 bren ⊢ ( 𝑥 ≈ 𝑚 ↔ ∃ 𝑓 𝑓 : 𝑥 –1-1-onto→ 𝑚 )
42 neq0 ⊢ ( ¬ ( 𝐴 ∖ 𝑥 ) = ∅ ↔ ∃ 𝑧 𝑧 ∈ ( 𝐴 ∖ 𝑥 ) )
43 eldifi ⊢ ( 𝑧 ∈ ( 𝐴 ∖ 𝑥 ) → 𝑧 ∈ 𝐴 )
44 43 snssd ⊢ ( 𝑧 ∈ ( 𝐴 ∖ 𝑥 ) → { 𝑧 } ⊆ 𝐴 )
45 unss ⊢ ( ( 𝑥 ⊆ 𝐴 ∧ { 𝑧 } ⊆ 𝐴 ) ↔ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐴 )
46 45 biimpi ⊢ ( ( 𝑥 ⊆ 𝐴 ∧ { 𝑧 } ⊆ 𝐴 ) → ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐴 )
47 44 46 sylan2 ⊢ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑥 ) ) → ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐴 )
48 47 ad2ant2r ⊢ ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑓 : 𝑥 –1-1-onto→ 𝑚 ) ∧ ( 𝑧 ∈ ( 𝐴 ∖ 𝑥 ) ∧ 𝑚 ∈ ω ) ) → ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐴 )
49 vex ⊢ 𝑧 ∈ V
50 vex ⊢ 𝑚 ∈ V
51 49 50 f1osn ⊢ { ⟨ 𝑧 , 𝑚 ⟩ } : { 𝑧 } –1-1-onto→ { 𝑚 }
52 51 jctr ⊢ ( 𝑓 : 𝑥 –1-1-onto→ 𝑚 → ( 𝑓 : 𝑥 –1-1-onto→ 𝑚 ∧ { ⟨ 𝑧 , 𝑚 ⟩ } : { 𝑧 } –1-1-onto→ { 𝑚 } ) )
53 eldifn ⊢ ( 𝑧 ∈ ( 𝐴 ∖ 𝑥 ) → ¬ 𝑧 ∈ 𝑥 )
54 disjsn ⊢ ( ( 𝑥 ∩ { 𝑧 } ) = ∅ ↔ ¬ 𝑧 ∈ 𝑥 )
55 53 54 sylibr ⊢ ( 𝑧 ∈ ( 𝐴 ∖ 𝑥 ) → ( 𝑥 ∩ { 𝑧 } ) = ∅ )
56 nnord ⊢ ( 𝑚 ∈ ω → Ord 𝑚 )
57 orddisj ⊢ ( Ord 𝑚 → ( 𝑚 ∩ { 𝑚 } ) = ∅ )
58 56 57 syl ⊢ ( 𝑚 ∈ ω → ( 𝑚 ∩ { 𝑚 } ) = ∅ )
59 55 58 anim12i ⊢ ( ( 𝑧 ∈ ( 𝐴 ∖ 𝑥 ) ∧ 𝑚 ∈ ω ) → ( ( 𝑥 ∩ { 𝑧 } ) = ∅ ∧ ( 𝑚 ∩ { 𝑚 } ) = ∅ ) )
60 f1oun ⊢ ( ( ( 𝑓 : 𝑥 –1-1-onto→ 𝑚 ∧ { ⟨ 𝑧 , 𝑚 ⟩ } : { 𝑧 } –1-1-onto→ { 𝑚 } ) ∧ ( ( 𝑥 ∩ { 𝑧 } ) = ∅ ∧ ( 𝑚 ∩ { 𝑚 } ) = ∅ ) ) → ( 𝑓 ∪ { ⟨ 𝑧 , 𝑚 ⟩ } ) : ( 𝑥 ∪ { 𝑧 } ) –1-1-onto→ ( 𝑚 ∪ { 𝑚 } ) )
61 52 59 60 syl2an ⊢ ( ( 𝑓 : 𝑥 –1-1-onto→ 𝑚 ∧ ( 𝑧 ∈ ( 𝐴 ∖ 𝑥 ) ∧ 𝑚 ∈ ω ) ) → ( 𝑓 ∪ { ⟨ 𝑧 , 𝑚 ⟩ } ) : ( 𝑥 ∪ { 𝑧 } ) –1-1-onto→ ( 𝑚 ∪ { 𝑚 } ) )
62 df-suc ⊢ suc 𝑚 = ( 𝑚 ∪ { 𝑚 } )
63 f1oeq3 ⊢ ( suc 𝑚 = ( 𝑚 ∪ { 𝑚 } ) → ( ( 𝑓 ∪ { ⟨ 𝑧 , 𝑚 ⟩ } ) : ( 𝑥 ∪ { 𝑧 } ) –1-1-onto→ suc 𝑚 ↔ ( 𝑓 ∪ { ⟨ 𝑧 , 𝑚 ⟩ } ) : ( 𝑥 ∪ { 𝑧 } ) –1-1-onto→ ( 𝑚 ∪ { 𝑚 } ) ) )
64 62 63 ax-mp ⊢ ( ( 𝑓 ∪ { ⟨ 𝑧 , 𝑚 ⟩ } ) : ( 𝑥 ∪ { 𝑧 } ) –1-1-onto→ suc 𝑚 ↔ ( 𝑓 ∪ { ⟨ 𝑧 , 𝑚 ⟩ } ) : ( 𝑥 ∪ { 𝑧 } ) –1-1-onto→ ( 𝑚 ∪ { 𝑚 } ) )
65 vex ⊢ 𝑓 ∈ V
66 snex ⊢ { ⟨ 𝑧 , 𝑚 ⟩ } ∈ V
67 65 66 unex ⊢ ( 𝑓 ∪ { ⟨ 𝑧 , 𝑚 ⟩ } ) ∈ V
68 f1oeq1 ⊢ ( 𝑔 = ( 𝑓 ∪ { ⟨ 𝑧 , 𝑚 ⟩ } ) → ( 𝑔 : ( 𝑥 ∪ { 𝑧 } ) –1-1-onto→ suc 𝑚 ↔ ( 𝑓 ∪ { ⟨ 𝑧 , 𝑚 ⟩ } ) : ( 𝑥 ∪ { 𝑧 } ) –1-1-onto→ suc 𝑚 ) )
69 67 68 spcev ⊢ ( ( 𝑓 ∪ { ⟨ 𝑧 , 𝑚 ⟩ } ) : ( 𝑥 ∪ { 𝑧 } ) –1-1-onto→ suc 𝑚 → ∃ 𝑔 𝑔 : ( 𝑥 ∪ { 𝑧 } ) –1-1-onto→ suc 𝑚 )
70 bren ⊢ ( ( 𝑥 ∪ { 𝑧 } ) ≈ suc 𝑚 ↔ ∃ 𝑔 𝑔 : ( 𝑥 ∪ { 𝑧 } ) –1-1-onto→ suc 𝑚 )
71 69 70 sylibr ⊢ ( ( 𝑓 ∪ { ⟨ 𝑧 , 𝑚 ⟩ } ) : ( 𝑥 ∪ { 𝑧 } ) –1-1-onto→ suc 𝑚 → ( 𝑥 ∪ { 𝑧 } ) ≈ suc 𝑚 )
72 64 71 sylbir ⊢ ( ( 𝑓 ∪ { ⟨ 𝑧 , 𝑚 ⟩ } ) : ( 𝑥 ∪ { 𝑧 } ) –1-1-onto→ ( 𝑚 ∪ { 𝑚 } ) → ( 𝑥 ∪ { 𝑧 } ) ≈ suc 𝑚 )
73 61 72 syl ⊢ ( ( 𝑓 : 𝑥 –1-1-onto→ 𝑚 ∧ ( 𝑧 ∈ ( 𝐴 ∖ 𝑥 ) ∧ 𝑚 ∈ ω ) ) → ( 𝑥 ∪ { 𝑧 } ) ≈ suc 𝑚 )
74 73 adantll ⊢ ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑓 : 𝑥 –1-1-onto→ 𝑚 ) ∧ ( 𝑧 ∈ ( 𝐴 ∖ 𝑥 ) ∧ 𝑚 ∈ ω ) ) → ( 𝑥 ∪ { 𝑧 } ) ≈ suc 𝑚 )
75 vex ⊢ 𝑥 ∈ V
76 snex ⊢ { 𝑧 } ∈ V
77 75 76 unex ⊢ ( 𝑥 ∪ { 𝑧 } ) ∈ V
78 sseq1 ⊢ ( 𝑦 = ( 𝑥 ∪ { 𝑧 } ) → ( 𝑦 ⊆ 𝐴 ↔ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐴 ) )
79 breq1 ⊢ ( 𝑦 = ( 𝑥 ∪ { 𝑧 } ) → ( 𝑦 ≈ suc 𝑚 ↔ ( 𝑥 ∪ { 𝑧 } ) ≈ suc 𝑚 ) )
80 78 79 anbi12d ⊢ ( 𝑦 = ( 𝑥 ∪ { 𝑧 } ) → ( ( 𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚 ) ↔ ( ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐴 ∧ ( 𝑥 ∪ { 𝑧 } ) ≈ suc 𝑚 ) ) )
81 77 80 spcev ⊢ ( ( ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐴 ∧ ( 𝑥 ∪ { 𝑧 } ) ≈ suc 𝑚 ) → ∃ 𝑦 ( 𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚 ) )
82 48 74 81 syl2anc ⊢ ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑓 : 𝑥 –1-1-onto→ 𝑚 ) ∧ ( 𝑧 ∈ ( 𝐴 ∖ 𝑥 ) ∧ 𝑚 ∈ ω ) ) → ∃ 𝑦 ( 𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚 ) )
83 82 expcom ⊢ ( ( 𝑧 ∈ ( 𝐴 ∖ 𝑥 ) ∧ 𝑚 ∈ ω ) → ( ( 𝑥 ⊆ 𝐴 ∧ 𝑓 : 𝑥 –1-1-onto→ 𝑚 ) → ∃ 𝑦 ( 𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚 ) ) )
84 83 ex ⊢ ( 𝑧 ∈ ( 𝐴 ∖ 𝑥 ) → ( 𝑚 ∈ ω → ( ( 𝑥 ⊆ 𝐴 ∧ 𝑓 : 𝑥 –1-1-onto→ 𝑚 ) → ∃ 𝑦 ( 𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚 ) ) ) )
85 84 exlimiv ⊢ ( ∃ 𝑧 𝑧 ∈ ( 𝐴 ∖ 𝑥 ) → ( 𝑚 ∈ ω → ( ( 𝑥 ⊆ 𝐴 ∧ 𝑓 : 𝑥 –1-1-onto→ 𝑚 ) → ∃ 𝑦 ( 𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚 ) ) ) )
86 42 85 sylbi ⊢ ( ¬ ( 𝐴 ∖ 𝑥 ) = ∅ → ( 𝑚 ∈ ω → ( ( 𝑥 ⊆ 𝐴 ∧ 𝑓 : 𝑥 –1-1-onto→ 𝑚 ) → ∃ 𝑦 ( 𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚 ) ) ) )
87 86 com13 ⊢ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑓 : 𝑥 –1-1-onto→ 𝑚 ) → ( 𝑚 ∈ ω → ( ¬ ( 𝐴 ∖ 𝑥 ) = ∅ → ∃ 𝑦 ( 𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚 ) ) ) )
88 87 expcom ⊢ ( 𝑓 : 𝑥 –1-1-onto→ 𝑚 → ( 𝑥 ⊆ 𝐴 → ( 𝑚 ∈ ω → ( ¬ ( 𝐴 ∖ 𝑥 ) = ∅ → ∃ 𝑦 ( 𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚 ) ) ) ) )
89 88 exlimiv ⊢ ( ∃ 𝑓 𝑓 : 𝑥 –1-1-onto→ 𝑚 → ( 𝑥 ⊆ 𝐴 → ( 𝑚 ∈ ω → ( ¬ ( 𝐴 ∖ 𝑥 ) = ∅ → ∃ 𝑦 ( 𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚 ) ) ) ) )
90 41 89 sylbi ⊢ ( 𝑥 ≈ 𝑚 → ( 𝑥 ⊆ 𝐴 → ( 𝑚 ∈ ω → ( ¬ ( 𝐴 ∖ 𝑥 ) = ∅ → ∃ 𝑦 ( 𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚 ) ) ) ) )
91 90 3imp21 ⊢ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑚 ∧ 𝑚 ∈ ω ) → ( ¬ ( 𝐴 ∖ 𝑥 ) = ∅ → ∃ 𝑦 ( 𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚 ) ) )
92 40 91 syld ⊢ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑚 ∧ 𝑚 ∈ ω ) → ( ¬ 𝐴 ∈ Fin → ∃ 𝑦 ( 𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚 ) ) )
93 92 3expia ⊢ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑚 ) → ( 𝑚 ∈ ω → ( ¬ 𝐴 ∈ Fin → ∃ 𝑦 ( 𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚 ) ) ) )
94 93 exlimiv ⊢ ( ∃ 𝑥 ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑚 ) → ( 𝑚 ∈ ω → ( ¬ 𝐴 ∈ Fin → ∃ 𝑦 ( 𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚 ) ) ) )
95 94 com3l ⊢ ( 𝑚 ∈ ω → ( ¬ 𝐴 ∈ Fin → ( ∃ 𝑥 ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑚 ) → ∃ 𝑦 ( 𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ suc 𝑚 ) ) ) )
96 3 6 13 24 95 finds2 ⊢ ( 𝑛 ∈ ω → ( ¬ 𝐴 ∈ Fin → ∃ 𝑥 ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑛 ) ) )
97 96 com12 ⊢ ( ¬ 𝐴 ∈ Fin → ( 𝑛 ∈ ω → ∃ 𝑥 ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑛 ) ) )
98 97 ralrimiv ⊢ ( ¬ 𝐴 ∈ Fin → ∀ 𝑛 ∈ ω ∃ 𝑥 ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑛 ) )