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 ffvelrnd ( ( 𝜑 ∧ ¬ ( 𝑛 = 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 ffvelrnda ( ( 𝜑𝑘𝐴 ) → ( 𝐺𝑘 ) ∈ 𝑋 )
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 ffvelrnda ( ( 𝜑 ∧ ( 𝑚 − 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 𝑛 ∈ ℕ ( 𝑓𝑛 ) ) )