Metamath Proof Explorer

Theorem nnfoctbdjlem

Description: There exists a mapping from NN onto any (nonempty) countable set of disjoint sets, such that elements in the range of the map are disjoint. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses nnfoctbdjlem.a ⊢ ( 𝜑 → 𝐴 ⊆ ℕ )
nnfoctbdjlem.g ⊢ ( 𝜑 → 𝐺 : 𝐴 –1-1-onto→ 𝑋 )
nnfoctbdjlem.dj ⊢ ( 𝜑 → Disj 𝑦 ∈ 𝑋 𝑦 )
nnfoctbdjlem.f ⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ if ( ( 𝑛 = 1 ∨ ¬ ( 𝑛 − 1 ) ∈ 𝐴 ) , ∅ , ( 𝐺 ‘ ( 𝑛 − 1 ) ) ) )
Assertion nnfoctbdjlem ( 𝜑 → ∃ 𝑓 ( 𝑓 : ℕ –onto→ ( 𝑋 ∪ { ∅ } ) ∧ Disj 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ) )

Proof

Step Hyp Ref Expression
1 nnfoctbdjlem.a ⊢ ( 𝜑 → 𝐴 ⊆ ℕ )
2 nnfoctbdjlem.g ⊢ ( 𝜑 → 𝐺 : 𝐴 –1-1-onto→ 𝑋 )
3 nnfoctbdjlem.dj ⊢ ( 𝜑 → Disj 𝑦 ∈ 𝑋 𝑦 )
4 nnfoctbdjlem.f ⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ if ( ( 𝑛 = 1 ∨ ¬ ( 𝑛 − 1 ) ∈ 𝐴 ) , ∅ , ( 𝐺 ‘ ( 𝑛 − 1 ) ) ) )
5 iftrue ⊢ ( ( 𝑛 = 1 ∨ ¬ ( 𝑛 − 1 ) ∈ 𝐴 ) → if ( ( 𝑛 = 1 ∨ ¬ ( 𝑛 − 1 ) ∈ 𝐴 ) , ∅ , ( 𝐺 ‘ ( 𝑛 − 1 ) ) ) = ∅ )
6 5 adantl ⊢ ( ( 𝑛 ∈ ℕ ∧ ( 𝑛 = 1 ∨ ¬ ( 𝑛 − 1 ) ∈ 𝐴 ) ) → if ( ( 𝑛 = 1 ∨ ¬ ( 𝑛 − 1 ) ∈ 𝐴 ) , ∅ , ( 𝐺 ‘ ( 𝑛 − 1 ) ) ) = ∅ )
7 0ex ⊢ ∅ ∈ V
8 7 snid ⊢ ∅ ∈ { ∅ }
9 elun2 ⊢ ( ∅ ∈ { ∅ } → ∅ ∈ ( 𝑋 ∪ { ∅ } ) )
10 8 9 ax-mp ⊢ ∅ ∈ ( 𝑋 ∪ { ∅ } )
11 6 10 eqeltrdi ⊢ ( ( 𝑛 ∈ ℕ ∧ ( 𝑛 = 1 ∨ ¬ ( 𝑛 − 1 ) ∈ 𝐴 ) ) → if ( ( 𝑛 = 1 ∨ ¬ ( 𝑛 − 1 ) ∈ 𝐴 ) , ∅ , ( 𝐺 ‘ ( 𝑛 − 1 ) ) ) ∈ ( 𝑋 ∪ { ∅ } ) )
12 11 adantll ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑛 = 1 ∨ ¬ ( 𝑛 − 1 ) ∈ 𝐴 ) ) → if ( ( 𝑛 = 1 ∨ ¬ ( 𝑛 − 1 ) ∈ 𝐴 ) , ∅ , ( 𝐺 ‘ ( 𝑛 − 1 ) ) ) ∈ ( 𝑋 ∪ { ∅ } ) )
13 iffalse ⊢ ( ¬ ( 𝑛 = 1 ∨ ¬ ( 𝑛 − 1 ) ∈ 𝐴 ) → if ( ( 𝑛 = 1 ∨ ¬ ( 𝑛 − 1 ) ∈ 𝐴 ) , ∅ , ( 𝐺 ‘ ( 𝑛 − 1 ) ) ) = ( 𝐺 ‘ ( 𝑛 − 1 ) ) )
14 13 adantl ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ ¬ ( 𝑛 = 1 ∨ ¬ ( 𝑛 − 1 ) ∈ 𝐴 ) ) → if ( ( 𝑛 = 1 ∨ ¬ ( 𝑛 − 1 ) ∈ 𝐴 ) , ∅ , ( 𝐺 ‘ ( 𝑛 − 1 ) ) ) = ( 𝐺 ‘ ( 𝑛 − 1 ) ) )
15 f1of ⊢ ( 𝐺 : 𝐴 –1-1-onto→ 𝑋 → 𝐺 : 𝐴 ⟶ 𝑋 )
16 2 15 syl ⊢ ( 𝜑 → 𝐺 : 𝐴 ⟶ 𝑋 )
17 16 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝑛 = 1 ∨ ¬ ( 𝑛 − 1 ) ∈ 𝐴 ) ) → 𝐺 : 𝐴 ⟶ 𝑋 )
18 pm2.46 ⊢ ( ¬ ( 𝑛 = 1 ∨ ¬ ( 𝑛 − 1 ) ∈ 𝐴 ) → ¬ ¬ ( 𝑛 − 1 ) ∈ 𝐴 )
19 18 notnotrd ⊢ ( ¬ ( 𝑛 = 1 ∨ ¬ ( 𝑛 − 1 ) ∈ 𝐴 ) → ( 𝑛 − 1 ) ∈ 𝐴 )
20 19 adantl ⊢ ( ( 𝜑 ∧ ¬ ( 𝑛 = 1 ∨ ¬ ( 𝑛 − 1 ) ∈ 𝐴 ) ) → ( 𝑛 − 1 ) ∈ 𝐴 )
21 17 20 ffvelcdmd ⊢ ( ( 𝜑 ∧ ¬ ( 𝑛 = 1 ∨ ¬ ( 𝑛 − 1 ) ∈ 𝐴 ) ) → ( 𝐺 ‘ ( 𝑛 − 1 ) ) ∈ 𝑋 )
22 21 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ ¬ ( 𝑛 = 1 ∨ ¬ ( 𝑛 − 1 ) ∈ 𝐴 ) ) → ( 𝐺 ‘ ( 𝑛 − 1 ) ) ∈ 𝑋 )
23 elun1 ⊢ ( ( 𝐺 ‘ ( 𝑛 − 1 ) ) ∈ 𝑋 → ( 𝐺 ‘ ( 𝑛 − 1 ) ) ∈ ( 𝑋 ∪ { ∅ } ) )
24 22 23 syl ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ ¬ ( 𝑛 = 1 ∨ ¬ ( 𝑛 − 1 ) ∈ 𝐴 ) ) → ( 𝐺 ‘ ( 𝑛 − 1 ) ) ∈ ( 𝑋 ∪ { ∅ } ) )
25 14 24 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ ¬ ( 𝑛 = 1 ∨ ¬ ( 𝑛 − 1 ) ∈ 𝐴 ) ) → if ( ( 𝑛 = 1 ∨ ¬ ( 𝑛 − 1 ) ∈ 𝐴 ) , ∅ , ( 𝐺 ‘ ( 𝑛 − 1 ) ) ) ∈ ( 𝑋 ∪ { ∅ } ) )
26 12 25 pm2.61dan ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → if ( ( 𝑛 = 1 ∨ ¬ ( 𝑛 − 1 ) ∈ 𝐴 ) , ∅ , ( 𝐺 ‘ ( 𝑛 − 1 ) ) ) ∈ ( 𝑋 ∪ { ∅ } ) )
27 26 4 fmptd ⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ( 𝑋 ∪ { ∅ } ) )
28 simpr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) → 𝑦 ∈ 𝑋 )
29 f1ofo ⊢ ( 𝐺 : 𝐴 –1-1-onto→ 𝑋 → 𝐺 : 𝐴 –onto→ 𝑋 )
30 forn ⊢ ( 𝐺 : 𝐴 –onto→ 𝑋 → ran 𝐺 = 𝑋 )
31 2 29 30 3syl ⊢ ( 𝜑 → ran 𝐺 = 𝑋 )
32 31 eqcomd ⊢ ( 𝜑 → 𝑋 = ran 𝐺 )
33 32 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) → 𝑋 = ran 𝐺 )
34 28 33 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) → 𝑦 ∈ ran 𝐺 )
35 16 ffnd ⊢ ( 𝜑 → 𝐺 Fn 𝐴 )
36 fvelrnb ⊢ ( 𝐺 Fn 𝐴 → ( 𝑦 ∈ ran 𝐺 ↔ ∃ 𝑘 ∈ 𝐴 ( 𝐺 ‘ 𝑘 ) = 𝑦 ) )
37 35 36 syl ⊢ ( 𝜑 → ( 𝑦 ∈ ran 𝐺 ↔ ∃ 𝑘 ∈ 𝐴 ( 𝐺 ‘ 𝑘 ) = 𝑦 ) )
38 37 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑦 ∈ ran 𝐺 ↔ ∃ 𝑘 ∈ 𝐴 ( 𝐺 ‘ 𝑘 ) = 𝑦 ) )
39 34 38 mpbid ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) → ∃ 𝑘 ∈ 𝐴 ( 𝐺 ‘ 𝑘 ) = 𝑦 )
40 1 sselda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑘 ∈ ℕ )
41 40 peano2nnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝑘 + 1 ) ∈ ℕ )
42 41 3adant3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ∧ ( 𝐺 ‘ 𝑘 ) = 𝑦 ) → ( 𝑘 + 1 ) ∈ ℕ )
43 4 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐹 = ( 𝑛 ∈ ℕ ↦ if ( ( 𝑛 = 1 ∨ ¬ ( 𝑛 − 1 ) ∈ 𝐴 ) , ∅ , ( 𝐺 ‘ ( 𝑛 − 1 ) ) ) ) )
44 1red ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ 𝑛 = ( 𝑘 + 1 ) ) → 1 ∈ ℝ )
45 1red ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 1 ∈ ℝ )
46 40 nnrpd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑘 ∈ ℝ+ )
47 45 46 ltaddrp2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 1 < ( 𝑘 + 1 ) )
48 47 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ 𝑛 = ( 𝑘 + 1 ) ) → 1 < ( 𝑘 + 1 ) )
49 id ⊢ ( 𝑛 = ( 𝑘 + 1 ) → 𝑛 = ( 𝑘 + 1 ) )
50 49 eqcomd ⊢ ( 𝑛 = ( 𝑘 + 1 ) → ( 𝑘 + 1 ) = 𝑛 )
51 50 adantl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ 𝑛 = ( 𝑘 + 1 ) ) → ( 𝑘 + 1 ) = 𝑛 )
52 48 51 breqtrd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ 𝑛 = ( 𝑘 + 1 ) ) → 1 < 𝑛 )
53 44 52 gtned ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ 𝑛 = ( 𝑘 + 1 ) ) → 𝑛 ≠ 1 )
54 53 neneqd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ 𝑛 = ( 𝑘 + 1 ) ) → ¬ 𝑛 = 1 )
55 oveq1 ⊢ ( 𝑛 = ( 𝑘 + 1 ) → ( 𝑛 − 1 ) = ( ( 𝑘 + 1 ) − 1 ) )
56 40 nncnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑘 ∈ ℂ )
57 1cnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 1 ∈ ℂ )
58 56 57 pncand ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( ( 𝑘 + 1 ) − 1 ) = 𝑘 )
59 55 58 sylan9eqr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ 𝑛 = ( 𝑘 + 1 ) ) → ( 𝑛 − 1 ) = 𝑘 )
60 simplr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ 𝑛 = ( 𝑘 + 1 ) ) → 𝑘 ∈ 𝐴 )
61 59 60 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ 𝑛 = ( 𝑘 + 1 ) ) → ( 𝑛 − 1 ) ∈ 𝐴 )
62 61 notnotd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ 𝑛 = ( 𝑘 + 1 ) ) → ¬ ¬ ( 𝑛 − 1 ) ∈ 𝐴 )
63 ioran ⊢ ( ¬ ( 𝑛 = 1 ∨ ¬ ( 𝑛 − 1 ) ∈ 𝐴 ) ↔ ( ¬ 𝑛 = 1 ∧ ¬ ¬ ( 𝑛 − 1 ) ∈ 𝐴 ) )
64 54 62 63 sylanbrc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ 𝑛 = ( 𝑘 + 1 ) ) → ¬ ( 𝑛 = 1 ∨ ¬ ( 𝑛 − 1 ) ∈ 𝐴 ) )
65 64 iffalsed ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ 𝑛 = ( 𝑘 + 1 ) ) → if ( ( 𝑛 = 1 ∨ ¬ ( 𝑛 − 1 ) ∈ 𝐴 ) , ∅ , ( 𝐺 ‘ ( 𝑛 − 1 ) ) ) = ( 𝐺 ‘ ( 𝑛 − 1 ) ) )
66 59 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ 𝑛 = ( 𝑘 + 1 ) ) → ( 𝐺 ‘ ( 𝑛 − 1 ) ) = ( 𝐺 ‘ 𝑘 ) )
67 65 66 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ 𝑛 = ( 𝑘 + 1 ) ) → if ( ( 𝑛 = 1 ∨ ¬ ( 𝑛 − 1 ) ∈ 𝐴 ) , ∅ , ( 𝐺 ‘ ( 𝑛 − 1 ) ) ) = ( 𝐺 ‘ 𝑘 ) )
68 16 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑘 ) ∈ 𝑋 )
69 43 67 41 68 fvmptd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝐹 ‘ ( 𝑘 + 1 ) ) = ( 𝐺 ‘ 𝑘 ) )
70 69 3adant3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ∧ ( 𝐺 ‘ 𝑘 ) = 𝑦 ) → ( 𝐹 ‘ ( 𝑘 + 1 ) ) = ( 𝐺 ‘ 𝑘 ) )
71 simp3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ∧ ( 𝐺 ‘ 𝑘 ) = 𝑦 ) → ( 𝐺 ‘ 𝑘 ) = 𝑦 )
72 70 71 eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ∧ ( 𝐺 ‘ 𝑘 ) = 𝑦 ) → ( 𝐹 ‘ ( 𝑘 + 1 ) ) = 𝑦 )
73 fveq2 ⊢ ( 𝑚 = ( 𝑘 + 1 ) → ( 𝐹 ‘ 𝑚 ) = ( 𝐹 ‘ ( 𝑘 + 1 ) ) )
74 73 eqeq1d ⊢ ( 𝑚 = ( 𝑘 + 1 ) → ( ( 𝐹 ‘ 𝑚 ) = 𝑦 ↔ ( 𝐹 ‘ ( 𝑘 + 1 ) ) = 𝑦 ) )
75 74 rspcev ⊢ ( ( ( 𝑘 + 1 ) ∈ ℕ ∧ ( 𝐹 ‘ ( 𝑘 + 1 ) ) = 𝑦 ) → ∃ 𝑚 ∈ ℕ ( 𝐹 ‘ 𝑚 ) = 𝑦 )
76 42 72 75 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ∧ ( 𝐺 ‘ 𝑘 ) = 𝑦 ) → ∃ 𝑚 ∈ ℕ ( 𝐹 ‘ 𝑚 ) = 𝑦 )
77 76 3exp ⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 → ( ( 𝐺 ‘ 𝑘 ) = 𝑦 → ∃ 𝑚 ∈ ℕ ( 𝐹 ‘ 𝑚 ) = 𝑦 ) ) )
78 77 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑘 ∈ 𝐴 → ( ( 𝐺 ‘ 𝑘 ) = 𝑦 → ∃ 𝑚 ∈ ℕ ( 𝐹 ‘ 𝑚 ) = 𝑦 ) ) )
79 78 rexlimdv ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) → ( ∃ 𝑘 ∈ 𝐴 ( 𝐺 ‘ 𝑘 ) = 𝑦 → ∃ 𝑚 ∈ ℕ ( 𝐹 ‘ 𝑚 ) = 𝑦 ) )
80 39 79 mpd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) → ∃ 𝑚 ∈ ℕ ( 𝐹 ‘ 𝑚 ) = 𝑦 )
81 id ⊢ ( ( 𝐹 ‘ 𝑚 ) = 𝑦 → ( 𝐹 ‘ 𝑚 ) = 𝑦 )
82 81 eqcomd ⊢ ( ( 𝐹 ‘ 𝑚 ) = 𝑦 → 𝑦 = ( 𝐹 ‘ 𝑚 ) )
83 82 a1i ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑚 ∈ ℕ ) → ( ( 𝐹 ‘ 𝑚 ) = 𝑦 → 𝑦 = ( 𝐹 ‘ 𝑚 ) ) )
84 83 reximdva ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) → ( ∃ 𝑚 ∈ ℕ ( 𝐹 ‘ 𝑚 ) = 𝑦 → ∃ 𝑚 ∈ ℕ 𝑦 = ( 𝐹 ‘ 𝑚 ) ) )
85 80 84 mpd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) → ∃ 𝑚 ∈ ℕ 𝑦 = ( 𝐹 ‘ 𝑚 ) )
86 85 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 ∪ { ∅ } ) ) ∧ 𝑦 ∈ 𝑋 ) → ∃ 𝑚 ∈ ℕ 𝑦 = ( 𝐹 ‘ 𝑚 ) )
87 simpll ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 ∪ { ∅ } ) ) ∧ ¬ 𝑦 ∈ 𝑋 ) → 𝜑 )
88 elunnel1 ⊢ ( ( 𝑦 ∈ ( 𝑋 ∪ { ∅ } ) ∧ ¬ 𝑦 ∈ 𝑋 ) → 𝑦 ∈ { ∅ } )
89 elsni ⊢ ( 𝑦 ∈ { ∅ } → 𝑦 = ∅ )
90 88 89 syl ⊢ ( ( 𝑦 ∈ ( 𝑋 ∪ { ∅ } ) ∧ ¬ 𝑦 ∈ 𝑋 ) → 𝑦 = ∅ )
91 90 adantll ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 ∪ { ∅ } ) ) ∧ ¬ 𝑦 ∈ 𝑋 ) → 𝑦 = ∅ )
92 1nn ⊢ 1 ∈ ℕ
93 92 a1i ⊢ ( ( 𝜑 ∧ 𝑦 = ∅ ) → 1 ∈ ℕ )
94 5 orcs ⊢ ( 𝑛 = 1 → if ( ( 𝑛 = 1 ∨ ¬ ( 𝑛 − 1 ) ∈ 𝐴 ) , ∅ , ( 𝐺 ‘ ( 𝑛 − 1 ) ) ) = ∅ )
95 92 a1i ⊢ ( 𝜑 → 1 ∈ ℕ )
96 7 a1i ⊢ ( 𝜑 → ∅ ∈ V )
97 4 94 95 96 fvmptd3 ⊢ ( 𝜑 → ( 𝐹 ‘ 1 ) = ∅ )
98 97 adantr ⊢ ( ( 𝜑 ∧ 𝑦 = ∅ ) → ( 𝐹 ‘ 1 ) = ∅ )
99 id ⊢ ( 𝑦 = ∅ → 𝑦 = ∅ )
100 99 eqcomd ⊢ ( 𝑦 = ∅ → ∅ = 𝑦 )
101 100 adantl ⊢ ( ( 𝜑 ∧ 𝑦 = ∅ ) → ∅ = 𝑦 )
102 98 101 eqtr2d ⊢ ( ( 𝜑 ∧ 𝑦 = ∅ ) → 𝑦 = ( 𝐹 ‘ 1 ) )
103 fveq2 ⊢ ( 𝑚 = 1 → ( 𝐹 ‘ 𝑚 ) = ( 𝐹 ‘ 1 ) )
104 103 rspceeqv ⊢ ( ( 1 ∈ ℕ ∧ 𝑦 = ( 𝐹 ‘ 1 ) ) → ∃ 𝑚 ∈ ℕ 𝑦 = ( 𝐹 ‘ 𝑚 ) )
105 93 102 104 syl2anc ⊢ ( ( 𝜑 ∧ 𝑦 = ∅ ) → ∃ 𝑚 ∈ ℕ 𝑦 = ( 𝐹 ‘ 𝑚 ) )
106 87 91 105 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 ∪ { ∅ } ) ) ∧ ¬ 𝑦 ∈ 𝑋 ) → ∃ 𝑚 ∈ ℕ 𝑦 = ( 𝐹 ‘ 𝑚 ) )
107 86 106 pm2.61dan ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 ∪ { ∅ } ) ) → ∃ 𝑚 ∈ ℕ 𝑦 = ( 𝐹 ‘ 𝑚 ) )
108 107 ralrimiva ⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 𝑋 ∪ { ∅ } ) ∃ 𝑚 ∈ ℕ 𝑦 = ( 𝐹 ‘ 𝑚 ) )
109 dffo3 ⊢ ( 𝐹 : ℕ –onto→ ( 𝑋 ∪ { ∅ } ) ↔ ( 𝐹 : ℕ ⟶ ( 𝑋 ∪ { ∅ } ) ∧ ∀ 𝑦 ∈ ( 𝑋 ∪ { ∅ } ) ∃ 𝑚 ∈ ℕ 𝑦 = ( 𝐹 ‘ 𝑚 ) ) )
110 27 108 109 sylanbrc ⊢ ( 𝜑 → 𝐹 : ℕ –onto→ ( 𝑋 ∪ { ∅ } ) )
111 animorrl ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ ) ) ∧ 𝑛 = 𝑚 ) → ( 𝑛 = 𝑚 ∨ ( ( 𝐹 ‘ 𝑛 ) ∩ ( 𝐹 ‘ 𝑚 ) ) = ∅ ) )
112 6 7 eqeltrdi ⊢ ( ( 𝑛 ∈ ℕ ∧ ( 𝑛 = 1 ∨ ¬ ( 𝑛 − 1 ) ∈ 𝐴 ) ) → if ( ( 𝑛 = 1 ∨ ¬ ( 𝑛 − 1 ) ∈ 𝐴 ) , ∅ , ( 𝐺 ‘ ( 𝑛 − 1 ) ) ) ∈ V )
113 4 fvmpt2 ⊢ ( ( 𝑛 ∈ ℕ ∧ if ( ( 𝑛 = 1 ∨ ¬ ( 𝑛 − 1 ) ∈ 𝐴 ) , ∅ , ( 𝐺 ‘ ( 𝑛 − 1 ) ) ) ∈ V ) → ( 𝐹 ‘ 𝑛 ) = if ( ( 𝑛 = 1 ∨ ¬ ( 𝑛 − 1 ) ∈ 𝐴 ) , ∅ , ( 𝐺 ‘ ( 𝑛 − 1 ) ) ) )
114 112 113 syldan ⊢ ( ( 𝑛 ∈ ℕ ∧ ( 𝑛 = 1 ∨ ¬ ( 𝑛 − 1 ) ∈ 𝐴 ) ) → ( 𝐹 ‘ 𝑛 ) = if ( ( 𝑛 = 1 ∨ ¬ ( 𝑛 − 1 ) ∈ 𝐴 ) , ∅ , ( 𝐺 ‘ ( 𝑛 − 1 ) ) ) )
115 114 6 eqtrd ⊢ ( ( 𝑛 ∈ ℕ ∧ ( 𝑛 = 1 ∨ ¬ ( 𝑛 − 1 ) ∈ 𝐴 ) ) → ( 𝐹 ‘ 𝑛 ) = ∅ )
116 115 ineq1d ⊢ ( ( 𝑛 ∈ ℕ ∧ ( 𝑛 = 1 ∨ ¬ ( 𝑛 − 1 ) ∈ 𝐴 ) ) → ( ( 𝐹 ‘ 𝑛 ) ∩ ( 𝐹 ‘ 𝑚 ) ) = ( ∅ ∩ ( 𝐹 ‘ 𝑚 ) ) )
117 0in ⊢ ( ∅ ∩ ( 𝐹 ‘ 𝑚 ) ) = ∅
118 116 117 eqtrdi ⊢ ( ( 𝑛 ∈ ℕ ∧ ( 𝑛 = 1 ∨ ¬ ( 𝑛 − 1 ) ∈ 𝐴 ) ) → ( ( 𝐹 ‘ 𝑛 ) ∩ ( 𝐹 ‘ 𝑚 ) ) = ∅ )
119 118 adantlr ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑛 = 1 ∨ ¬ ( 𝑛 − 1 ) ∈ 𝐴 ) ) → ( ( 𝐹 ‘ 𝑛 ) ∩ ( 𝐹 ‘ 𝑚 ) ) = ∅ )
120 119 ad4ant24 ⊢ ( ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ ) ) ∧ 𝑛 ≠ 𝑚 ) ∧ ( 𝑛 = 1 ∨ ¬ ( 𝑛 − 1 ) ∈ 𝐴 ) ) → ( ( 𝐹 ‘ 𝑛 ) ∩ ( 𝐹 ‘ 𝑚 ) ) = ∅ )
121 eqeq1 ⊢ ( 𝑛 = 𝑚 → ( 𝑛 = 1 ↔ 𝑚 = 1 ) )
122 oveq1 ⊢ ( 𝑛 = 𝑚 → ( 𝑛 − 1 ) = ( 𝑚 − 1 ) )
123 122 eleq1d ⊢ ( 𝑛 = 𝑚 → ( ( 𝑛 − 1 ) ∈ 𝐴 ↔ ( 𝑚 − 1 ) ∈ 𝐴 ) )
124 123 notbid ⊢ ( 𝑛 = 𝑚 → ( ¬ ( 𝑛 − 1 ) ∈ 𝐴 ↔ ¬ ( 𝑚 − 1 ) ∈ 𝐴 ) )
125 121 124 orbi12d ⊢ ( 𝑛 = 𝑚 → ( ( 𝑛 = 1 ∨ ¬ ( 𝑛 − 1 ) ∈ 𝐴 ) ↔ ( 𝑚 = 1 ∨ ¬ ( 𝑚 − 1 ) ∈ 𝐴 ) ) )
126 122 fveq2d ⊢ ( 𝑛 = 𝑚 → ( 𝐺 ‘ ( 𝑛 − 1 ) ) = ( 𝐺 ‘ ( 𝑚 − 1 ) ) )
127 125 126 ifbieq2d ⊢ ( 𝑛 = 𝑚 → if ( ( 𝑛 = 1 ∨ ¬ ( 𝑛 − 1 ) ∈ 𝐴 ) , ∅ , ( 𝐺 ‘ ( 𝑛 − 1 ) ) ) = if ( ( 𝑚 = 1 ∨ ¬ ( 𝑚 − 1 ) ∈ 𝐴 ) , ∅ , ( 𝐺 ‘ ( 𝑚 − 1 ) ) ) )
128 simpl ⊢ ( ( 𝑚 ∈ ℕ ∧ ( 𝑚 = 1 ∨ ¬ ( 𝑚 − 1 ) ∈ 𝐴 ) ) → 𝑚 ∈ ℕ )
129 iftrue ⊢ ( ( 𝑚 = 1 ∨ ¬ ( 𝑚 − 1 ) ∈ 𝐴 ) → if ( ( 𝑚 = 1 ∨ ¬ ( 𝑚 − 1 ) ∈ 𝐴 ) , ∅ , ( 𝐺 ‘ ( 𝑚 − 1 ) ) ) = ∅ )
130 129 7 eqeltrdi ⊢ ( ( 𝑚 = 1 ∨ ¬ ( 𝑚 − 1 ) ∈ 𝐴 ) → if ( ( 𝑚 = 1 ∨ ¬ ( 𝑚 − 1 ) ∈ 𝐴 ) , ∅ , ( 𝐺 ‘ ( 𝑚 − 1 ) ) ) ∈ V )
131 130 adantl ⊢ ( ( 𝑚 ∈ ℕ ∧ ( 𝑚 = 1 ∨ ¬ ( 𝑚 − 1 ) ∈ 𝐴 ) ) → if ( ( 𝑚 = 1 ∨ ¬ ( 𝑚 − 1 ) ∈ 𝐴 ) , ∅ , ( 𝐺 ‘ ( 𝑚 − 1 ) ) ) ∈ V )
132 4 127 128 131 fvmptd3 ⊢ ( ( 𝑚 ∈ ℕ ∧ ( 𝑚 = 1 ∨ ¬ ( 𝑚 − 1 ) ∈ 𝐴 ) ) → ( 𝐹 ‘ 𝑚 ) = if ( ( 𝑚 = 1 ∨ ¬ ( 𝑚 − 1 ) ∈ 𝐴 ) , ∅ , ( 𝐺 ‘ ( 𝑚 − 1 ) ) ) )
133 129 adantl ⊢ ( ( 𝑚 ∈ ℕ ∧ ( 𝑚 = 1 ∨ ¬ ( 𝑚 − 1 ) ∈ 𝐴 ) ) → if ( ( 𝑚 = 1 ∨ ¬ ( 𝑚 − 1 ) ∈ 𝐴 ) , ∅ , ( 𝐺 ‘ ( 𝑚 − 1 ) ) ) = ∅ )
134 132 133 eqtrd ⊢ ( ( 𝑚 ∈ ℕ ∧ ( 𝑚 = 1 ∨ ¬ ( 𝑚 − 1 ) ∈ 𝐴 ) ) → ( 𝐹 ‘ 𝑚 ) = ∅ )
135 134 ineq2d ⊢ ( ( 𝑚 ∈ ℕ ∧ ( 𝑚 = 1 ∨ ¬ ( 𝑚 − 1 ) ∈ 𝐴 ) ) → ( ( 𝐹 ‘ 𝑛 ) ∩ ( 𝐹 ‘ 𝑚 ) ) = ( ( 𝐹 ‘ 𝑛 ) ∩ ∅ ) )
136 in0 ⊢ ( ( 𝐹 ‘ 𝑛 ) ∩ ∅ ) = ∅
137 135 136 eqtrdi ⊢ ( ( 𝑚 ∈ ℕ ∧ ( 𝑚 = 1 ∨ ¬ ( 𝑚 − 1 ) ∈ 𝐴 ) ) → ( ( 𝐹 ‘ 𝑛 ) ∩ ( 𝐹 ‘ 𝑚 ) ) = ∅ )
138 137 adantll ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 = 1 ∨ ¬ ( 𝑚 − 1 ) ∈ 𝐴 ) ) → ( ( 𝐹 ‘ 𝑛 ) ∩ ( 𝐹 ‘ 𝑚 ) ) = ∅ )
139 138 ad5ant25 ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ ) ) ∧ 𝑛 ≠ 𝑚 ) ∧ ¬ ( 𝑛 = 1 ∨ ¬ ( 𝑛 − 1 ) ∈ 𝐴 ) ) ∧ ( 𝑚 = 1 ∨ ¬ ( 𝑚 − 1 ) ∈ 𝐴 ) ) → ( ( 𝐹 ‘ 𝑛 ) ∩ ( 𝐹 ‘ 𝑚 ) ) = ∅ )
140 fvex ⊢ ( 𝐺 ‘ ( 𝑛 − 1 ) ) ∈ V
141 7 140 ifex ⊢ if ( ( 𝑛 = 1 ∨ ¬ ( 𝑛 − 1 ) ∈ 𝐴 ) , ∅ , ( 𝐺 ‘ ( 𝑛 − 1 ) ) ) ∈ V
142 141 113 mpan2 ⊢ ( 𝑛 ∈ ℕ → ( 𝐹 ‘ 𝑛 ) = if ( ( 𝑛 = 1 ∨ ¬ ( 𝑛 − 1 ) ∈ 𝐴 ) , ∅ , ( 𝐺 ‘ ( 𝑛 − 1 ) ) ) )
143 142 13 sylan9eq ⊢ ( ( 𝑛 ∈ ℕ ∧ ¬ ( 𝑛 = 1 ∨ ¬ ( 𝑛 − 1 ) ∈ 𝐴 ) ) → ( 𝐹 ‘ 𝑛 ) = ( 𝐺 ‘ ( 𝑛 − 1 ) ) )
144 143 adantlr ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ ) ∧ ¬ ( 𝑛 = 1 ∨ ¬ ( 𝑛 − 1 ) ∈ 𝐴 ) ) → ( 𝐹 ‘ 𝑛 ) = ( 𝐺 ‘ ( 𝑛 − 1 ) ) )
145 144 3adant3 ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ ) ∧ ¬ ( 𝑛 = 1 ∨ ¬ ( 𝑛 − 1 ) ∈ 𝐴 ) ∧ ¬ ( 𝑚 = 1 ∨ ¬ ( 𝑚 − 1 ) ∈ 𝐴 ) ) → ( 𝐹 ‘ 𝑛 ) = ( 𝐺 ‘ ( 𝑛 − 1 ) ) )
146 4 a1i ⊢ ( ( 𝑚 ∈ ℕ ∧ ¬ ( 𝑚 = 1 ∨ ¬ ( 𝑚 − 1 ) ∈ 𝐴 ) ) → 𝐹 = ( 𝑛 ∈ ℕ ↦ if ( ( 𝑛 = 1 ∨ ¬ ( 𝑛 − 1 ) ∈ 𝐴 ) , ∅ , ( 𝐺 ‘ ( 𝑛 − 1 ) ) ) ) )
147 127 adantl ⊢ ( ( ( 𝑚 ∈ ℕ ∧ ¬ ( 𝑚 = 1 ∨ ¬ ( 𝑚 − 1 ) ∈ 𝐴 ) ) ∧ 𝑛 = 𝑚 ) → if ( ( 𝑛 = 1 ∨ ¬ ( 𝑛 − 1 ) ∈ 𝐴 ) , ∅ , ( 𝐺 ‘ ( 𝑛 − 1 ) ) ) = if ( ( 𝑚 = 1 ∨ ¬ ( 𝑚 − 1 ) ∈ 𝐴 ) , ∅ , ( 𝐺 ‘ ( 𝑚 − 1 ) ) ) )
148 iffalse ⊢ ( ¬ ( 𝑚 = 1 ∨ ¬ ( 𝑚 − 1 ) ∈ 𝐴 ) → if ( ( 𝑚 = 1 ∨ ¬ ( 𝑚 − 1 ) ∈ 𝐴 ) , ∅ , ( 𝐺 ‘ ( 𝑚 − 1 ) ) ) = ( 𝐺 ‘ ( 𝑚 − 1 ) ) )
149 148 ad2antlr ⊢ ( ( ( 𝑚 ∈ ℕ ∧ ¬ ( 𝑚 = 1 ∨ ¬ ( 𝑚 − 1 ) ∈ 𝐴 ) ) ∧ 𝑛 = 𝑚 ) → if ( ( 𝑚 = 1 ∨ ¬ ( 𝑚 − 1 ) ∈ 𝐴 ) , ∅ , ( 𝐺 ‘ ( 𝑚 − 1 ) ) ) = ( 𝐺 ‘ ( 𝑚 − 1 ) ) )
150 147 149 eqtrd ⊢ ( ( ( 𝑚 ∈ ℕ ∧ ¬ ( 𝑚 = 1 ∨ ¬ ( 𝑚 − 1 ) ∈ 𝐴 ) ) ∧ 𝑛 = 𝑚 ) → if ( ( 𝑛 = 1 ∨ ¬ ( 𝑛 − 1 ) ∈ 𝐴 ) , ∅ , ( 𝐺 ‘ ( 𝑛 − 1 ) ) ) = ( 𝐺 ‘ ( 𝑚 − 1 ) ) )
151 simpl ⊢ ( ( 𝑚 ∈ ℕ ∧ ¬ ( 𝑚 = 1 ∨ ¬ ( 𝑚 − 1 ) ∈ 𝐴 ) ) → 𝑚 ∈ ℕ )
152 fvexd ⊢ ( ( 𝑚 ∈ ℕ ∧ ¬ ( 𝑚 = 1 ∨ ¬ ( 𝑚 − 1 ) ∈ 𝐴 ) ) → ( 𝐺 ‘ ( 𝑚 − 1 ) ) ∈ V )
153 146 150 151 152 fvmptd ⊢ ( ( 𝑚 ∈ ℕ ∧ ¬ ( 𝑚 = 1 ∨ ¬ ( 𝑚 − 1 ) ∈ 𝐴 ) ) → ( 𝐹 ‘ 𝑚 ) = ( 𝐺 ‘ ( 𝑚 − 1 ) ) )
154 153 adantll ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ ) ∧ ¬ ( 𝑚 = 1 ∨ ¬ ( 𝑚 − 1 ) ∈ 𝐴 ) ) → ( 𝐹 ‘ 𝑚 ) = ( 𝐺 ‘ ( 𝑚 − 1 ) ) )
155 154 3adant2 ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ ) ∧ ¬ ( 𝑛 = 1 ∨ ¬ ( 𝑛 − 1 ) ∈ 𝐴 ) ∧ ¬ ( 𝑚 = 1 ∨ ¬ ( 𝑚 − 1 ) ∈ 𝐴 ) ) → ( 𝐹 ‘ 𝑚 ) = ( 𝐺 ‘ ( 𝑚 − 1 ) ) )
156 145 155 ineq12d ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ ) ∧ ¬ ( 𝑛 = 1 ∨ ¬ ( 𝑛 − 1 ) ∈ 𝐴 ) ∧ ¬ ( 𝑚 = 1 ∨ ¬ ( 𝑚 − 1 ) ∈ 𝐴 ) ) → ( ( 𝐹 ‘ 𝑛 ) ∩ ( 𝐹 ‘ 𝑚 ) ) = ( ( 𝐺 ‘ ( 𝑛 − 1 ) ) ∩ ( 𝐺 ‘ ( 𝑚 − 1 ) ) ) )
157 156 ad5ant245 ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ ) ) ∧ 𝑛 ≠ 𝑚 ) ∧ ¬ ( 𝑛 = 1 ∨ ¬ ( 𝑛 − 1 ) ∈ 𝐴 ) ) ∧ ¬ ( 𝑚 = 1 ∨ ¬ ( 𝑚 − 1 ) ∈ 𝐴 ) ) → ( ( 𝐹 ‘ 𝑛 ) ∩ ( 𝐹 ‘ 𝑚 ) ) = ( ( 𝐺 ‘ ( 𝑛 − 1 ) ) ∩ ( 𝐺 ‘ ( 𝑚 − 1 ) ) ) )
158 19 ad2antlr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ ) ) ∧ 𝑛 ≠ 𝑚 ) ∧ ¬ ( 𝑛 = 1 ∨ ¬ ( 𝑛 − 1 ) ∈ 𝐴 ) ) ∧ ¬ ( 𝑚 = 1 ∨ ¬ ( 𝑚 − 1 ) ∈ 𝐴 ) ) → ( 𝑛 − 1 ) ∈ 𝐴 )
159 pm2.46 ⊢ ( ¬ ( 𝑚 = 1 ∨ ¬ ( 𝑚 − 1 ) ∈ 𝐴 ) → ¬ ¬ ( 𝑚 − 1 ) ∈ 𝐴 )
160 159 notnotrd ⊢ ( ¬ ( 𝑚 = 1 ∨ ¬ ( 𝑚 − 1 ) ∈ 𝐴 ) → ( 𝑚 − 1 ) ∈ 𝐴 )
161 160 adantl ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ ) ) ∧ 𝑛 ≠ 𝑚 ) ∧ ¬ ( 𝑛 = 1 ∨ ¬ ( 𝑛 − 1 ) ∈ 𝐴 ) ) ∧ ¬ ( 𝑚 = 1 ∨ ¬ ( 𝑚 − 1 ) ∈ 𝐴 ) ) → ( 𝑚 − 1 ) ∈ 𝐴 )
162 f1of1 ⊢ ( 𝐺 : 𝐴 –1-1-onto→ 𝑋 → 𝐺 : 𝐴 –1-1→ 𝑋 )
163 2 162 syl ⊢ ( 𝜑 → 𝐺 : 𝐴 –1-1→ 𝑋 )
164 dff14a ⊢ ( 𝐺 : 𝐴 –1-1→ 𝑋 ↔ ( 𝐺 : 𝐴 ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≠ 𝑦 → ( 𝐺 ‘ 𝑥 ) ≠ ( 𝐺 ‘ 𝑦 ) ) ) )
165 163 164 sylib ⊢ ( 𝜑 → ( 𝐺 : 𝐴 ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≠ 𝑦 → ( 𝐺 ‘ 𝑥 ) ≠ ( 𝐺 ‘ 𝑦 ) ) ) )
166 165 simprd ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≠ 𝑦 → ( 𝐺 ‘ 𝑥 ) ≠ ( 𝐺 ‘ 𝑦 ) ) )
167 166 adantr ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ ) ) → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≠ 𝑦 → ( 𝐺 ‘ 𝑥 ) ≠ ( 𝐺 ‘ 𝑦 ) ) )
168 167 ad3antrrr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ ) ) ∧ 𝑛 ≠ 𝑚 ) ∧ ¬ ( 𝑛 = 1 ∨ ¬ ( 𝑛 − 1 ) ∈ 𝐴 ) ) ∧ ¬ ( 𝑚 = 1 ∨ ¬ ( 𝑚 − 1 ) ∈ 𝐴 ) ) → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≠ 𝑦 → ( 𝐺 ‘ 𝑥 ) ≠ ( 𝐺 ‘ 𝑦 ) ) )
169 158 161 168 jca31 ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ ) ) ∧ 𝑛 ≠ 𝑚 ) ∧ ¬ ( 𝑛 = 1 ∨ ¬ ( 𝑛 − 1 ) ∈ 𝐴 ) ) ∧ ¬ ( 𝑚 = 1 ∨ ¬ ( 𝑚 − 1 ) ∈ 𝐴 ) ) → ( ( ( 𝑛 − 1 ) ∈ 𝐴 ∧ ( 𝑚 − 1 ) ∈ 𝐴 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≠ 𝑦 → ( 𝐺 ‘ 𝑥 ) ≠ ( 𝐺 ‘ 𝑦 ) ) ) )
170 nncn ⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℂ )
171 170 adantr ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ ) → 𝑛 ∈ ℂ )
172 171 ad2antlr ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ ) ) ∧ 𝑛 ≠ 𝑚 ) → 𝑛 ∈ ℂ )
173 nncn ⊢ ( 𝑚 ∈ ℕ → 𝑚 ∈ ℂ )
174 173 adantl ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ ) → 𝑚 ∈ ℂ )
175 174 ad2antlr ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ ) ) ∧ 𝑛 ≠ 𝑚 ) → 𝑚 ∈ ℂ )
176 1cnd ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ ) ) ∧ 𝑛 ≠ 𝑚 ) → 1 ∈ ℂ )
177 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ ) ) ∧ 𝑛 ≠ 𝑚 ) → 𝑛 ≠ 𝑚 )
178 172 175 176 177 subneintr2d ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ ) ) ∧ 𝑛 ≠ 𝑚 ) → ( 𝑛 − 1 ) ≠ ( 𝑚 − 1 ) )
179 178 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ ) ) ∧ 𝑛 ≠ 𝑚 ) ∧ ¬ ( 𝑛 = 1 ∨ ¬ ( 𝑛 − 1 ) ∈ 𝐴 ) ) ∧ ¬ ( 𝑚 = 1 ∨ ¬ ( 𝑚 − 1 ) ∈ 𝐴 ) ) → ( 𝑛 − 1 ) ≠ ( 𝑚 − 1 ) )
180 neeq1 ⊢ ( 𝑥 = ( 𝑛 − 1 ) → ( 𝑥 ≠ 𝑦 ↔ ( 𝑛 − 1 ) ≠ 𝑦 ) )
181 fveq2 ⊢ ( 𝑥 = ( 𝑛 − 1 ) → ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ ( 𝑛 − 1 ) ) )
182 181 neeq1d ⊢ ( 𝑥 = ( 𝑛 − 1 ) → ( ( 𝐺 ‘ 𝑥 ) ≠ ( 𝐺 ‘ 𝑦 ) ↔ ( 𝐺 ‘ ( 𝑛 − 1 ) ) ≠ ( 𝐺 ‘ 𝑦 ) ) )
183 180 182 imbi12d ⊢ ( 𝑥 = ( 𝑛 − 1 ) → ( ( 𝑥 ≠ 𝑦 → ( 𝐺 ‘ 𝑥 ) ≠ ( 𝐺 ‘ 𝑦 ) ) ↔ ( ( 𝑛 − 1 ) ≠ 𝑦 → ( 𝐺 ‘ ( 𝑛 − 1 ) ) ≠ ( 𝐺 ‘ 𝑦 ) ) ) )
184 neeq2 ⊢ ( 𝑦 = ( 𝑚 − 1 ) → ( ( 𝑛 − 1 ) ≠ 𝑦 ↔ ( 𝑛 − 1 ) ≠ ( 𝑚 − 1 ) ) )
185 fveq2 ⊢ ( 𝑦 = ( 𝑚 − 1 ) → ( 𝐺 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑚 − 1 ) ) )
186 185 neeq2d ⊢ ( 𝑦 = ( 𝑚 − 1 ) → ( ( 𝐺 ‘ ( 𝑛 − 1 ) ) ≠ ( 𝐺 ‘ 𝑦 ) ↔ ( 𝐺 ‘ ( 𝑛 − 1 ) ) ≠ ( 𝐺 ‘ ( 𝑚 − 1 ) ) ) )
187 184 186 imbi12d ⊢ ( 𝑦 = ( 𝑚 − 1 ) → ( ( ( 𝑛 − 1 ) ≠ 𝑦 → ( 𝐺 ‘ ( 𝑛 − 1 ) ) ≠ ( 𝐺 ‘ 𝑦 ) ) ↔ ( ( 𝑛 − 1 ) ≠ ( 𝑚 − 1 ) → ( 𝐺 ‘ ( 𝑛 − 1 ) ) ≠ ( 𝐺 ‘ ( 𝑚 − 1 ) ) ) ) )
188 183 187 rspc2va ⊢ ( ( ( ( 𝑛 − 1 ) ∈ 𝐴 ∧ ( 𝑚 − 1 ) ∈ 𝐴 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≠ 𝑦 → ( 𝐺 ‘ 𝑥 ) ≠ ( 𝐺 ‘ 𝑦 ) ) ) → ( ( 𝑛 − 1 ) ≠ ( 𝑚 − 1 ) → ( 𝐺 ‘ ( 𝑛 − 1 ) ) ≠ ( 𝐺 ‘ ( 𝑚 − 1 ) ) ) )
189 169 179 188 sylc ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ ) ) ∧ 𝑛 ≠ 𝑚 ) ∧ ¬ ( 𝑛 = 1 ∨ ¬ ( 𝑛 − 1 ) ∈ 𝐴 ) ) ∧ ¬ ( 𝑚 = 1 ∨ ¬ ( 𝑚 − 1 ) ∈ 𝐴 ) ) → ( 𝐺 ‘ ( 𝑛 − 1 ) ) ≠ ( 𝐺 ‘ ( 𝑚 − 1 ) ) )
190 189 neneqd ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ ) ) ∧ 𝑛 ≠ 𝑚 ) ∧ ¬ ( 𝑛 = 1 ∨ ¬ ( 𝑛 − 1 ) ∈ 𝐴 ) ) ∧ ¬ ( 𝑚 = 1 ∨ ¬ ( 𝑚 − 1 ) ∈ 𝐴 ) ) → ¬ ( 𝐺 ‘ ( 𝑛 − 1 ) ) = ( 𝐺 ‘ ( 𝑚 − 1 ) ) )
191 21 ad4ant13 ⊢ ( ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ ) ) ∧ ¬ ( 𝑛 = 1 ∨ ¬ ( 𝑛 − 1 ) ∈ 𝐴 ) ) ∧ ¬ ( 𝑚 = 1 ∨ ¬ ( 𝑚 − 1 ) ∈ 𝐴 ) ) → ( 𝐺 ‘ ( 𝑛 − 1 ) ) ∈ 𝑋 )
192 16 ffvelcdmda ⊢ ( ( 𝜑 ∧ ( 𝑚 − 1 ) ∈ 𝐴 ) → ( 𝐺 ‘ ( 𝑚 − 1 ) ) ∈ 𝑋 )
193 160 192 sylan2 ⊢ ( ( 𝜑 ∧ ¬ ( 𝑚 = 1 ∨ ¬ ( 𝑚 − 1 ) ∈ 𝐴 ) ) → ( 𝐺 ‘ ( 𝑚 − 1 ) ) ∈ 𝑋 )
194 193 ad4ant14 ⊢ ( ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ ) ) ∧ ¬ ( 𝑛 = 1 ∨ ¬ ( 𝑛 − 1 ) ∈ 𝐴 ) ) ∧ ¬ ( 𝑚 = 1 ∨ ¬ ( 𝑚 − 1 ) ∈ 𝐴 ) ) → ( 𝐺 ‘ ( 𝑚 − 1 ) ) ∈ 𝑋 )
195 id ⊢ ( 𝑦 = 𝑧 → 𝑦 = 𝑧 )
196 195 disjor ⊢ ( Disj 𝑦 ∈ 𝑋 𝑦 ↔ ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( 𝑦 = 𝑧 ∨ ( 𝑦 ∩ 𝑧 ) = ∅ ) )
197 3 196 sylib ⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( 𝑦 = 𝑧 ∨ ( 𝑦 ∩ 𝑧 ) = ∅ ) )
198 197 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ ) ) ∧ ¬ ( 𝑛 = 1 ∨ ¬ ( 𝑛 − 1 ) ∈ 𝐴 ) ) ∧ ¬ ( 𝑚 = 1 ∨ ¬ ( 𝑚 − 1 ) ∈ 𝐴 ) ) → ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( 𝑦 = 𝑧 ∨ ( 𝑦 ∩ 𝑧 ) = ∅ ) )
199 eqeq1 ⊢ ( 𝑦 = ( 𝐺 ‘ ( 𝑛 − 1 ) ) → ( 𝑦 = 𝑧 ↔ ( 𝐺 ‘ ( 𝑛 − 1 ) ) = 𝑧 ) )
200 ineq1 ⊢ ( 𝑦 = ( 𝐺 ‘ ( 𝑛 − 1 ) ) → ( 𝑦 ∩ 𝑧 ) = ( ( 𝐺 ‘ ( 𝑛 − 1 ) ) ∩ 𝑧 ) )
201 200 eqeq1d ⊢ ( 𝑦 = ( 𝐺 ‘ ( 𝑛 − 1 ) ) → ( ( 𝑦 ∩ 𝑧 ) = ∅ ↔ ( ( 𝐺 ‘ ( 𝑛 − 1 ) ) ∩ 𝑧 ) = ∅ ) )
202 199 201 orbi12d ⊢ ( 𝑦 = ( 𝐺 ‘ ( 𝑛 − 1 ) ) → ( ( 𝑦 = 𝑧 ∨ ( 𝑦 ∩ 𝑧 ) = ∅ ) ↔ ( ( 𝐺 ‘ ( 𝑛 − 1 ) ) = 𝑧 ∨ ( ( 𝐺 ‘ ( 𝑛 − 1 ) ) ∩ 𝑧 ) = ∅ ) ) )
203 eqeq2 ⊢ ( 𝑧 = ( 𝐺 ‘ ( 𝑚 − 1 ) ) → ( ( 𝐺 ‘ ( 𝑛 − 1 ) ) = 𝑧 ↔ ( 𝐺 ‘ ( 𝑛 − 1 ) ) = ( 𝐺 ‘ ( 𝑚 − 1 ) ) ) )
204 ineq2 ⊢ ( 𝑧 = ( 𝐺 ‘ ( 𝑚 − 1 ) ) → ( ( 𝐺 ‘ ( 𝑛 − 1 ) ) ∩ 𝑧 ) = ( ( 𝐺 ‘ ( 𝑛 − 1 ) ) ∩ ( 𝐺 ‘ ( 𝑚 − 1 ) ) ) )
205 204 eqeq1d ⊢ ( 𝑧 = ( 𝐺 ‘ ( 𝑚 − 1 ) ) → ( ( ( 𝐺 ‘ ( 𝑛 − 1 ) ) ∩ 𝑧 ) = ∅ ↔ ( ( 𝐺 ‘ ( 𝑛 − 1 ) ) ∩ ( 𝐺 ‘ ( 𝑚 − 1 ) ) ) = ∅ ) )
206 203 205 orbi12d ⊢ ( 𝑧 = ( 𝐺 ‘ ( 𝑚 − 1 ) ) → ( ( ( 𝐺 ‘ ( 𝑛 − 1 ) ) = 𝑧 ∨ ( ( 𝐺 ‘ ( 𝑛 − 1 ) ) ∩ 𝑧 ) = ∅ ) ↔ ( ( 𝐺 ‘ ( 𝑛 − 1 ) ) = ( 𝐺 ‘ ( 𝑚 − 1 ) ) ∨ ( ( 𝐺 ‘ ( 𝑛 − 1 ) ) ∩ ( 𝐺 ‘ ( 𝑚 − 1 ) ) ) = ∅ ) ) )
207 202 206 rspc2va ⊢ ( ( ( ( 𝐺 ‘ ( 𝑛 − 1 ) ) ∈ 𝑋 ∧ ( 𝐺 ‘ ( 𝑚 − 1 ) ) ∈ 𝑋 ) ∧ ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( 𝑦 = 𝑧 ∨ ( 𝑦 ∩ 𝑧 ) = ∅ ) ) → ( ( 𝐺 ‘ ( 𝑛 − 1 ) ) = ( 𝐺 ‘ ( 𝑚 − 1 ) ) ∨ ( ( 𝐺 ‘ ( 𝑛 − 1 ) ) ∩ ( 𝐺 ‘ ( 𝑚 − 1 ) ) ) = ∅ ) )
208 191 194 198 207 syl21anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ ) ) ∧ ¬ ( 𝑛 = 1 ∨ ¬ ( 𝑛 − 1 ) ∈ 𝐴 ) ) ∧ ¬ ( 𝑚 = 1 ∨ ¬ ( 𝑚 − 1 ) ∈ 𝐴 ) ) → ( ( 𝐺 ‘ ( 𝑛 − 1 ) ) = ( 𝐺 ‘ ( 𝑚 − 1 ) ) ∨ ( ( 𝐺 ‘ ( 𝑛 − 1 ) ) ∩ ( 𝐺 ‘ ( 𝑚 − 1 ) ) ) = ∅ ) )
209 208 adantllr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ ) ) ∧ 𝑛 ≠ 𝑚 ) ∧ ¬ ( 𝑛 = 1 ∨ ¬ ( 𝑛 − 1 ) ∈ 𝐴 ) ) ∧ ¬ ( 𝑚 = 1 ∨ ¬ ( 𝑚 − 1 ) ∈ 𝐴 ) ) → ( ( 𝐺 ‘ ( 𝑛 − 1 ) ) = ( 𝐺 ‘ ( 𝑚 − 1 ) ) ∨ ( ( 𝐺 ‘ ( 𝑛 − 1 ) ) ∩ ( 𝐺 ‘ ( 𝑚 − 1 ) ) ) = ∅ ) )
210 orel1 ⊢ ( ¬ ( 𝐺 ‘ ( 𝑛 − 1 ) ) = ( 𝐺 ‘ ( 𝑚 − 1 ) ) → ( ( ( 𝐺 ‘ ( 𝑛 − 1 ) ) = ( 𝐺 ‘ ( 𝑚 − 1 ) ) ∨ ( ( 𝐺 ‘ ( 𝑛 − 1 ) ) ∩ ( 𝐺 ‘ ( 𝑚 − 1 ) ) ) = ∅ ) → ( ( 𝐺 ‘ ( 𝑛 − 1 ) ) ∩ ( 𝐺 ‘ ( 𝑚 − 1 ) ) ) = ∅ ) )
211 190 209 210 sylc ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ ) ) ∧ 𝑛 ≠ 𝑚 ) ∧ ¬ ( 𝑛 = 1 ∨ ¬ ( 𝑛 − 1 ) ∈ 𝐴 ) ) ∧ ¬ ( 𝑚 = 1 ∨ ¬ ( 𝑚 − 1 ) ∈ 𝐴 ) ) → ( ( 𝐺 ‘ ( 𝑛 − 1 ) ) ∩ ( 𝐺 ‘ ( 𝑚 − 1 ) ) ) = ∅ )
212 157 211 eqtrd ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ ) ) ∧ 𝑛 ≠ 𝑚 ) ∧ ¬ ( 𝑛 = 1 ∨ ¬ ( 𝑛 − 1 ) ∈ 𝐴 ) ) ∧ ¬ ( 𝑚 = 1 ∨ ¬ ( 𝑚 − 1 ) ∈ 𝐴 ) ) → ( ( 𝐹 ‘ 𝑛 ) ∩ ( 𝐹 ‘ 𝑚 ) ) = ∅ )
213 139 212 pm2.61dan ⊢ ( ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ ) ) ∧ 𝑛 ≠ 𝑚 ) ∧ ¬ ( 𝑛 = 1 ∨ ¬ ( 𝑛 − 1 ) ∈ 𝐴 ) ) → ( ( 𝐹 ‘ 𝑛 ) ∩ ( 𝐹 ‘ 𝑚 ) ) = ∅ )
214 120 213 pm2.61dan ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ ) ) ∧ 𝑛 ≠ 𝑚 ) → ( ( 𝐹 ‘ 𝑛 ) ∩ ( 𝐹 ‘ 𝑚 ) ) = ∅ )
215 214 olcd ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ ) ) ∧ 𝑛 ≠ 𝑚 ) → ( 𝑛 = 𝑚 ∨ ( ( 𝐹 ‘ 𝑛 ) ∩ ( 𝐹 ‘ 𝑚 ) ) = ∅ ) )
216 111 215 pm2.61dane ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ ) ) → ( 𝑛 = 𝑚 ∨ ( ( 𝐹 ‘ 𝑛 ) ∩ ( 𝐹 ‘ 𝑚 ) ) = ∅ ) )
217 216 ralrimivva ⊢ ( 𝜑 → ∀ 𝑛 ∈ ℕ ∀ 𝑚 ∈ ℕ ( 𝑛 = 𝑚 ∨ ( ( 𝐹 ‘ 𝑛 ) ∩ ( 𝐹 ‘ 𝑚 ) ) = ∅ ) )
218 fveq2 ⊢ ( 𝑛 = 𝑚 → ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑚 ) )
219 218 disjor ⊢ ( Disj 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ↔ ∀ 𝑛 ∈ ℕ ∀ 𝑚 ∈ ℕ ( 𝑛 = 𝑚 ∨ ( ( 𝐹 ‘ 𝑛 ) ∩ ( 𝐹 ‘ 𝑚 ) ) = ∅ ) )
220 217 219 sylibr ⊢ ( 𝜑 → Disj 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) )
221 nnex ⊢ ℕ ∈ V
222 221 mptex ⊢ ( 𝑛 ∈ ℕ ↦ if ( ( 𝑛 = 1 ∨ ¬ ( 𝑛 − 1 ) ∈ 𝐴 ) , ∅ , ( 𝐺 ‘ ( 𝑛 − 1 ) ) ) ) ∈ V
223 4 222 eqeltri ⊢ 𝐹 ∈ V
224 foeq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 : ℕ –onto→ ( 𝑋 ∪ { ∅ } ) ↔ 𝐹 : ℕ –onto→ ( 𝑋 ∪ { ∅ } ) ) )
225 simpl ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑛 ∈ ℕ ) → 𝑓 = 𝐹 )
226 225 fveq1d ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑛 ∈ ℕ ) → ( 𝑓 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑛 ) )
227 226 disjeq2dv ⊢ ( 𝑓 = 𝐹 → ( Disj 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ↔ Disj 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ) )
228 224 227 anbi12d ⊢ ( 𝑓 = 𝐹 → ( ( 𝑓 : ℕ –onto→ ( 𝑋 ∪ { ∅ } ) ∧ Disj 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ) ↔ ( 𝐹 : ℕ –onto→ ( 𝑋 ∪ { ∅ } ) ∧ Disj 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ) ) )
229 223 228 spcev ⊢ ( ( 𝐹 : ℕ –onto→ ( 𝑋 ∪ { ∅ } ) ∧ Disj 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ) → ∃ 𝑓 ( 𝑓 : ℕ –onto→ ( 𝑋 ∪ { ∅ } ) ∧ Disj 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ) )
230 110 220 229 syl2anc ⊢ ( 𝜑 → ∃ 𝑓 ( 𝑓 : ℕ –onto→ ( 𝑋 ∪ { ∅ } ) ∧ Disj 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ) )