Metamath Proof Explorer

Theorem heiborlem3

Description: Lemma for heibor . Using countable choice ax-cc , we have fixed in advance a collection of finite 2 ^ -u n nets ( Fn ) for X (note that an r -net is a set of points in X whose r -balls cover X ). The set G is the subset of these points whose corresponding balls have no finite subcover (i.e. in the set K ). If the theorem was false, then X would be in K , and so some ball at each level would also be in K . But we can say more than this; given a ball ( y B n ) on level n , since level n + 1 covers the space and thus also ( y B n ) , using heiborlem1 there is a ball on the next level whose intersection with ( y B n ) also has no finite subcover. Now since the set G is a countable union of finite sets, it is countable (which needs ax-cc via iunctb ), and so we can apply ax-cc to G directly to get a function from G to itself, which points from each ball in K to a ball on the next level in K , and such that the intersection between these balls is also in K . (Contributed by Jeff Madsen, 18-Jan-2014)

Ref Expression
Hypotheses heibor.1 
|- J = ( MetOpen ` D )
heibor.3 
|- K = { u | -. E. v e. ( ~P U i^i Fin ) u C_ U. v }
heibor.4 
|- G = { <. y , n >. | ( n e. NN0 /\ y e. ( F ` n ) /\ ( y B n ) e. K ) }
heibor.5 
|- B = ( z e. X , m e. NN0 |-> ( z ( ball ` D ) ( 1 / ( 2 ^ m ) ) ) )
heibor.6 
|- ( ph -> D e. ( CMet ` X ) )
heibor.7 
|- ( ph -> F : NN0 --> ( ~P X i^i Fin ) )
heibor.8 
|- ( ph -> A. n e. NN0 X = U_ y e. ( F ` n ) ( y B n ) )
Assertion heiborlem3 
|- ( ph -> E. g A. x e. G ( ( g ` x ) G ( ( 2nd ` x ) + 1 ) /\ ( ( B ` x ) i^i ( ( g ` x ) B ( ( 2nd ` x ) + 1 ) ) ) e. K ) )

Proof

Step Hyp Ref Expression
1 heibor.1 
 |-  J = ( MetOpen ` D )
2 heibor.3 
 |-  K = { u | -. E. v e. ( ~P U i^i Fin ) u C_ U. v }
3 heibor.4 
 |-  G = { <. y , n >. | ( n e. NN0 /\ y e. ( F ` n ) /\ ( y B n ) e. K ) }
4 heibor.5 
 |-  B = ( z e. X , m e. NN0 |-> ( z ( ball ` D ) ( 1 / ( 2 ^ m ) ) ) )
5 heibor.6 
 |-  ( ph -> D e. ( CMet ` X ) )
6 heibor.7 
 |-  ( ph -> F : NN0 --> ( ~P X i^i Fin ) )
7 heibor.8 
 |-  ( ph -> A. n e. NN0 X = U_ y e. ( F ` n ) ( y B n ) )
8 nn0ex 
 |-  NN0 e. _V
9 fvex 
 |-  ( F ` t ) e. _V
10 vsnex 
 |-  { t } e. _V
11 9 10 xpex 
 |-  ( ( F ` t ) X. { t } ) e. _V
12 8 11 iunex 
 |-  U_ t e. NN0 ( ( F ` t ) X. { t } ) e. _V
13 3 relopabiv 
 |-  Rel G
14 1st2nd 
 |-  ( ( Rel G /\ x e. G ) -> x = <. ( 1st ` x ) , ( 2nd ` x ) >. )
15 13 14 mpan 
 |-  ( x e. G -> x = <. ( 1st ` x ) , ( 2nd ` x ) >. )
16 15 eleq1d 
 |-  ( x e. G -> ( x e. G <-> <. ( 1st ` x ) , ( 2nd ` x ) >. e. G ) )
17 df-br 
 |-  ( ( 1st ` x ) G ( 2nd ` x ) <-> <. ( 1st ` x ) , ( 2nd ` x ) >. e. G )
18 16 17 bitr4di 
 |-  ( x e. G -> ( x e. G <-> ( 1st ` x ) G ( 2nd ` x ) ) )
19 fvex 
 |-  ( 1st ` x ) e. _V
20 fvex 
 |-  ( 2nd ` x ) e. _V
21 1 2 3 19 20 heiborlem2 
 |-  ( ( 1st ` x ) G ( 2nd ` x ) <-> ( ( 2nd ` x ) e. NN0 /\ ( 1st ` x ) e. ( F ` ( 2nd ` x ) ) /\ ( ( 1st ` x ) B ( 2nd ` x ) ) e. K ) )
22 18 21 bitrdi 
 |-  ( x e. G -> ( x e. G <-> ( ( 2nd ` x ) e. NN0 /\ ( 1st ` x ) e. ( F ` ( 2nd ` x ) ) /\ ( ( 1st ` x ) B ( 2nd ` x ) ) e. K ) ) )
