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