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)

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