23 22 ibi 
 |-  ( x e. G -> ( ( 2nd ` x ) e. NN0 /\ ( 1st ` x ) e. ( F ` ( 2nd ` x ) ) /\ ( ( 1st ` x ) B ( 2nd ` x ) ) e. K ) )
24 20 snid 
 |-  ( 2nd ` x ) e. { ( 2nd ` x ) }
25 opelxp 
 |-  ( <. ( 1st ` x ) , ( 2nd ` x ) >. e. ( ( F ` ( 2nd ` x ) ) X. { ( 2nd ` x ) } ) <-> ( ( 1st ` x ) e. ( F ` ( 2nd ` x ) ) /\ ( 2nd ` x ) e. { ( 2nd ` x ) } ) )
26 24 25 mpbiran2 
 |-  ( <. ( 1st ` x ) , ( 2nd ` x ) >. e. ( ( F ` ( 2nd ` x ) ) X. { ( 2nd ` x ) } ) <-> ( 1st ` x ) e. ( F ` ( 2nd ` x ) ) )
27 fveq2 
 |-  ( t = ( 2nd ` x ) -> ( F ` t ) = ( F ` ( 2nd ` x ) ) )
28 sneq 
 |-  ( t = ( 2nd ` x ) -> { t } = { ( 2nd ` x ) } )
29 27 28 xpeq12d 
 |-  ( t = ( 2nd ` x ) -> ( ( F ` t ) X. { t } ) = ( ( F ` ( 2nd ` x ) ) X. { ( 2nd ` x ) } ) )
30 29 eleq2d 
 |-  ( t = ( 2nd ` x ) -> ( <. ( 1st ` x ) , ( 2nd ` x ) >. e. ( ( F ` t ) X. { t } ) <-> <. ( 1st ` x ) , ( 2nd ` x ) >. e. ( ( F ` ( 2nd ` x ) ) X. { ( 2nd ` x ) } ) ) )
31 30 rspcev 
 |-  ( ( ( 2nd ` x ) e. NN0 /\ <. ( 1st ` x ) , ( 2nd ` x ) >. e. ( ( F ` ( 2nd ` x ) ) X. { ( 2nd ` x ) } ) ) -> E. t e. NN0 <. ( 1st ` x ) , ( 2nd ` x ) >. e. ( ( F ` t ) X. { t } ) )
32 26 31 sylan2br 
 |-  ( ( ( 2nd ` x ) e. NN0 /\ ( 1st ` x ) e. ( F ` ( 2nd ` x ) ) ) -> E. t e. NN0 <. ( 1st ` x ) , ( 2nd ` x ) >. e. ( ( F ` t ) X. { t } ) )
33 eliun 
 |-  ( <. ( 1st ` x ) , ( 2nd ` x ) >. e. U_ t e. NN0 ( ( F ` t ) X. { t } ) <-> E. t e. NN0 <. ( 1st ` x ) , ( 2nd ` x ) >. e. ( ( F ` t ) X. { t } ) )
34 32 33 sylibr 
 |-  ( ( ( 2nd ` x ) e. NN0 /\ ( 1st ` x ) e. ( F ` ( 2nd ` x ) ) ) -> <. ( 1st ` x ) , ( 2nd ` x ) >. e. U_ t e. NN0 ( ( F ` t ) X. { t } ) )
35 34 3adant3 
 |-  ( ( ( 2nd ` x ) e. NN0 /\ ( 1st ` x ) e. ( F ` ( 2nd ` x ) ) /\ ( ( 1st ` x ) B ( 2nd ` x ) ) e. K ) -> <. ( 1st ` x ) , ( 2nd ` x ) >. e. U_ t e. NN0 ( ( F ` t ) X. { t } ) )
36 23 35 syl 
 |-  ( x e. G -> <. ( 1st ` x ) , ( 2nd ` x ) >. e. U_ t e. NN0 ( ( F ` t ) X. { t } ) )
37 15 36 eqeltrd 
 |-  ( x e. G -> x e. U_ t e. NN0 ( ( F ` t ) X. { t } ) )
38 37 ssriv 
 |-  G C_ U_ t e. NN0 ( ( F ` t ) X. { t } )
39 ssdomg 
 |-  ( U_ t e. NN0 ( ( F ` t ) X. { t } ) e. _V -> ( G C_ U_ t e. NN0 ( ( F ` t ) X. { t } ) -> G ~<_ U_ t e. NN0 ( ( F ` t ) X. { t } ) ) )
