Metamath Proof Explorer


Theorem isinfOLD

Description: Obsolete version of isinf as of 2-Jan-2025. (Contributed by Mario Carneiro, 15-Jan-2013) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion isinfOLD ( ¬ 𝐴 ∈ 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 → ∀ 𝑛 ∈ ω ∃ 𝑥 ( 𝑥𝐴𝑥𝑛 ) )