Metamath Proof Explorer

Theorem vitalilem3

Description: Lemma for vitali . (Contributed by Mario Carneiro, 16-Jun-2014)

Ref Expression
Hypotheses vitali.1 
|- .~ = { <. x , y >. | ( ( x e. ( 0 [,] 1 ) /\ y e. ( 0 [,] 1 ) ) /\ ( x - y ) e. QQ ) }
vitali.2 
|- S = ( ( 0 [,] 1 ) /. .~ )
vitali.3 
|- ( ph -> F Fn S )
vitali.4 
|- ( ph -> A. z e. S ( z =/= (/) -> ( F ` z ) e. z ) )
vitali.5 
|- ( ph -> G : NN -1-1-onto-> ( QQ i^i ( -u 1 [,] 1 ) ) )
vitali.6 
|- T = ( n e. NN |-> { s e. RR | ( s - ( G ` n ) ) e. ran F } )
vitali.7 
|- ( ph -> -. ran F e. ( ~P RR \ dom vol ) )
Assertion vitalilem3 
|- ( ph -> Disj_ m e. NN ( T ` m ) )

Proof

Step Hyp Ref Expression
1 vitali.1 
 |-  .~ = { <. x , y >. | ( ( x e. ( 0 [,] 1 ) /\ y e. ( 0 [,] 1 ) ) /\ ( x - y ) e. QQ ) }
2 vitali.2 
 |-  S = ( ( 0 [,] 1 ) /. .~ )
3 vitali.3 
 |-  ( ph -> F Fn S )
4 vitali.4 
 |-  ( ph -> A. z e. S ( z =/= (/) -> ( F ` z ) e. z ) )
5 vitali.5 
 |-  ( ph -> G : NN -1-1-onto-> ( QQ i^i ( -u 1 [,] 1 ) ) )