40 12 38 39 mp2 
 |-  G ~<_ U_ t e. NN0 ( ( F ` t ) X. { t } )
41 nn0ennn 
 |-  NN0 ~~ NN
42 nnenom 
 |-  NN ~~ _om
43 41 42 entri 
 |-  NN0 ~~ _om
44 endom 
 |-  ( NN0 ~~ _om -> NN0 ~<_ _om )
45 43 44 ax-mp 
 |-  NN0 ~<_ _om
46 vex 
 |-  t e. _V
47 9 46 xpsnen 
 |-  ( ( F ` t ) X. { t } ) ~~ ( F ` t )
48 inss2 
 |-  ( ~P X i^i Fin ) C_ Fin
49 6 ffvelcdmda 
 |-  ( ( ph /\ t e. NN0 ) -> ( F ` t ) e. ( ~P X i^i Fin ) )
50 48 49 sselid 
 |-  ( ( ph /\ t e. NN0 ) -> ( F ` t ) e. Fin )
51 isfinite 
 |-  ( ( F ` t ) e. Fin <-> ( F ` t ) ~< _om )
52 sdomdom 
 |-  ( ( F ` t ) ~< _om -> ( F ` t ) ~<_ _om )
53 51 52 sylbi 
 |-  ( ( F ` t ) e. Fin -> ( F ` t ) ~<_ _om )
54 50 53 syl 
 |-  ( ( ph /\ t e. NN0 ) -> ( F ` t ) ~<_ _om )
55 endomtr 
 |-  ( ( ( ( F ` t ) X. { t } ) ~~ ( F ` t ) /\ ( F ` t ) ~<_ _om ) -> ( ( F ` t ) X. { t } ) ~<_ _om )
56 47 54 55 sylancr 
 |-  ( ( ph /\ t e. NN0 ) -> ( ( F ` t ) X. { t } ) ~<_ _om )
57 56 ralrimiva 
 |-  ( ph -> A. t e. NN0 ( ( F ` t ) X. { t } ) ~<_ _om )
58 iunctb 
 |-  ( ( NN0 ~<_ _om /\ A. t e. NN0 ( ( F ` t ) X. { t } ) ~<_ _om ) -> U_ t e. NN0 ( ( F ` t ) X. { t } ) ~<_ _om )
59 45 57 58 sylancr 
 |-  ( ph -> U_ t e. NN0 ( ( F ` t ) X. { t } ) ~<_ _om )
60 domtr 
 |-  ( ( G ~<_ U_ t e. NN0 ( ( F ` t ) X. { t } ) /\ U_ t e. NN0 ( ( F ` t ) X. { t } ) ~<_ _om ) -> G ~<_ _om )
61 40 59 60 sylancr 
 |-  ( ph -> G ~<_ _om )
62 23 simp1d 
 |-  ( x e. G -> ( 2nd ` x ) e. NN0 )
63 peano2nn0 
 |-  ( ( 2nd ` x ) e. NN0 -> ( ( 2nd ` x ) + 1 ) e. NN0 )
64 62 63 syl 
 |-  ( x e. G -> ( ( 2nd ` x ) + 1 ) e. NN0 )
65 ffvelcdm 
 |-  ( ( F : NN0 --> ( ~P X i^i Fin ) /\ ( ( 2nd ` x ) + 1 ) e. NN0 ) -> ( F ` ( ( 2nd ` x ) + 1 ) ) e. ( ~P X i^i Fin ) )
66 6 64 65 syl2an 
 |-  ( ( ph /\ x e. G ) -> ( F ` ( ( 2nd ` x ) + 1 ) ) e. ( ~P X i^i Fin ) )
67 48 66 sselid 
 |-  ( ( ph /\ x e. G ) -> ( F ` ( ( 2nd ` x ) + 1 ) ) e. Fin )
68 iunin2 
 |-  U_ t e. ( F ` ( ( 2nd ` x ) + 1 ) ) ( ( B ` x ) i^i ( t B ( ( 2nd ` x ) + 1 ) ) ) = ( ( B ` x ) i^i U_ t e. ( F ` ( ( 2nd ` x ) + 1 ) ) ( t B ( ( 2nd ` x ) + 1 ) ) )
69 oveq1 
 |-  ( y = t -> ( y B n ) = ( t B n ) )
70 69 cbviunv 
 |-  U_ y e. ( F ` n ) ( y B n ) = U_ t e. ( F ` n ) ( t B n )
71 fveq2 
 |-  ( n = ( ( 2nd ` x ) + 1 ) -> ( F ` n ) = ( F ` ( ( 2nd ` x ) + 1 ) ) )
