Metamath Proof Explorer

Theorem iundjiun

Description: Given a sequence E of sets, a sequence F of disjoint sets is built, such that the indexed union stays the same. As in the proof of Property 112C (d) of Fremlin1 p. 16. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses iundjiun.nph 
|- F/ n ph
iundjiun.z 
|- Z = ( ZZ>= ` N )
iundjiun.e 
|- ( ph -> E : Z --> V )
iundjiun.f 
|- F = ( n e. Z |-> ( ( E ` n ) \ U_ i e. ( N ..^ n ) ( E ` i ) ) )
Assertion iundjiun 
|- ( ph -> ( ( A. m e. Z U_ n e. ( N ... m ) ( F ` n ) = U_ n e. ( N ... m ) ( E ` n ) /\ U_ n e. Z ( F ` n ) = U_ n e. Z ( E ` n ) ) /\ Disj_ n e. Z ( F ` n ) ) )

Proof

Step Hyp Ref Expression
1 iundjiun.nph 
 |-  F/ n ph
2 iundjiun.z 
 |-  Z = ( ZZ>= ` N )
3 iundjiun.e 
 |-  ( ph -> E : Z --> V )
4 iundjiun.f 
 |-  F = ( n e. Z |-> ( ( E ` n ) \ U_ i e. ( N ..^ n ) ( E ` i ) ) )
5 eliun 
 |-  ( x e. U_ n e. ( N ... m ) ( F ` n ) <-> E. n e. ( N ... m ) x e. ( F ` n ) )
6 5 biimpi 
 |-  ( x e. U_ n e. ( N ... m ) ( F ` n ) -> E. n e. ( N ... m ) x e. ( F ` n ) )
7 6 adantl 
 |-  ( ( ph /\ x e. U_ n e. ( N ... m ) ( F ` n ) ) -> E. n e. ( N ... m ) x e. ( F ` n ) )
8 nfcv 
 |-  F/_ n x
9 nfiu1 
 |-  F/_ n U_ n e. ( N ... m ) ( E ` n )
10 8 9 nfel 
 |-  F/ n x e. U_ n e. ( N ... m ) ( E ` n )
11 simp2 
 |-  ( ( ph /\ n e. ( N ... m ) /\ x e. ( F ` n ) ) -> n e. ( N ... m ) )
12 simpl 
 |-  ( ( ph /\ n e. ( N ... m ) ) -> ph )
13 elfzuz 
 |-  ( n e. ( N ... m ) -> n e. ( ZZ>= ` N ) )
14 2 eqcomi 
 |-  ( ZZ>= ` N ) = Z
15 13 14 eleqtrdi 
 |-  ( n e. ( N ... m ) -> n e. Z )
16 15 adantl 
 |-  ( ( ph /\ n e. ( N ... m ) ) -> n e. Z )
17 simpr 
 |-  ( ( ph /\ n e. Z ) -> n e. Z )
18 3 ffvelrnda 
 |-  ( ( ph /\ n e. Z ) -> ( E ` n ) e. V )
19 difexg 
 |-  ( ( E ` n ) e. V -> ( ( E ` n ) \ U_ i e. ( N ..^ n ) ( E ` i ) ) e. _V )
20 18 19 syl 
 |-  ( ( ph /\ n e. Z ) -> ( ( E ` n ) \ U_ i e. ( N ..^ n ) ( E ` i ) ) e. _V )
21 4 fvmpt2 
 |-  ( ( n e. Z /\ ( ( E ` n ) \ U_ i e. ( N ..^ n ) ( E ` i ) ) e. _V ) -> ( F ` n ) = ( ( E ` n ) \ U_ i e. ( N ..^ n ) ( E ` i ) ) )
22 17 20 21 syl2anc 
 |-  ( ( ph /\ n e. Z ) -> ( F ` n ) = ( ( E ` n ) \ U_ i e. ( N ..^ n ) ( E ` i ) ) )
23 difssd 
 |-  ( ( ph /\ n e. Z ) -> ( ( E ` n ) \ U_ i e. ( N ..^ n ) ( E ` i ) ) C_ ( E ` n ) )
24 22 23 eqsstrd 
 |-  ( ( ph /\ n e. Z ) -> ( F ` n ) C_ ( E ` n ) )
25 12 16 24 syl2anc 
 |-  ( ( ph /\ n e. ( N ... m ) ) -> ( F ` n ) C_ ( E ` n ) )
26 25 3adant3 
 |-  ( ( ph /\ n e. ( N ... m ) /\ x e. ( F ` n ) ) -> ( F ` n ) C_ ( E ` n ) )
