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 snex
 |-  { 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 ffvelrnda
 |-  ( ( ph /\ t e. NN0 ) -> ( F ` t ) e. ( ~P X i^i Fin ) )
50 48 49 sseldi
 |-  ( ( 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 ffvelrn
 |-  ( ( 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 sseldi
 |-  ( ( 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 syl5eq
 |-  ( 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 ffvelrn
 |-  ( ( 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 sseldi
 |-  ( ( 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 df-ss
 |-  ( ( 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 syl5eq
 |-  ( ( 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 sseldi
 |-  ( ( 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 ) )