72 71 iuneq1d 
 |-  ( n = ( ( 2nd ` x ) + 1 ) -> U_ t e. ( F ` n ) ( t B n ) = U_ t e. ( F ` ( ( 2nd ` x ) + 1 ) ) ( t B n ) )
73 70 72 eqtrid 
 |-  ( n = ( ( 2nd ` x ) + 1 ) -> U_ y e. ( F ` n ) ( y B n ) = U_ t e. ( F ` ( ( 2nd ` x ) + 1 ) ) ( t B n ) )
74 oveq2 
 |-  ( n = ( ( 2nd ` x ) + 1 ) -> ( t B n ) = ( t B ( ( 2nd ` x ) + 1 ) ) )
75 74 iuneq2d 
 |-  ( n = ( ( 2nd ` x ) + 1 ) -> U_ t e. ( F ` ( ( 2nd ` x ) + 1 ) ) ( t B n ) = U_ t e. ( F ` ( ( 2nd ` x ) + 1 ) ) ( t B ( ( 2nd ` x ) + 1 ) ) )
76 73 75 eqtrd 
 |-  ( n = ( ( 2nd ` x ) + 1 ) -> U_ y e. ( F ` n ) ( y B n ) = U_ t e. ( F ` ( ( 2nd ` x ) + 1 ) ) ( t B ( ( 2nd ` x ) + 1 ) ) )
77 76 eqeq2d 
 |-  ( n = ( ( 2nd ` x ) + 1 ) -> ( X = U_ y e. ( F ` n ) ( y B n ) <-> X = U_ t e. ( F ` ( ( 2nd ` x ) + 1 ) ) ( t B ( ( 2nd ` x ) + 1 ) ) ) )
78 77 rspccva 
 |-  ( ( A. n e. NN0 X = U_ y e. ( F ` n ) ( y B n ) /\ ( ( 2nd ` x ) + 1 ) e. NN0 ) -> X = U_ t e. ( F ` ( ( 2nd ` x ) + 1 ) ) ( t B ( ( 2nd ` x ) + 1 ) ) )
79 7 64 78 syl2an 
 |-  ( ( ph /\ x e. G ) -> X = U_ t e. ( F ` ( ( 2nd ` x ) + 1 ) ) ( t B ( ( 2nd ` x ) + 1 ) ) )
80 79 ineq2d 
 |-  ( ( ph /\ x e. G ) -> ( ( B ` x ) i^i X ) = ( ( B ` x ) i^i U_ t e. ( F ` ( ( 2nd ` x ) + 1 ) ) ( t B ( ( 2nd ` x ) + 1 ) ) ) )
81 15 fveq2d 
 |-  ( x e. G -> ( B ` x ) = ( B ` <. ( 1st ` x ) , ( 2nd ` x ) >. ) )
82 df-ov 
 |-  ( ( 1st ` x ) B ( 2nd ` x ) ) = ( B ` <. ( 1st ` x ) , ( 2nd ` x ) >. )
83 81 82 eqtr4di 
 |-  ( x e. G -> ( B ` x ) = ( ( 1st ` x ) B ( 2nd ` x ) ) )
84 83 adantl 
 |-  ( ( ph /\ x e. G ) -> ( B ` x ) = ( ( 1st ` x ) B ( 2nd ` x ) ) )
85 inss1 
 |-  ( ~P X i^i Fin ) C_ ~P X
86 ffvelcdm 
 |-  ( ( F : NN0 --> ( ~P X i^i Fin ) /\ ( 2nd ` x ) e. NN0 ) -> ( F ` ( 2nd ` x ) ) e. ( ~P X i^i Fin ) )
87 6 62 86 syl2an 
 |-  ( ( ph /\ x e. G ) -> ( F ` ( 2nd ` x ) ) e. ( ~P X i^i Fin ) )
88 85 87 sselid 
 |-  ( ( ph /\ x e. G ) -> ( F ` ( 2nd ` x ) ) e. ~P X )
89 88 elpwid 
 |-  ( ( ph /\ x e. G ) -> ( F ` ( 2nd ` x ) ) C_ X )
90 23 simp2d 
 |-  ( x e. G -> ( 1st ` x ) e. ( F ` ( 2nd ` x ) ) )
91 90 adantl 
 |-  ( ( ph /\ x e. G ) -> ( 1st ` x ) e. ( F ` ( 2nd ` x ) ) )
92 89 91 sseldd 
 |-  ( ( ph /\ x e. G ) -> ( 1st ` x ) e. X )
93 62 adantl 
 |-  ( ( ph /\ x e. G ) -> ( 2nd ` x ) e. NN0 )
94 oveq1 
 |-  ( z = ( 1st ` x ) -> ( z ( ball ` D ) ( 1 / ( 2 ^ m ) ) ) = ( ( 1st ` x ) ( ball ` D ) ( 1 / ( 2 ^ m ) ) ) )
95 oveq2 
 |-  ( m = ( 2nd ` x ) -> ( 2 ^ m ) = ( 2 ^ ( 2nd ` x ) ) )
96 95 oveq2d 
 |-  ( m = ( 2nd ` x ) -> ( 1 / ( 2 ^ m ) ) = ( 1 / ( 2 ^ ( 2nd ` x ) ) ) )
97 96 oveq2d 
 |-  ( m = ( 2nd ` x ) -> ( ( 1st ` x ) ( ball ` D ) ( 1 / ( 2 ^ m ) ) ) = ( ( 1st ` x ) ( ball ` D ) ( 1 / ( 2 ^ ( 2nd ` x ) ) ) ) )
98 ovex 
 |-  ( ( 1st ` x ) ( ball ` D ) ( 1 / ( 2 ^ ( 2nd ` x ) ) ) ) e. _V
99 94 97 4 98 ovmpo 
 |-  ( ( ( 1st ` x ) e. X /\ ( 2nd ` x ) e. NN0 ) -> ( ( 1st ` x ) B ( 2nd ` x ) ) = ( ( 1st ` x ) ( ball ` D ) ( 1 / ( 2 ^ ( 2nd ` x ) ) ) ) )
100 92 93 99 syl2anc 
 |-  ( ( ph /\ x e. G ) -> ( ( 1st ` x ) B ( 2nd ` x ) ) = ( ( 1st ` x ) ( ball ` D ) ( 1 / ( 2 ^ ( 2nd ` x ) ) ) ) )
101 84 100 eqtrd 
 |-  ( ( ph /\ x e. G ) -> ( B ` x ) = ( ( 1st ` x ) ( ball ` D ) ( 1 / ( 2 ^ ( 2nd ` x ) ) ) ) )
102 cmetmet 
 |-  ( D e. ( CMet ` X ) -> D e. ( Met ` X ) )
103 5 102 syl 
 |-  ( ph -> D e. ( Met ` X ) )
104 metxmet 
 |-  ( D e. ( Met ` X ) -> D e. ( *Met ` X ) )
105 103 104 syl 
 |-  ( ph -> D e. ( *Met ` X ) )
106 105 adantr 
 |-  ( ( ph /\ x e. G ) -> D e. ( *Met ` X ) )
107 2nn 
 |-  2 e. NN
108 nnexpcl 
 |-  ( ( 2 e. NN /\ ( 2nd ` x ) e. NN0 ) -> ( 2 ^ ( 2nd ` x ) ) e. NN )
109 107 93 108 sylancr 
 |-  ( ( ph /\ x e. G ) -> ( 2 ^ ( 2nd ` x ) ) e. NN )
110 109 nnrpd 
 |-  ( ( ph /\ x e. G ) -> ( 2 ^ ( 2nd ` x ) ) e. RR+ )
111 110 rpreccld 
 |-  ( ( ph /\ x e. G ) -> ( 1 / ( 2 ^ ( 2nd ` x ) ) ) e. RR+ )
112 111 rpxrd 
 |-  ( ( ph /\ x e. G ) -> ( 1 / ( 2 ^ ( 2nd ` x ) ) ) e. RR* )
113 blssm 
 |-  ( ( D e. ( *Met ` X ) /\ ( 1st ` x ) e. X /\ ( 1 / ( 2 ^ ( 2nd ` x ) ) ) e. RR* ) -> ( ( 1st ` x ) ( ball ` D ) ( 1 / ( 2 ^ ( 2nd ` x ) ) ) ) C_ X )
114 106 92 112 113 syl3anc 
 |-  ( ( ph /\ x e. G ) -> ( ( 1st ` x ) ( ball ` D ) ( 1 / ( 2 ^ ( 2nd ` x ) ) ) ) C_ X )
115 101 114 eqsstrd 
 |-  ( ( ph /\ x e. G ) -> ( B ` x ) C_ X )
116 dfss2 
 |-  ( ( B ` x ) C_ X <-> ( ( B ` x ) i^i X ) = ( B ` x ) )
117 115 116 sylib 
 |-  ( ( ph /\ x e. G ) -> ( ( B ` x ) i^i X ) = ( B ` x ) )
118 80 117 eqtr3d 
 |-  ( ( ph /\ x e. G ) -> ( ( B ` x ) i^i U_ t e. ( F ` ( ( 2nd ` x ) + 1 ) ) ( t B ( ( 2nd ` x ) + 1 ) ) ) = ( B ` x ) )
119 68 118 eqtrid 
 |-  ( ( ph /\ x e. G ) -> U_ t e. ( F ` ( ( 2nd ` x ) + 1 ) ) ( ( B ` x ) i^i ( t B ( ( 2nd ` x ) + 1 ) ) ) = ( B ` x ) )
120 eqimss2 
 |-  ( U_ t e. ( F ` ( ( 2nd ` x ) + 1 ) ) ( ( B ` x ) i^i ( t B ( ( 2nd ` x ) + 1 ) ) ) = ( B ` x ) -> ( B ` x ) C_ U_ t e. ( F ` ( ( 2nd ` x ) + 1 ) ) ( ( B ` x ) i^i ( t B ( ( 2nd ` x ) + 1 ) ) ) )
121 119 120 syl 
 |-  ( ( ph /\ x e. G ) -> ( B ` x ) C_ U_ t e. ( F ` ( ( 2nd ` x ) + 1 ) ) ( ( B ` x ) i^i ( t B ( ( 2nd ` x ) + 1 ) ) ) )
122 23 simp3d 
 |-  ( x e. G -> ( ( 1st ` x ) B ( 2nd ` x ) ) e. K )
123 83 122 eqeltrd 
 |-  ( x e. G -> ( B ` x ) e. K )
124 123 adantl 
 |-  ( ( ph /\ x e. G ) -> ( B ` x ) e. K )
125 fvex 
 |-  ( B ` x ) e. _V
126 125 inex1 
 |-  ( ( B ` x ) i^i ( t B ( ( 2nd ` x ) + 1 ) ) ) e. _V
127 1 2 126 heiborlem1 
 |-  ( ( ( F ` ( ( 2nd ` x ) + 1 ) ) e. Fin /\ ( B ` x ) C_ U_ t e. ( F ` ( ( 2nd ` x ) + 1 ) ) ( ( B ` x ) i^i ( t B ( ( 2nd ` x ) + 1 ) ) ) /\ ( B ` x ) e. K ) -> E. t e. ( F ` ( ( 2nd ` x ) + 1 ) ) ( ( B ` x ) i^i ( t B ( ( 2nd ` x ) + 1 ) ) ) e. K )
128 67 121 124 127 syl3anc 
 |-  ( ( ph /\ x e. G ) -> E. t e. ( F ` ( ( 2nd ` x ) + 1 ) ) ( ( B ` x ) i^i ( t B ( ( 2nd ` x ) + 1 ) ) ) e. K )
129 85 66 sselid 
 |-  ( ( ph /\ x e. G ) -> ( F ` ( ( 2nd ` x ) + 1 ) ) e. ~P X )
130 129 elpwid 
 |-  ( ( ph /\ x e. G ) -> ( F ` ( ( 2nd ` x ) + 1 ) ) C_ X )
