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 
|- ( ph -> A C_ NN )
nnfoctbdjlem.g 
|- ( ph -> G : A -1-1-onto-> X )
nnfoctbdjlem.dj 
|- ( ph -> Disj_ y e. X y )
nnfoctbdjlem.f 
|- F = ( n e. NN |-> if ( ( n = 1 \/ -. ( n - 1 ) e. A ) , (/) , ( G ` ( n - 1 ) ) ) )
Assertion nnfoctbdjlem 
|- ( ph -> E. f ( f : NN -onto-> ( X u. { (/) } ) /\ Disj_ n e. NN ( f ` n ) ) )

Proof

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