6 vitali.6 
 |-  T = ( n e. NN |-> { s e. RR | ( s - ( G ` n ) ) e. ran F } )
7 vitali.7 
 |-  ( ph -> -. ran F e. ( ~P RR \ dom vol ) )
8 simprlr 
 |-  ( ( ph /\ ( ( m e. NN /\ w e. ( T ` m ) ) /\ ( k e. NN /\ w e. ( T ` k ) ) ) ) -> w e. ( T ` m ) )
9 simprll 
 |-  ( ( ph /\ ( ( m e. NN /\ w e. ( T ` m ) ) /\ ( k e. NN /\ w e. ( T ` k ) ) ) ) -> m e. NN )
10 fveq2 
 |-  ( n = m -> ( G ` n ) = ( G ` m ) )
11 10 oveq2d 
 |-  ( n = m -> ( s - ( G ` n ) ) = ( s - ( G ` m ) ) )
12 11 eleq1d 
 |-  ( n = m -> ( ( s - ( G ` n ) ) e. ran F <-> ( s - ( G ` m ) ) e. ran F ) )
13 12 rabbidv 
 |-  ( n = m -> { s e. RR | ( s - ( G ` n ) ) e. ran F } = { s e. RR | ( s - ( G ` m ) ) e. ran F } )
14 reex 
 |-  RR e. _V
15 14 rabex 
 |-  { s e. RR | ( s - ( G ` m ) ) e. ran F } e. _V
16 13 6 15 fvmpt 
 |-  ( m e. NN -> ( T ` m ) = { s e. RR | ( s - ( G ` m ) ) e. ran F } )
17 9 16 syl 
 |-  ( ( ph /\ ( ( m e. NN /\ w e. ( T ` m ) ) /\ ( k e. NN /\ w e. ( T ` k ) ) ) ) -> ( T ` m ) = { s e. RR | ( s - ( G ` m ) ) e. ran F } )
18 8 17 eleqtrd 
 |-  ( ( ph /\ ( ( m e. NN /\ w e. ( T ` m ) ) /\ ( k e. NN /\ w e. ( T ` k ) ) ) ) -> w e. { s e. RR | ( s - ( G ` m ) ) e. ran F } )
19 oveq1 
 |-  ( s = w -> ( s - ( G ` m ) ) = ( w - ( G ` m ) ) )
20 19 eleq1d 
 |-  ( s = w -> ( ( s - ( G ` m ) ) e. ran F <-> ( w - ( G ` m ) ) e. ran F ) )
21 20 elrab 
 |-  ( w e. { s e. RR | ( s - ( G ` m ) ) e. ran F } <-> ( w e. RR /\ ( w - ( G ` m ) ) e. ran F ) )
22 18 21 sylib 
 |-  ( ( ph /\ ( ( m e. NN /\ w e. ( T ` m ) ) /\ ( k e. NN /\ w e. ( T ` k ) ) ) ) -> ( w e. RR /\ ( w - ( G ` m ) ) e. ran F ) )
23 22 simpld 
 |-  ( ( ph /\ ( ( m e. NN /\ w e. ( T ` m ) ) /\ ( k e. NN /\ w e. ( T ` k ) ) ) ) -> w e. RR )
24 23 recnd 
 |-  ( ( ph /\ ( ( m e. NN /\ w e. ( T ` m ) ) /\ ( k e. NN /\ w e. ( T ` k ) ) ) ) -> w e. CC )
25 f1of 
 |-  ( G : NN -1-1-onto-> ( QQ i^i ( -u 1 [,] 1 ) ) -> G : NN --> ( QQ i^i ( -u 1 [,] 1 ) ) )
26 5 25 syl 
 |-  ( ph -> G : NN --> ( QQ i^i ( -u 1 [,] 1 ) ) )
27 inss1 
 |-  ( QQ i^i ( -u 1 [,] 1 ) ) C_ QQ
28 fss 
 |-  ( ( G : NN --> ( QQ i^i ( -u 1 [,] 1 ) ) /\ ( QQ i^i ( -u 1 [,] 1 ) ) C_ QQ ) -> G : NN --> QQ )
29 26 27 28 sylancl 
 |-  ( ph -> G : NN --> QQ )
30 29 adantr 
 |-  ( ( ph /\ ( ( m e. NN /\ w e. ( T ` m ) ) /\ ( k e. NN /\ w e. ( T ` k ) ) ) ) -> G : NN --> QQ )
31 30 9 ffvelcdmd 
 |-  ( ( ph /\ ( ( m e. NN /\ w e. ( T ` m ) ) /\ ( k e. NN /\ w e. ( T ` k ) ) ) ) -> ( G ` m ) e. QQ )
32 qcn 
 |-  ( ( G ` m ) e. QQ -> ( G ` m ) e. CC )
33 31 32 syl 
 |-  ( ( ph /\ ( ( m e. NN /\ w e. ( T ` m ) ) /\ ( k e. NN /\ w e. ( T ` k ) ) ) ) -> ( G ` m ) e. CC )
34 simprrl 
 |-  ( ( ph /\ ( ( m e. NN /\ w e. ( T ` m ) ) /\ ( k e. NN /\ w e. ( T ` k ) ) ) ) -> k e. NN )
35 30 34 ffvelcdmd 
 |-  ( ( ph /\ ( ( m e. NN /\ w e. ( T ` m ) ) /\ ( k e. NN /\ w e. ( T ` k ) ) ) ) -> ( G ` k ) e. QQ )
36 qcn 
 |-  ( ( G ` k ) e. QQ -> ( G ` k ) e. CC )
37 35 36 syl 
 |-  ( ( ph /\ ( ( m e. NN /\ w e. ( T ` m ) ) /\ ( k e. NN /\ w e. ( T ` k ) ) ) ) -> ( G ` k ) e. CC )
38 1 vitalilem1 
 |-  .~ Er ( 0 [,] 1 )
39 38 a1i 
 |-  ( ( ph /\ ( ( m e. NN /\ w e. ( T ` m ) ) /\ ( k e. NN /\ w e. ( T ` k ) ) ) ) -> .~ Er ( 0 [,] 1 ) )
40 1 2 3 4 5 6 7 vitalilem2 
 |-  ( ph -> ( ran F C_ ( 0 [,] 1 ) /\ ( 0 [,] 1 ) C_ U_ m e. NN ( T ` m ) /\ U_ m e. NN ( T ` m ) C_ ( -u 1 [,] 2 ) ) )
41 40 simp1d 
 |-  ( ph -> ran F C_ ( 0 [,] 1 ) )
42 41 adantr 
 |-  ( ( ph /\ ( ( m e. NN /\ w e. ( T ` m ) ) /\ ( k e. NN /\ w e. ( T ` k ) ) ) ) -> ran F C_ ( 0 [,] 1 ) )
43 22 simprd 
 |-  ( ( ph /\ ( ( m e. NN /\ w e. ( T ` m ) ) /\ ( k e. NN /\ w e. ( T ` k ) ) ) ) -> ( w - ( G ` m ) ) e. ran F )
44 42 43 sseldd 
 |-  ( ( ph /\ ( ( m e. NN /\ w e. ( T ` m ) ) /\ ( k e. NN /\ w e. ( T ` k ) ) ) ) -> ( w - ( G ` m ) ) e. ( 0 [,] 1 ) )
45 simprrr 
 |-  ( ( ph /\ ( ( m e. NN /\ w e. ( T ` m ) ) /\ ( k e. NN /\ w e. ( T ` k ) ) ) ) -> w e. ( T ` k ) )
46 fveq2 
 |-  ( n = k -> ( G ` n ) = ( G ` k ) )
47 46 oveq2d 
 |-  ( n = k -> ( s - ( G ` n ) ) = ( s - ( G ` k ) ) )
48 47 eleq1d 
 |-  ( n = k -> ( ( s - ( G ` n ) ) e. ran F <-> ( s - ( G ` k ) ) e. ran F ) )
49 48 rabbidv 
 |-  ( n = k -> { s e. RR | ( s - ( G ` n ) ) e. ran F } = { s e. RR | ( s - ( G ` k ) ) e. ran F } )
50 14 rabex 
 |-  { s e. RR | ( s - ( G ` k ) ) e. ran F } e. _V
51 49 6 50 fvmpt 
 |-  ( k e. NN -> ( T ` k ) = { s e. RR | ( s - ( G ` k ) ) e. ran F } )
52 34 51 syl 
 |-  ( ( ph /\ ( ( m e. NN /\ w e. ( T ` m ) ) /\ ( k e. NN /\ w e. ( T ` k ) ) ) ) -> ( T ` k ) = { s e. RR | ( s - ( G ` k ) ) e. ran F } )
53 45 52 eleqtrd 
 |-  ( ( ph /\ ( ( m e. NN /\ w e. ( T ` m ) ) /\ ( k e. NN /\ w e. ( T ` k ) ) ) ) -> w e. { s e. RR | ( s - ( G ` k ) ) e. ran F } )
54 oveq1 
 |-  ( s = w -> ( s - ( G ` k ) ) = ( w - ( G ` k ) ) )
55 54 eleq1d 
 |-  ( s = w -> ( ( s - ( G ` k ) ) e. ran F <-> ( w - ( G ` k ) ) e. ran F ) )
56 55 elrab 
 |-  ( w e. { s e. RR | ( s - ( G ` k ) ) e. ran F } <-> ( w e. RR /\ ( w - ( G ` k ) ) e. ran F ) )
57 53 56 sylib 
 |-  ( ( ph /\ ( ( m e. NN /\ w e. ( T ` m ) ) /\ ( k e. NN /\ w e. ( T ` k ) ) ) ) -> ( w e. RR /\ ( w - ( G ` k ) ) e. ran F ) )
58 57 simprd 
 |-  ( ( ph /\ ( ( m e. NN /\ w e. ( T ` m ) ) /\ ( k e. NN /\ w e. ( T ` k ) ) ) ) -> ( w - ( G ` k ) ) e. ran F )
59 42 58 sseldd 
 |-  ( ( ph /\ ( ( m e. NN /\ w e. ( T ` m ) ) /\ ( k e. NN /\ w e. ( T ` k ) ) ) ) -> ( w - ( G ` k ) ) e. ( 0 [,] 1 ) )
60 24 33 37 nnncan1d 
 |-  ( ( ph /\ ( ( m e. NN /\ w e. ( T ` m ) ) /\ ( k e. NN /\ w e. ( T ` k ) ) ) ) -> ( ( w - ( G ` m ) ) - ( w - ( G ` k ) ) ) = ( ( G ` k ) - ( G ` m ) ) )
61 qsubcl 
 |-  ( ( ( G ` k ) e. QQ /\ ( G ` m ) e. QQ ) -> ( ( G ` k ) - ( G ` m ) ) e. QQ )
62 35 31 61 syl2anc 
 |-  ( ( ph /\ ( ( m e. NN /\ w e. ( T ` m ) ) /\ ( k e. NN /\ w e. ( T ` k ) ) ) ) -> ( ( G ` k ) - ( G ` m ) ) e. QQ )
63 60 62 eqeltrd 
 |-  ( ( ph /\ ( ( m e. NN /\ w e. ( T ` m ) ) /\ ( k e. NN /\ w e. ( T ` k ) ) ) ) -> ( ( w - ( G ` m ) ) - ( w - ( G ` k ) ) ) e. QQ )
64 oveq12 
 |-  ( ( x = ( w - ( G ` m ) ) /\ y = ( w - ( G ` k ) ) ) -> ( x - y ) = ( ( w - ( G ` m ) ) - ( w - ( G ` k ) ) ) )
65 64 eleq1d 
 |-  ( ( x = ( w - ( G ` m ) ) /\ y = ( w - ( G ` k ) ) ) -> ( ( x - y ) e. QQ <-> ( ( w - ( G ` m ) ) - ( w - ( G ` k ) ) ) e. QQ ) )
66 65 1 brab2a 
 |-  ( ( w - ( G ` m ) ) .~ ( w - ( G ` k ) ) <-> ( ( ( w - ( G ` m ) ) e. ( 0 [,] 1 ) /\ ( w - ( G ` k ) ) e. ( 0 [,] 1 ) ) /\ ( ( w - ( G ` m ) ) - ( w - ( G ` k ) ) ) e. QQ ) )
67 44 59 63 66 syl21anbrc 
 |-  ( ( ph /\ ( ( m e. NN /\ w e. ( T ` m ) ) /\ ( k e. NN /\ w e. ( T ` k ) ) ) ) -> ( w - ( G ` m ) ) .~ ( w - ( G ` k ) ) )
68 39 67 erthi 
 |-  ( ( ph /\ ( ( m e. NN /\ w e. ( T ` m ) ) /\ ( k e. NN /\ w e. ( T ` k ) ) ) ) -> [ ( w - ( G ` m ) ) ] .~ = [ ( w - ( G ` k ) ) ] .~ )
69 68 fveq2d 
 |-  ( ( ph /\ ( ( m e. NN /\ w e. ( T ` m ) ) /\ ( k e. NN /\ w e. ( T ` k ) ) ) ) -> ( F ` [ ( w - ( G ` m ) ) ] .~ ) = ( F ` [ ( w - ( G ` k ) ) ] .~ ) )
70 eceq1 
 |-  ( z = ( w - ( G ` m ) ) -> [ z ] .~ = [ ( w - ( G ` m ) ) ] .~ )
71 70 fveq2d 
 |-  ( z = ( w - ( G ` m ) ) -> ( F ` [ z ] .~ ) = ( F ` [ ( w - ( G ` m ) ) ] .~ ) )
72 id 
 |-  ( z = ( w - ( G ` m ) ) -> z = ( w - ( G ` m ) ) )
73 71 72 eqeq12d 
 |-  ( z = ( w - ( G ` m ) ) -> ( ( F ` [ z ] .~ ) = z <-> ( F ` [ ( w - ( G ` m ) ) ] .~ ) = ( w - ( G ` m ) ) ) )
74 fveq2 
 |-  ( [ v ] .~ = w -> ( F ` [ v ] .~ ) = ( F ` w ) )
75 74 eceq1d 
 |-  ( [ v ] .~ = w -> [ ( F ` [ v ] .~ ) ] .~ = [ ( F ` w ) ] .~ )
76 75 fveq2d 
 |-  ( [ v ] .~ = w -> ( F ` [ ( F ` [ v ] .~ ) ] .~ ) = ( F ` [ ( F ` w ) ] .~ ) )
77 76 74 eqeq12d 
 |-  ( [ v ] .~ = w -> ( ( F ` [ ( F ` [ v ] .~ ) ] .~ ) = ( F ` [ v ] .~ ) <-> ( F ` [ ( F ` w ) ] .~ ) = ( F ` w ) ) )
78 38 a1i 
 |-  ( ( ph /\ v e. ( 0 [,] 1 ) ) -> .~ Er ( 0 [,] 1 ) )
79 erdm 
 |-  ( .~ Er ( 0 [,] 1 ) -> dom .~ = ( 0 [,] 1 ) )
80 38 79 ax-mp 
 |-  dom .~ = ( 0 [,] 1 )
81 80 eleq2i 
 |-  ( v e. dom .~ <-> v e. ( 0 [,] 1 ) )
82 ecdmn0 
 |-  ( v e. dom .~ <-> [ v ] .~ =/= (/) )
83 81 82 bitr3i 
 |-  ( v e. ( 0 [,] 1 ) <-> [ v ] .~ =/= (/) )
84 83 bilani 
 |-  ( ( ph /\ v e. ( 0 [,] 1 ) ) -> [ v ] .~ =/= (/) )
85 neeq1 
 |-  ( z = [ v ] .~ -> ( z =/= (/) <-> [ v ] .~ =/= (/) ) )
86 fveq2 
 |-  ( z = [ v ] .~ -> ( F ` z ) = ( F ` [ v ] .~ ) )
87 id 
 |-  ( z = [ v ] .~ -> z = [ v ] .~ )
88 86 87 eleq12d 
 |-  ( z = [ v ] .~ -> ( ( F ` z ) e. z <-> ( F ` [ v ] .~ ) e. [ v ] .~ ) )
89 85 88 imbi12d 
 |-  ( z = [ v ] .~ -> ( ( z =/= (/) -> ( F ` z ) e. z ) <-> ( [ v ] .~ =/= (/) -> ( F ` [ v ] .~ ) e. [ v ] .~ ) ) )
90 4 adantr 
 |-  ( ( ph /\ v e. ( 0 [,] 1 ) ) -> A. z e. S ( z =/= (/) -> ( F ` z ) e. z ) )
91 ovex 
 |-  ( 0 [,] 1 ) e. _V
92 erex 
 |-  ( .~ Er ( 0 [,] 1 ) -> ( ( 0 [,] 1 ) e. _V -> .~ e. _V ) )
93 38 91 92 mp2 
 |-  .~ e. _V
94 93 ecelqsi 
 |-  ( v e. ( 0 [,] 1 ) -> [ v ] .~ e. ( ( 0 [,] 1 ) /. .~ ) )
95 94 2 eleqtrrdi 
 |-  ( v e. ( 0 [,] 1 ) -> [ v ] .~ e. S )
96 95 adantl 
 |-  ( ( ph /\ v e. ( 0 [,] 1 ) ) -> [ v ] .~ e. S )
97 89 90 96 rspcdva 
 |-  ( ( ph /\ v e. ( 0 [,] 1 ) ) -> ( [ v ] .~ =/= (/) -> ( F ` [ v ] .~ ) e. [ v ] .~ ) )
98 84 97 mpd 
 |-  ( ( ph /\ v e. ( 0 [,] 1 ) ) -> ( F ` [ v ] .~ ) e. [ v ] .~ )
99 fvex 
 |-  ( F ` [ v ] .~ ) e. _V
100 vex 
 |-  v e. _V
101 99 100 elec 
 |-  ( ( F ` [ v ] .~ ) e. [ v ] .~ <-> v .~ ( F ` [ v ] .~ ) )
102 98 101 sylib 
 |-  ( ( ph /\ v e. ( 0 [,] 1 ) ) -> v .~ ( F ` [ v ] .~ ) )
103 78 102 erthi 
 |-  ( ( ph /\ v e. ( 0 [,] 1 ) ) -> [ v ] .~ = [ ( F ` [ v ] .~ ) ] .~ )
104 103 eqcomd 
 |-  ( ( ph /\ v e. ( 0 [,] 1 ) ) -> [ ( F ` [ v ] .~ ) ] .~ = [ v ] .~ )
105 104 fveq2d 
 |-  ( ( ph /\ v e. ( 0 [,] 1 ) ) -> ( F ` [ ( F ` [ v ] .~ ) ] .~ ) = ( F ` [ v ] .~ ) )
106 2 77 105 ectocld 
 |-  ( ( ph /\ w e. S ) -> ( F ` [ ( F ` w ) ] .~ ) = ( F ` w ) )
107 106 ralrimiva 
 |-  ( ph -> A. w e. S ( F ` [ ( F ` w ) ] .~ ) = ( F ` w ) )
108 eceq1 
 |-  ( z = ( F ` w ) -> [ z ] .~ = [ ( F ` w ) ] .~ )
109 108 fveq2d 
 |-  ( z = ( F ` w ) -> ( F ` [ z ] .~ ) = ( F ` [ ( F ` w ) ] .~ ) )
110 id 
 |-  ( z = ( F ` w ) -> z = ( F ` w ) )
111 109 110 eqeq12d 
 |-  ( z = ( F ` w ) -> ( ( F ` [ z ] .~ ) = z <-> ( F ` [ ( F ` w ) ] .~ ) = ( F ` w ) ) )
112 111 ralrn 
 |-  ( F Fn S -> ( A. z e. ran F ( F ` [ z ] .~ ) = z <-> A. w e. S ( F ` [ ( F ` w ) ] .~ ) = ( F ` w ) ) )
113 3 112 syl 
 |-  ( ph -> ( A. z e. ran F ( F ` [ z ] .~ ) = z <-> A. w e. S ( F ` [ ( F ` w ) ] .~ ) = ( F ` w ) ) )
114 107 113 mpbird 
 |-  ( ph -> A. z e. ran F ( F ` [ z ] .~ ) = z )
115 114 adantr 
 |-  ( ( ph /\ ( ( m e. NN /\ w e. ( T ` m ) ) /\ ( k e. NN /\ w e. ( T ` k ) ) ) ) -> A. z e. ran F ( F ` [ z ] .~ ) = z )
116 73 115 43 rspcdva 
 |-  ( ( ph /\ ( ( m e. NN /\ w e. ( T ` m ) ) /\ ( k e. NN /\ w e. ( T ` k ) ) ) ) -> ( F ` [ ( w - ( G ` m ) ) ] .~ ) = ( w - ( G ` m ) ) )
117 eceq1 
 |-  ( z = ( w - ( G ` k ) ) -> [ z ] .~ = [ ( w - ( G ` k ) ) ] .~ )
118 117 fveq2d 
 |-  ( z = ( w - ( G ` k ) ) -> ( F ` [ z ] .~ ) = ( F ` [ ( w - ( G ` k ) ) ] .~ ) )
119 id 
 |-  ( z = ( w - ( G ` k ) ) -> z = ( w - ( G ` k ) ) )
120 118 119 eqeq12d 
 |-  ( z = ( w - ( G ` k ) ) -> ( ( F ` [ z ] .~ ) = z <-> ( F ` [ ( w - ( G ` k ) ) ] .~ ) = ( w - ( G ` k ) ) ) )
121 120 115 58 rspcdva 
 |-  ( ( ph /\ ( ( m e. NN /\ w e. ( T ` m ) ) /\ ( k e. NN /\ w e. ( T ` k ) ) ) ) -> ( F ` [ ( w - ( G ` k ) ) ] .~ ) = ( w - ( G ` k ) ) )
122 69 116 121 3eqtr3d 
 |-  ( ( ph /\ ( ( m e. NN /\ w e. ( T ` m ) ) /\ ( k e. NN /\ w e. ( T ` k ) ) ) ) -> ( w - ( G ` m ) ) = ( w - ( G ` k ) ) )
123 24 33 37 122 subcand 
 |-  ( ( ph /\ ( ( m e. NN /\ w e. ( T ` m ) ) /\ ( k e. NN /\ w e. ( T ` k ) ) ) ) -> ( G ` m ) = ( G ` k ) )
124 5 adantr 
 |-  ( ( ph /\ ( ( m e. NN /\ w e. ( T ` m ) ) /\ ( k e. NN /\ w e. ( T ` k ) ) ) ) -> G : NN -1-1-onto-> ( QQ i^i ( -u 1 [,] 1 ) ) )
125 f1of1 
 |-  ( G : NN -1-1-onto-> ( QQ i^i ( -u 1 [,] 1 ) ) -> G : NN -1-1-> ( QQ i^i ( -u 1 [,] 1 ) ) )
126 124 125 syl 
 |-  ( ( ph /\ ( ( m e. NN /\ w e. ( T ` m ) ) /\ ( k e. NN /\ w e. ( T ` k ) ) ) ) -> G : NN -1-1-> ( QQ i^i ( -u 1 [,] 1 ) ) )
127 f1fveq 
 |-  ( ( G : NN -1-1-> ( QQ i^i ( -u 1 [,] 1 ) ) /\ ( m e. NN /\ k e. NN ) ) -> ( ( G ` m ) = ( G ` k ) <-> m = k ) )
128 126 9 34 127 syl12anc 
 |-  ( ( ph /\ ( ( m e. NN /\ w e. ( T ` m ) ) /\ ( k e. NN /\ w e. ( T ` k ) ) ) ) -> ( ( G ` m ) = ( G ` k ) <-> m = k ) )
129 123 128 mpbid 
 |-  ( ( ph /\ ( ( m e. NN /\ w e. ( T ` m ) ) /\ ( k e. NN /\ w e. ( T ` k ) ) ) ) -> m = k )
130 129 ex 
 |-  ( ph -> ( ( ( m e. NN /\ w e. ( T ` m ) ) /\ ( k e. NN /\ w e. ( T ` k ) ) ) -> m = k ) )
131 130 alrimivv 
 |-  ( ph -> A. m A. k ( ( ( m e. NN /\ w e. ( T ` m ) ) /\ ( k e. NN /\ w e. ( T ` k ) ) ) -> m = k ) )
132 eleq1w 
 |-  ( m = k -> ( m e. NN <-> k e. NN ) )
133 fveq2 
 |-  ( m = k -> ( T ` m ) = ( T ` k ) )
134 133 eleq2d 
 |-  ( m = k -> ( w e. ( T ` m ) <-> w e. ( T ` k ) ) )
135 132 134 anbi12d 
 |-  ( m = k -> ( ( m e. NN /\ w e. ( T ` m ) ) <-> ( k e. NN /\ w e. ( T ` k ) ) ) )
136 135 mo4 
 |-  ( E* m ( m e. NN /\ w e. ( T ` m ) ) <-> A. m A. k ( ( ( m e. NN /\ w e. ( T ` m ) ) /\ ( k e. NN /\ w e. ( T ` k ) ) ) -> m = k ) )
137 131 136 sylibr 
 |-  ( ph -> E* m ( m e. NN /\ w e. ( T ` m ) ) )
138 137 alrimiv 
 |-  ( ph -> A. w E* m ( m e. NN /\ w e. ( T ` m ) ) )
139 dfdisj2 
 |-  ( Disj_ m e. NN ( T ` m ) <-> A. w E* m ( m e. NN /\ w e. ( T ` m ) ) )
140 138 139 sylibr 
 |-  ( ph -> Disj_ m e. NN ( T ` m ) )