131 1 mopnuni 
 |-  ( D e. ( *Met ` X ) -> X = U. J )
132 105 131 syl 
 |-  ( ph -> X = U. J )
133 132 adantr 
 |-  ( ( ph /\ x e. G ) -> X = U. J )
134 130 133 sseqtrd 
 |-  ( ( ph /\ x e. G ) -> ( F ` ( ( 2nd ` x ) + 1 ) ) C_ U. J )
135 134 sselda 
 |-  ( ( ( ph /\ x e. G ) /\ t e. ( F ` ( ( 2nd ` x ) + 1 ) ) ) -> t e. U. J )
136 135 adantrr 
 |-  ( ( ( ph /\ x e. G ) /\ ( t e. ( F ` ( ( 2nd ` x ) + 1 ) ) /\ ( ( B ` x ) i^i ( t B ( ( 2nd ` x ) + 1 ) ) ) e. K ) ) -> t e. U. J )
137 64 adantl 
 |-  ( ( ph /\ x e. G ) -> ( ( 2nd ` x ) + 1 ) e. NN0 )
138 id 
 |-  ( t e. ( F ` ( ( 2nd ` x ) + 1 ) ) -> t e. ( F ` ( ( 2nd ` x ) + 1 ) ) )
139 snfi 
 |-  { ( t B ( ( 2nd ` x ) + 1 ) ) } e. Fin
140 inss2 
 |-  ( ( B ` x ) i^i ( t B ( ( 2nd ` x ) + 1 ) ) ) C_ ( t B ( ( 2nd ` x ) + 1 ) )
141 ovex 
 |-  ( t B ( ( 2nd ` x ) + 1 ) ) e. _V
142 141 unisn 
 |-  U. { ( t B ( ( 2nd ` x ) + 1 ) ) } = ( t B ( ( 2nd ` x ) + 1 ) )
143 uniiun 
 |-  U. { ( t B ( ( 2nd ` x ) + 1 ) ) } = U_ g e. { ( t B ( ( 2nd ` x ) + 1 ) ) } g
144 142 143 eqtr3i 
 |-  ( t B ( ( 2nd ` x ) + 1 ) ) = U_ g e. { ( t B ( ( 2nd ` x ) + 1 ) ) } g
145 140 144 sseqtri 
 |-  ( ( B ` x ) i^i ( t B ( ( 2nd ` x ) + 1 ) ) ) C_ U_ g e. { ( t B ( ( 2nd ` x ) + 1 ) ) } g
146 vex 
 |-  g e. _V
147 1 2 146 heiborlem1 
 |-  ( ( { ( t B ( ( 2nd ` x ) + 1 ) ) } e. Fin /\ ( ( B ` x ) i^i ( t B ( ( 2nd ` x ) + 1 ) ) ) C_ U_ g e. { ( t B ( ( 2nd ` x ) + 1 ) ) } g /\ ( ( B ` x ) i^i ( t B ( ( 2nd ` x ) + 1 ) ) ) e. K ) -> E. g e. { ( t B ( ( 2nd ` x ) + 1 ) ) } g e. K )
148 139 145 147 mp3an12 
 |-  ( ( ( B ` x ) i^i ( t B ( ( 2nd ` x ) + 1 ) ) ) e. K -> E. g e. { ( t B ( ( 2nd ` x ) + 1 ) ) } g e. K )
149 eleq1 
 |-  ( g = ( t B ( ( 2nd ` x ) + 1 ) ) -> ( g e. K <-> ( t B ( ( 2nd ` x ) + 1 ) ) e. K ) )
150 141 149 rexsn 
 |-  ( E. g e. { ( t B ( ( 2nd ` x ) + 1 ) ) } g e. K <-> ( t B ( ( 2nd ` x ) + 1 ) ) e. K )
151 148 150 sylib 
 |-  ( ( ( B ` x ) i^i ( t B ( ( 2nd ` x ) + 1 ) ) ) e. K -> ( t B ( ( 2nd ` x ) + 1 ) ) e. K )
152 ovex 
 |-  ( ( 2nd ` x ) + 1 ) e. _V
153 1 2 3 46 152 heiborlem2 
 |-  ( t G ( ( 2nd ` x ) + 1 ) <-> ( ( ( 2nd ` x ) + 1 ) e. NN0 /\ t e. ( F ` ( ( 2nd ` x ) + 1 ) ) /\ ( t B ( ( 2nd ` x ) + 1 ) ) e. K ) )
154 153 biimpri 
 |-  ( ( ( ( 2nd ` x ) + 1 ) e. NN0 /\ t e. ( F ` ( ( 2nd ` x ) + 1 ) ) /\ ( t B ( ( 2nd ` x ) + 1 ) ) e. K ) -> t G ( ( 2nd ` x ) + 1 ) )
155 137 138 151 154 syl3an 
 |-  ( ( ( ph /\ x e. G ) /\ t e. ( F ` ( ( 2nd ` x ) + 1 ) ) /\ ( ( B ` x ) i^i ( t B ( ( 2nd ` x ) + 1 ) ) ) e. K ) -> t G ( ( 2nd ` x ) + 1 ) )
156 155 3expb 
 |-  ( ( ( ph /\ x e. G ) /\ ( t e. ( F ` ( ( 2nd ` x ) + 1 ) ) /\ ( ( B ` x ) i^i ( t B ( ( 2nd ` x ) + 1 ) ) ) e. K ) ) -> t G ( ( 2nd ` x ) + 1 ) )
157 simprr 
 |-  ( ( ( ph /\ x e. G ) /\ ( t e. ( F ` ( ( 2nd ` x ) + 1 ) ) /\ ( ( B ` x ) i^i ( t B ( ( 2nd ` x ) + 1 ) ) ) e. K ) ) -> ( ( B ` x ) i^i ( t B ( ( 2nd ` x ) + 1 ) ) ) e. K )
158 136 156 157 jca32 
 |-  ( ( ( ph /\ x e. G ) /\ ( t e. ( F ` ( ( 2nd ` x ) + 1 ) ) /\ ( ( B ` x ) i^i ( t B ( ( 2nd ` x ) + 1 ) ) ) e. K ) ) -> ( t e. U. J /\ ( t G ( ( 2nd ` x ) + 1 ) /\ ( ( B ` x ) i^i ( t B ( ( 2nd ` x ) + 1 ) ) ) e. K ) ) )
159 158 ex 
 |-  ( ( ph /\ x e. G ) -> ( ( t e. ( F ` ( ( 2nd ` x ) + 1 ) ) /\ ( ( B ` x ) i^i ( t B ( ( 2nd ` x ) + 1 ) ) ) e. K ) -> ( t e. U. J /\ ( t G ( ( 2nd ` x ) + 1 ) /\ ( ( B ` x ) i^i ( t B ( ( 2nd ` x ) + 1 ) ) ) e. K ) ) ) )
160 159 reximdv2 
 |-  ( ( ph /\ x e. G ) -> ( E. t e. ( F ` ( ( 2nd ` x ) + 1 ) ) ( ( B ` x ) i^i ( t B ( ( 2nd ` x ) + 1 ) ) ) e. K -> E. t e. U. J ( t G ( ( 2nd ` x ) + 1 ) /\ ( ( B ` x ) i^i ( t B ( ( 2nd ` x ) + 1 ) ) ) e. K ) ) )
161 128 160 mpd 
 |-  ( ( ph /\ x e. G ) -> E. t e. U. J ( t G ( ( 2nd ` x ) + 1 ) /\ ( ( B ` x ) i^i ( t B ( ( 2nd ` x ) + 1 ) ) ) e. K ) )