27 simp3 
 |-  ( ( ph /\ n e. ( N ... m ) /\ x e. ( F ` n ) ) -> x e. ( F ` n ) )
28 26 27 sseldd 
 |-  ( ( ph /\ n e. ( N ... m ) /\ x e. ( F ` n ) ) -> x e. ( E ` n ) )
29 rspe 
 |-  ( ( n e. ( N ... m ) /\ x e. ( E ` n ) ) -> E. n e. ( N ... m ) x e. ( E ` n ) )
30 11 28 29 syl2anc 
 |-  ( ( ph /\ n e. ( N ... m ) /\ x e. ( F ` n ) ) -> E. n e. ( N ... m ) x e. ( E ` n ) )
31 eliun 
 |-  ( x e. U_ n e. ( N ... m ) ( E ` n ) <-> E. n e. ( N ... m ) x e. ( E ` n ) )
32 30 31 sylibr 
 |-  ( ( ph /\ n e. ( N ... m ) /\ x e. ( F ` n ) ) -> x e. U_ n e. ( N ... m ) ( E ` n ) )
33 32 3exp 
 |-  ( ph -> ( n e. ( N ... m ) -> ( x e. ( F ` n ) -> x e. U_ n e. ( N ... m ) ( E ` n ) ) ) )
34 1 10 33 rexlimd 
 |-  ( ph -> ( E. n e. ( N ... m ) x e. ( F ` n ) -> x e. U_ n e. ( N ... m ) ( E ` n ) ) )
35 34 adantr 
 |-  ( ( ph /\ x e. U_ n e. ( N ... m ) ( F ` n ) ) -> ( E. n e. ( N ... m ) x e. ( F ` n ) -> x e. U_ n e. ( N ... m ) ( E ` n ) ) )
36 7 35 mpd 
 |-  ( ( ph /\ x e. U_ n e. ( N ... m ) ( F ` n ) ) -> x e. U_ n e. ( N ... m ) ( E ` n ) )
37 36 ralrimiva 
 |-  ( ph -> A. x e. U_ n e. ( N ... m ) ( F ` n ) x e. U_ n e. ( N ... m ) ( E ` n ) )
38 dfss3 
 |-  ( U_ n e. ( N ... m ) ( F ` n ) C_ U_ n e. ( N ... m ) ( E ` n ) <-> A. x e. U_ n e. ( N ... m ) ( F ` n ) x e. U_ n e. ( N ... m ) ( E ` n ) )
39 37 38 sylibr 
 |-  ( ph -> U_ n e. ( N ... m ) ( F ` n ) C_ U_ n e. ( N ... m ) ( E ` n ) )
40 fzssuz 
 |-  ( N ... m ) C_ ( ZZ>= ` N )
41 40 a1i 
 |-  ( x e. U_ n e. ( N ... m ) ( E ` n ) -> ( N ... m ) C_ ( ZZ>= ` N ) )
42 31 biimpi 
 |-  ( x e. U_ n e. ( N ... m ) ( E ` n ) -> E. n e. ( N ... m ) x e. ( E ` n ) )
43 nfv 
 |-  F/ n x e. ( E ` i )
44 fveq2 
 |-  ( n = i -> ( E ` n ) = ( E ` i ) )
45 44 eleq2d 
 |-  ( n = i -> ( x e. ( E ` n ) <-> x e. ( E ` i ) ) )
46 43 45 uzwo4 
 |-  ( ( ( N ... m ) C_ ( ZZ>= ` N ) /\ E. n e. ( N ... m ) x e. ( E ` n ) ) -> E. n e. ( N ... m ) ( x e. ( E ` n ) /\ A. i e. ( N ... m ) ( i < n -> -. x e. ( E ` i ) ) ) )
47 41 42 46 syl2anc 
 |-  ( x e. U_ n e. ( N ... m ) ( E ` n ) -> E. n e. ( N ... m ) ( x e. ( E ` n ) /\ A. i e. ( N ... m ) ( i < n -> -. x e. ( E ` i ) ) ) )
48 47 adantl 
 |-  ( ( ph /\ x e. U_ n e. ( N ... m ) ( E ` n ) ) -> E. n e. ( N ... m ) ( x e. ( E ` n ) /\ A. i e. ( N ... m ) ( i < n -> -. x e. ( E ` i ) ) ) )
49 simprl 
 |-  ( ( ( ph /\ n e. ( N ... m ) ) /\ ( x e. ( E ` n ) /\ A. i e. ( N ... m ) ( i < n -> -. x e. ( E ` i ) ) ) ) -> x e. ( E ` n ) )
50 nfv 
 |-  F/ i ( ph /\ n e. ( N ... m ) )
51 nfra1 
 |-  F/ i A. i e. ( N ... m ) ( i < n -> -. x e. ( E ` i ) )
52 50 51 nfan 
 |-  F/ i ( ( ph /\ n e. ( N ... m ) ) /\ A. i e. ( N ... m ) ( i < n -> -. x e. ( E ` i ) ) )
53 elfzoelz 
 |-  ( i e. ( N ..^ n ) -> i e. ZZ )
54 53 zred 
 |-  ( i e. ( N ..^ n ) -> i e. RR )
55 54 adantl 
 |-  ( ( n e. ( N ... m ) /\ i e. ( N ..^ n ) ) -> i e. RR )
56 elfzelz 
 |-  ( n e. ( N ... m ) -> n e. ZZ )
57 56 zred 
 |-  ( n e. ( N ... m ) -> n e. RR )
58 57 adantr 
 |-  ( ( n e. ( N ... m ) /\ i e. ( N ..^ n ) ) -> n e. RR )
59 1red 
 |-  ( ( n e. ( N ... m ) /\ i e. ( N ..^ n ) ) -> 1 e. RR )
60 58 59 resubcld 
 |-  ( ( n e. ( N ... m ) /\ i e. ( N ..^ n ) ) -> ( n - 1 ) e. RR )
61 elfzolem1 
 |-  ( i e. ( N ..^ n ) -> i <_ ( n - 1 ) )
62 61 adantl 
 |-  ( ( n e. ( N ... m ) /\ i e. ( N ..^ n ) ) -> i <_ ( n - 1 ) )
63 58 ltm1d 
 |-  ( ( n e. ( N ... m ) /\ i e. ( N ..^ n ) ) -> ( n - 1 ) < n )
64 55 60 58 62 63 lelttrd 
 |-  ( ( n e. ( N ... m ) /\ i e. ( N ..^ n ) ) -> i < n )
65 64 ad4ant24 
 |-  ( ( ( ( ph /\ n e. ( N ... m ) ) /\ A. i e. ( N ... m ) ( i < n -> -. x e. ( E ` i ) ) ) /\ i e. ( N ..^ n ) ) -> i < n )
66 simplr 
 |-  ( ( ( n e. ( N ... m ) /\ A. i e. ( N ... m ) ( i < n -> -. x e. ( E ` i ) ) ) /\ i e. ( N ..^ n ) ) -> A. i e. ( N ... m ) ( i < n -> -. x e. ( E ` i ) ) )
67 elfzel1 
 |-  ( n e. ( N ... m ) -> N e. ZZ )
68 67 adantr 
 |-  ( ( n e. ( N ... m ) /\ i e. ( N ..^ n ) ) -> N e. ZZ )
69 elfzel2 
 |-  ( n e. ( N ... m ) -> m e. ZZ )
70 69 adantr 
 |-  ( ( n e. ( N ... m ) /\ i e. ( N ..^ n ) ) -> m e. ZZ )
71 53 adantl 
 |-  ( ( n e. ( N ... m ) /\ i e. ( N ..^ n ) ) -> i e. ZZ )
72 68 70 71 3jca 
 |-  ( ( n e. ( N ... m ) /\ i e. ( N ..^ n ) ) -> ( N e. ZZ /\ m e. ZZ /\ i e. ZZ ) )
73 elfzole1 
 |-  ( i e. ( N ..^ n ) -> N <_ i )
74 73 adantl 
 |-  ( ( n e. ( N ... m ) /\ i e. ( N ..^ n ) ) -> N <_ i )
75 70 zred 
 |-  ( ( n e. ( N ... m ) /\ i e. ( N ..^ n ) ) -> m e. RR )
76 1red 
 |-  ( n e. ( N ... m ) -> 1 e. RR )
77 57 76 resubcld 
 |-  ( n e. ( N ... m ) -> ( n - 1 ) e. RR )
78 69 zred 
 |-  ( n e. ( N ... m ) -> m e. RR )
79 57 ltm1d 
 |-  ( n e. ( N ... m ) -> ( n - 1 ) < n )
80 elfzle2 
 |-  ( n e. ( N ... m ) -> n <_ m )
81 77 57 78 79 80 ltletrd 
 |-  ( n e. ( N ... m ) -> ( n - 1 ) < m )
82 81 adantr 
 |-  ( ( n e. ( N ... m ) /\ i e. ( N ..^ n ) ) -> ( n - 1 ) < m )
83 55 60 75 62 82 lelttrd 
 |-  ( ( n e. ( N ... m ) /\ i e. ( N ..^ n ) ) -> i < m )
84 55 75 83 ltled 
 |-  ( ( n e. ( N ... m ) /\ i e. ( N ..^ n ) ) -> i <_ m )
85 72 74 84 jca32 
 |-  ( ( n e. ( N ... m ) /\ i e. ( N ..^ n ) ) -> ( ( N e. ZZ /\ m e. ZZ /\ i e. ZZ ) /\ ( N <_ i /\ i <_ m ) ) )
86 elfz2 
 |-  ( i e. ( N ... m ) <-> ( ( N e. ZZ /\ m e. ZZ /\ i e. ZZ ) /\ ( N <_ i /\ i <_ m ) ) )
87 85 86 sylibr 
 |-  ( ( n e. ( N ... m ) /\ i e. ( N ..^ n ) ) -> i e. ( N ... m ) )
88 87 adantlr 
 |-  ( ( ( n e. ( N ... m ) /\ A. i e. ( N ... m ) ( i < n -> -. x e. ( E ` i ) ) ) /\ i e. ( N ..^ n ) ) -> i e. ( N ... m ) )
89 rspa 
 |-  ( ( A. i e. ( N ... m ) ( i < n -> -. x e. ( E ` i ) ) /\ i e. ( N ... m ) ) -> ( i < n -> -. x e. ( E ` i ) ) )
90 66 88 89 syl2anc 
 |-  ( ( ( n e. ( N ... m ) /\ A. i e. ( N ... m ) ( i < n -> -. x e. ( E ` i ) ) ) /\ i e. ( N ..^ n ) ) -> ( i < n -> -. x e. ( E ` i ) ) )
91 90 adantlll 
 |-  ( ( ( ( ph /\ n e. ( N ... m ) ) /\ A. i e. ( N ... m ) ( i < n -> -. x e. ( E ` i ) ) ) /\ i e. ( N ..^ n ) ) -> ( i < n -> -. x e. ( E ` i ) ) )
92 65 91 mpd 
 |-  ( ( ( ( ph /\ n e. ( N ... m ) ) /\ A. i e. ( N ... m ) ( i < n -> -. x e. ( E ` i ) ) ) /\ i e. ( N ..^ n ) ) -> -. x e. ( E ` i ) )
93 92 ex 
 |-  ( ( ( ph /\ n e. ( N ... m ) ) /\ A. i e. ( N ... m ) ( i < n -> -. x e. ( E ` i ) ) ) -> ( i e. ( N ..^ n ) -> -. x e. ( E ` i ) ) )
94 52 93 ralrimi 
 |-  ( ( ( ph /\ n e. ( N ... m ) ) /\ A. i e. ( N ... m ) ( i < n -> -. x e. ( E ` i ) ) ) -> A. i e. ( N ..^ n ) -. x e. ( E ` i ) )
95 ralnex 
 |-  ( A. i e. ( N ..^ n ) -. x e. ( E ` i ) <-> -. E. i e. ( N ..^ n ) x e. ( E ` i ) )
96 94 95 sylib 
 |-  ( ( ( ph /\ n e. ( N ... m ) ) /\ A. i e. ( N ... m ) ( i < n -> -. x e. ( E ` i ) ) ) -> -. E. i e. ( N ..^ n ) x e. ( E ` i ) )
97 eliun 
 |-  ( x e. U_ i e. ( N ..^ n ) ( E ` i ) <-> E. i e. ( N ..^ n ) x e. ( E ` i ) )
98 96 97 sylnibr 
 |-  ( ( ( ph /\ n e. ( N ... m ) ) /\ A. i e. ( N ... m ) ( i < n -> -. x e. ( E ` i ) ) ) -> -. x e. U_ i e. ( N ..^ n ) ( E ` i ) )
99 98 adantrl 
 |-  ( ( ( ph /\ n e. ( N ... m ) ) /\ ( x e. ( E ` n ) /\ A. i e. ( N ... m ) ( i < n -> -. x e. ( E ` i ) ) ) ) -> -. x e. U_ i e. ( N ..^ n ) ( E ` i ) )
100 49 99 eldifd 
 |-  ( ( ( ph /\ n e. ( N ... m ) ) /\ ( x e. ( E ` n ) /\ A. i e. ( N ... m ) ( i < n -> -. x e. ( E ` i ) ) ) ) -> x e. ( ( E ` n ) \ U_ i e. ( N ..^ n ) ( E ` i ) ) )
101 16 22 syldan 
 |-  ( ( ph /\ n e. ( N ... m ) ) -> ( F ` n ) = ( ( E ` n ) \ U_ i e. ( N ..^ n ) ( E ` i ) ) )
102 101 eqcomd 
 |-  ( ( ph /\ n e. ( N ... m ) ) -> ( ( E ` n ) \ U_ i e. ( N ..^ n ) ( E ` i ) ) = ( F ` n ) )
103 102 adantr 
 |-  ( ( ( ph /\ n e. ( N ... m ) ) /\ ( x e. ( E ` n ) /\ A. i e. ( N ... m ) ( i < n -> -. x e. ( E ` i ) ) ) ) -> ( ( E ` n ) \ U_ i e. ( N ..^ n ) ( E ` i ) ) = ( F ` n ) )
104 100 103 eleqtrd 
 |-  ( ( ( ph /\ n e. ( N ... m ) ) /\ ( x e. ( E ` n ) /\ A. i e. ( N ... m ) ( i < n -> -. x e. ( E ` i ) ) ) ) -> x e. ( F ` n ) )
105 104 ex 
 |-  ( ( ph /\ n e. ( N ... m ) ) -> ( ( x e. ( E ` n ) /\ A. i e. ( N ... m ) ( i < n -> -. x e. ( E ` i ) ) ) -> x e. ( F ` n ) ) )
106 105 ex 
 |-  ( ph -> ( n e. ( N ... m ) -> ( ( x e. ( E ` n ) /\ A. i e. ( N ... m ) ( i < n -> -. x e. ( E ` i ) ) ) -> x e. ( F ` n ) ) ) )
107 1 106 reximdai 
 |-  ( ph -> ( E. n e. ( N ... m ) ( x e. ( E ` n ) /\ A. i e. ( N ... m ) ( i < n -> -. x e. ( E ` i ) ) ) -> E. n e. ( N ... m ) x e. ( F ` n ) ) )
108 107 adantr 
 |-  ( ( ph /\ x e. U_ n e. ( N ... m ) ( E ` n ) ) -> ( E. n e. ( N ... m ) ( x e. ( E ` n ) /\ A. i e. ( N ... m ) ( i < n -> -. x e. ( E ` i ) ) ) -> E. n e. ( N ... m ) x e. ( F ` n ) ) )
109 48 108 mpd 
 |-  ( ( ph /\ x e. U_ n e. ( N ... m ) ( E ` n ) ) -> E. n e. ( N ... m ) x e. ( F ` n ) )
110 109 5 sylibr 
 |-  ( ( ph /\ x e. U_ n e. ( N ... m ) ( E ` n ) ) -> x e. U_ n e. ( N ... m ) ( F ` n ) )
111 39 110 eqelssd 
 |-  ( ph -> U_ n e. ( N ... m ) ( F ` n ) = U_ n e. ( N ... m ) ( E ` n ) )
112 111 ralrimivw 
 |-  ( ph -> A. m e. Z U_ n e. ( N ... m ) ( F ` n ) = U_ n e. ( N ... m ) ( E ` n ) )
113 2 iuneqfzuz 
 |-  ( A. m e. Z U_ n e. ( N ... m ) ( F ` n ) = U_ n e. ( N ... m ) ( E ` n ) -> U_ n e. Z ( F ` n ) = U_ n e. Z ( E ` n ) )
114 112 113 syl 
 |-  ( ph -> U_ n e. Z ( F ` n ) = U_ n e. Z ( E ` n ) )
115 fveq2 
 |-  ( n = m -> ( E ` n ) = ( E ` m ) )
116 oveq2 
 |-  ( n = m -> ( N ..^ n ) = ( N ..^ m ) )
117 116 iuneq1d 
 |-  ( n = m -> U_ i e. ( N ..^ n ) ( E ` i ) = U_ i e. ( N ..^ m ) ( E ` i ) )
118 115 117 difeq12d 
 |-  ( n = m -> ( ( E ` n ) \ U_ i e. ( N ..^ n ) ( E ` i ) ) = ( ( E ` m ) \ U_ i e. ( N ..^ m ) ( E ` i ) ) )
119 118 cbvmptv 
 |-  ( n e. Z |-> ( ( E ` n ) \ U_ i e. ( N ..^ n ) ( E ` i ) ) ) = ( m e. Z |-> ( ( E ` m ) \ U_ i e. ( N ..^ m ) ( E ` i ) ) )
120 4 119 eqtri 
 |-  F = ( m e. Z |-> ( ( E ` m ) \ U_ i e. ( N ..^ m ) ( E ` i ) ) )
121 simpllr 
 |-  ( ( ( ( ph /\ n e. Z ) /\ k e. Z ) /\ n < k ) -> n e. Z )
122 simplr 
 |-  ( ( ( ( ph /\ n e. Z ) /\ k e. Z ) /\ n < k ) -> k e. Z )
123 simpr 
 |-  ( ( ( ( ph /\ n e. Z ) /\ k e. Z ) /\ n < k ) -> n < k )
124 2 120 121 122 123 iundjiunlem 
 |-  ( ( ( ( ph /\ n e. Z ) /\ k e. Z ) /\ n < k ) -> ( ( F ` n ) i^i ( F ` k ) ) = (/) )
125 124 adantlr 
 |-  ( ( ( ( ( ph /\ n e. Z ) /\ k e. Z ) /\ -. n = k ) /\ n < k ) -> ( ( F ` n ) i^i ( F ` k ) ) = (/) )
126 simpll 
 |-  ( ( ( ( ( ph /\ n e. Z ) /\ k e. Z ) /\ -. n = k ) /\ -. n < k ) -> ( ( ph /\ n e. Z ) /\ k e. Z ) )
127 neqne 
 |-  ( -. n = k -> n =/= k )
128 id 
 |-  ( k e. Z -> k e. Z )
129 128 2 eleqtrdi 
 |-  ( k e. Z -> k e. ( ZZ>= ` N ) )
130 eluzelz 
 |-  ( k e. ( ZZ>= ` N ) -> k e. ZZ )
131 129 130 syl 
 |-  ( k e. Z -> k e. ZZ )
132 131 zred 
 |-  ( k e. Z -> k e. RR )
133 132 adantl 
 |-  ( ( n e. Z /\ k e. Z ) -> k e. RR )
134 133 ad2antrr 
 |-  ( ( ( ( n e. Z /\ k e. Z ) /\ n =/= k ) /\ -. n < k ) -> k e. RR )
135 id 
 |-  ( n e. Z -> n e. Z )
136 135 2 eleqtrdi 
 |-  ( n e. Z -> n e. ( ZZ>= ` N ) )
137 eluzelz 
 |-  ( n e. ( ZZ>= ` N ) -> n e. ZZ )
138 136 137 syl 
 |-  ( n e. Z -> n e. ZZ )
139 138 zred 
 |-  ( n e. Z -> n e. RR )
140 139 ad3antrrr 
 |-  ( ( ( ( n e. Z /\ k e. Z ) /\ n =/= k ) /\ -. n < k ) -> n e. RR )
141 simpr 
 |-  ( ( ( n e. Z /\ k e. Z ) /\ -. n < k ) -> -. n < k )
142 133 adantr 
 |-  ( ( ( n e. Z /\ k e. Z ) /\ -. n < k ) -> k e. RR )
143 139 ad2antrr 
 |-  ( ( ( n e. Z /\ k e. Z ) /\ -. n < k ) -> n e. RR )
144 142 143 lenltd 
 |-  ( ( ( n e. Z /\ k e. Z ) /\ -. n < k ) -> ( k <_ n <-> -. n < k ) )
145 141 144 mpbird 
 |-  ( ( ( n e. Z /\ k e. Z ) /\ -. n < k ) -> k <_ n )
146 145 adantlr 
 |-  ( ( ( ( n e. Z /\ k e. Z ) /\ n =/= k ) /\ -. n < k ) -> k <_ n )
147 simplr 
 |-  ( ( ( ( n e. Z /\ k e. Z ) /\ n =/= k ) /\ -. n < k ) -> n =/= k )
148 134 140 146 147 leneltd 
 |-  ( ( ( ( n e. Z /\ k e. Z ) /\ n =/= k ) /\ -. n < k ) -> k < n )
149 127 148 sylanl2 
 |-  ( ( ( ( n e. Z /\ k e. Z ) /\ -. n = k ) /\ -. n < k ) -> k < n )
150 149 ad5ant2345 
 |-  ( ( ( ( ( ph /\ n e. Z ) /\ k e. Z ) /\ -. n = k ) /\ -. n < k ) -> k < n )
151 anass 
 |-  ( ( ( ph /\ n e. Z ) /\ k e. Z ) <-> ( ph /\ ( n e. Z /\ k e. Z ) ) )
152 incom 
 |-  ( ( F ` n ) i^i ( F ` k ) ) = ( ( F ` k ) i^i ( F ` n ) )
153 152 a1i 
 |-  ( ( ( ph /\ ( n e. Z /\ k e. Z ) ) /\ k < n ) -> ( ( F ` n ) i^i ( F ` k ) ) = ( ( F ` k ) i^i ( F ` n ) ) )
154 simplrr 
 |-  ( ( ( ph /\ ( n e. Z /\ k e. Z ) ) /\ k < n ) -> k e. Z )
155 simplrl 
 |-  ( ( ( ph /\ ( n e. Z /\ k e. Z ) ) /\ k < n ) -> n e. Z )
156 simpr 
 |-  ( ( ( ph /\ ( n e. Z /\ k e. Z ) ) /\ k < n ) -> k < n )
157 2 120 154 155 156 iundjiunlem 
 |-  ( ( ( ph /\ ( n e. Z /\ k e. Z ) ) /\ k < n ) -> ( ( F ` k ) i^i ( F ` n ) ) = (/) )
158 153 157 eqtrd 
 |-  ( ( ( ph /\ ( n e. Z /\ k e. Z ) ) /\ k < n ) -> ( ( F ` n ) i^i ( F ` k ) ) = (/) )
159 151 158 sylanb 
 |-  ( ( ( ( ph /\ n e. Z ) /\ k e. Z ) /\ k < n ) -> ( ( F ` n ) i^i ( F ` k ) ) = (/) )
160 126 150 159 syl2anc 
 |-  ( ( ( ( ( ph /\ n e. Z ) /\ k e. Z ) /\ -. n = k ) /\ -. n < k ) -> ( ( F ` n ) i^i ( F ` k ) ) = (/) )
161 125 160 pm2.61dan 
 |-  ( ( ( ( ph /\ n e. Z ) /\ k e. Z ) /\ -. n = k ) -> ( ( F ` n ) i^i ( F ` k ) ) = (/) )
162 161 ex 
 |-  ( ( ( ph /\ n e. Z ) /\ k e. Z ) -> ( -. n = k -> ( ( F ` n ) i^i ( F ` k ) ) = (/) ) )
163 df-or 
 |-  ( ( n = k \/ ( ( F ` n ) i^i ( F ` k ) ) = (/) ) <-> ( -. n = k -> ( ( F ` n ) i^i ( F ` k ) ) = (/) ) )
164 162 163 sylibr 
 |-  ( ( ( ph /\ n e. Z ) /\ k e. Z ) -> ( n = k \/ ( ( F ` n ) i^i ( F ` k ) ) = (/) ) )
165 164 ralrimiva 
 |-  ( ( ph /\ n e. Z ) -> A. k e. Z ( n = k \/ ( ( F ` n ) i^i ( F ` k ) ) = (/) ) )
166 165 ex 
 |-  ( ph -> ( n e. Z -> A. k e. Z ( n = k \/ ( ( F ` n ) i^i ( F ` k ) ) = (/) ) ) )
167 1 166 ralrimi 
 |-  ( ph -> A. n e. Z A. k e. Z ( n = k \/ ( ( F ` n ) i^i ( F ` k ) ) = (/) ) )
168 nfcv 
 |-  F/_ m ( F ` n )
169 nfmpt1 
 |-  F/_ n ( n e. Z |-> ( ( E ` n ) \ U_ i e. ( N ..^ n ) ( E ` i ) ) )
170 4 169 nfcxfr 
 |-  F/_ n F
171 nfcv 
 |-  F/_ n m
172 170 171 nffv 
 |-  F/_ n ( F ` m )
173 fveq2 
 |-  ( n = m -> ( F ` n ) = ( F ` m ) )
174 168 172 173 cbvdisj 
 |-  ( Disj_ n e. Z ( F ` n ) <-> Disj_ m e. Z ( F ` m ) )
175 fveq2 
 |-  ( m = k -> ( F ` m ) = ( F ` k ) )
176 175 disjor 
 |-  ( Disj_ m e. Z ( F ` m ) <-> A. m e. Z A. k e. Z ( m = k \/ ( ( F ` m ) i^i ( F ` k ) ) = (/) ) )
177 nfcv 
 |-  F/_ n Z
178 nfv 
 |-  F/ n m = k
179 nfcv 
 |-  F/_ n k
180 170 179 nffv 
 |-  F/_ n ( F ` k )
181 172 180 nfin 
 |-  F/_ n ( ( F ` m ) i^i ( F ` k ) )
182 nfcv 
 |-  F/_ n (/)
183 181 182 nfeq 
 |-  F/ n ( ( F ` m ) i^i ( F ` k ) ) = (/)
184 178 183 nfor 
 |-  F/ n ( m = k \/ ( ( F ` m ) i^i ( F ` k ) ) = (/) )
185 177 184 nfralw 
 |-  F/ n A. k e. Z ( m = k \/ ( ( F ` m ) i^i ( F ` k ) ) = (/) )
186 nfv 
 |-  F/ m A. k e. Z ( n = k \/ ( ( F ` n ) i^i ( F ` k ) ) = (/) )
187 equequ1 
 |-  ( m = n -> ( m = k <-> n = k ) )
188 fveq2 
 |-  ( m = n -> ( F ` m ) = ( F ` n ) )
189 188 ineq1d 
 |-  ( m = n -> ( ( F ` m ) i^i ( F ` k ) ) = ( ( F ` n ) i^i ( F ` k ) ) )
190 189 eqeq1d 
 |-  ( m = n -> ( ( ( F ` m ) i^i ( F ` k ) ) = (/) <-> ( ( F ` n ) i^i ( F ` k ) ) = (/) ) )
191 187 190 orbi12d 
 |-  ( m = n -> ( ( m = k \/ ( ( F ` m ) i^i ( F ` k ) ) = (/) ) <-> ( n = k \/ ( ( F ` n ) i^i ( F ` k ) ) = (/) ) ) )
192 191 ralbidv 
 |-  ( m = n -> ( A. k e. Z ( m = k \/ ( ( F ` m ) i^i ( F ` k ) ) = (/) ) <-> A. k e. Z ( n = k \/ ( ( F ` n ) i^i ( F ` k ) ) = (/) ) ) )
193 185 186 192 cbvralw 
 |-  ( A. m e. Z A. k e. Z ( m = k \/ ( ( F ` m ) i^i ( F ` k ) ) = (/) ) <-> A. n e. Z A. k e. Z ( n = k \/ ( ( F ` n ) i^i ( F ` k ) ) = (/) ) )
194 174 176 193 3bitri 
 |-  ( Disj_ n e. Z ( F ` n ) <-> A. n e. Z A. k e. Z ( n = k \/ ( ( F ` n ) i^i ( F ` k ) ) = (/) ) )
195 167 194 sylibr 
 |-  ( ph -> Disj_ n e. Z ( F ` n ) )
196 112 114 195 jca31 
 |-  ( ph -> ( ( A. m e. Z U_ n e. ( N ... m ) ( F ` n ) = U_ n e. ( N ... m ) ( E ` n ) /\ U_ n e. Z ( F ` n ) = U_ n e. Z ( E ` n ) ) /\ Disj_ n e. Z ( F ` n ) ) )