162 161 ralrimiva 
 |-  ( ph -> A. x e. G E. t e. U. J ( t G ( ( 2nd ` x ) + 1 ) /\ ( ( B ` x ) i^i ( t B ( ( 2nd ` x ) + 1 ) ) ) e. K ) )
163 1 fvexi 
 |-  J e. _V
164 163 uniex 
 |-  U. J e. _V
165 breq1 
 |-  ( t = ( g ` x ) -> ( t G ( ( 2nd ` x ) + 1 ) <-> ( g ` x ) G ( ( 2nd ` x ) + 1 ) ) )
166 oveq1 
 |-  ( t = ( g ` x ) -> ( t B ( ( 2nd ` x ) + 1 ) ) = ( ( g ` x ) B ( ( 2nd ` x ) + 1 ) ) )
167 166 ineq2d 
 |-  ( t = ( g ` x ) -> ( ( B ` x ) i^i ( t B ( ( 2nd ` x ) + 1 ) ) ) = ( ( B ` x ) i^i ( ( g ` x ) B ( ( 2nd ` x ) + 1 ) ) ) )
168 167 eleq1d 
 |-  ( t = ( g ` x ) -> ( ( ( B ` x ) i^i ( t B ( ( 2nd ` x ) + 1 ) ) ) e. K <-> ( ( B ` x ) i^i ( ( g ` x ) B ( ( 2nd ` x ) + 1 ) ) ) e. K ) )
169 165 168 anbi12d 
 |-  ( t = ( g ` x ) -> ( ( t G ( ( 2nd ` x ) + 1 ) /\ ( ( B ` x ) i^i ( t B ( ( 2nd ` x ) + 1 ) ) ) e. K ) <-> ( ( g ` x ) G ( ( 2nd ` x ) + 1 ) /\ ( ( B ` x ) i^i ( ( g ` x ) B ( ( 2nd ` x ) + 1 ) ) ) e. K ) ) )
170 164 169 axcc4dom 
 |-  ( ( G ~<_ _om /\ A. x e. G E. t e. U. J ( t G ( ( 2nd ` x ) + 1 ) /\ ( ( B ` x ) i^i ( t B ( ( 2nd ` x ) + 1 ) ) ) e. K ) ) -> E. g ( g : G --> U. J /\ A. x e. G ( ( g ` x ) G ( ( 2nd ` x ) + 1 ) /\ ( ( B ` x ) i^i ( ( g ` x ) B ( ( 2nd ` x ) + 1 ) ) ) e. K ) ) )
171 61 162 170 syl2anc 
 |-  ( ph -> E. g ( g : G --> U. J /\ A. x e. G ( ( g ` x ) G ( ( 2nd ` x ) + 1 ) /\ ( ( B ` x ) i^i ( ( g ` x ) B ( ( 2nd ` x ) + 1 ) ) ) e. K ) ) )
172 exsimpr 
 |-  ( E. g ( g : G --> U. J /\ A. x e. G ( ( g ` x ) G ( ( 2nd ` x ) + 1 ) /\ ( ( B ` x ) i^i ( ( g ` x ) B ( ( 2nd ` x ) + 1 ) ) ) e. K ) ) -> E. g A. x e. G ( ( g ` x ) G ( ( 2nd ` x ) + 1 ) /\ ( ( B ` x ) i^i ( ( g ` x ) B ( ( 2nd ` x ) + 1 ) ) ) e. K ) )
173 171 172 syl 
 |-  ( ph -> E. g A. x e. G ( ( g ` x ) G ( ( 2nd ` x ) + 1 ) /\ ( ( B ` x ) i^i ( ( g ` x ) B ( ( 2nd ` x ) + 1 ) ) ) e. K ) )