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 𝐽 = ( MetOpen ‘ 𝐷 )
heibor.3 𝐾 = { 𝑢 ∣ ¬ ∃ 𝑣 ∈ ( 𝒫 𝑈 ∩ Fin ) 𝑢 𝑣 }
heibor.4 𝐺 = { ⟨ 𝑦 , 𝑛 ⟩ ∣ ( 𝑛 ∈ ℕ0𝑦 ∈ ( 𝐹𝑛 ) ∧ ( 𝑦 𝐵 𝑛 ) ∈ 𝐾 ) }
heibor.5 𝐵 = ( 𝑧𝑋 , 𝑚 ∈ ℕ0 ↦ ( 𝑧 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑚 ) ) ) )
heibor.6 ( 𝜑𝐷 ∈ ( CMet ‘ 𝑋 ) )
heibor.7 ( 𝜑𝐹 : ℕ0 ⟶ ( 𝒫 𝑋 ∩ Fin ) )
heibor.8 ( 𝜑 → ∀ 𝑛 ∈ ℕ0 𝑋 = 𝑦 ∈ ( 𝐹𝑛 ) ( 𝑦 𝐵 𝑛 ) )
Assertion heiborlem3 ( 𝜑 → ∃ 𝑔𝑥𝐺 ( ( 𝑔𝑥 ) 𝐺 ( ( 2nd𝑥 ) + 1 ) ∧ ( ( 𝐵𝑥 ) ∩ ( ( 𝑔𝑥 ) 𝐵 ( ( 2nd𝑥 ) + 1 ) ) ) ∈ 𝐾 ) )

Proof

Step Hyp Ref Expression
1 heibor.1 𝐽 = ( MetOpen ‘ 𝐷 )
2 heibor.3 𝐾 = { 𝑢 ∣ ¬ ∃ 𝑣 ∈ ( 𝒫 𝑈 ∩ Fin ) 𝑢 𝑣 }
3 heibor.4 𝐺 = { ⟨ 𝑦 , 𝑛 ⟩ ∣ ( 𝑛 ∈ ℕ0𝑦 ∈ ( 𝐹𝑛 ) ∧ ( 𝑦 𝐵 𝑛 ) ∈ 𝐾 ) }
4 heibor.5 𝐵 = ( 𝑧𝑋 , 𝑚 ∈ ℕ0 ↦ ( 𝑧 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑚 ) ) ) )
5 heibor.6 ( 𝜑𝐷 ∈ ( CMet ‘ 𝑋 ) )
6 heibor.7 ( 𝜑𝐹 : ℕ0 ⟶ ( 𝒫 𝑋 ∩ Fin ) )
7 heibor.8 ( 𝜑 → ∀ 𝑛 ∈ ℕ0 𝑋 = 𝑦 ∈ ( 𝐹𝑛 ) ( 𝑦 𝐵 𝑛 ) )
8 nn0ex 0 ∈ V
9 fvex ( 𝐹𝑡 ) ∈ V
10 snex { 𝑡 } ∈ V
11 9 10 xpex ( ( 𝐹𝑡 ) × { 𝑡 } ) ∈ V
12 8 11 iunex 𝑡 ∈ ℕ0 ( ( 𝐹𝑡 ) × { 𝑡 } ) ∈ V
13 3 relopabiv Rel 𝐺
14 1st2nd ( ( Rel 𝐺𝑥𝐺 ) → 𝑥 = ⟨ ( 1st𝑥 ) , ( 2nd𝑥 ) ⟩ )
15 13 14 mpan ( 𝑥𝐺𝑥 = ⟨ ( 1st𝑥 ) , ( 2nd𝑥 ) ⟩ )
16 15 eleq1d ( 𝑥𝐺 → ( 𝑥𝐺 ↔ ⟨ ( 1st𝑥 ) , ( 2nd𝑥 ) ⟩ ∈ 𝐺 ) )
17 df-br ( ( 1st𝑥 ) 𝐺 ( 2nd𝑥 ) ↔ ⟨ ( 1st𝑥 ) , ( 2nd𝑥 ) ⟩ ∈ 𝐺 )
18 16 17 bitr4di ( 𝑥𝐺 → ( 𝑥𝐺 ↔ ( 1st𝑥 ) 𝐺 ( 2nd𝑥 ) ) )
19 fvex ( 1st𝑥 ) ∈ V
20 fvex ( 2nd𝑥 ) ∈ V
21 1 2 3 19 20 heiborlem2 ( ( 1st𝑥 ) 𝐺 ( 2nd𝑥 ) ↔ ( ( 2nd𝑥 ) ∈ ℕ0 ∧ ( 1st𝑥 ) ∈ ( 𝐹 ‘ ( 2nd𝑥 ) ) ∧ ( ( 1st𝑥 ) 𝐵 ( 2nd𝑥 ) ) ∈ 𝐾 ) )
22 18 21 bitrdi ( 𝑥𝐺 → ( 𝑥𝐺 ↔ ( ( 2nd𝑥 ) ∈ ℕ0 ∧ ( 1st𝑥 ) ∈ ( 𝐹 ‘ ( 2nd𝑥 ) ) ∧ ( ( 1st𝑥 ) 𝐵 ( 2nd𝑥 ) ) ∈ 𝐾 ) ) )
23 22 ibi ( 𝑥𝐺 → ( ( 2nd𝑥 ) ∈ ℕ0 ∧ ( 1st𝑥 ) ∈ ( 𝐹 ‘ ( 2nd𝑥 ) ) ∧ ( ( 1st𝑥 ) 𝐵 ( 2nd𝑥 ) ) ∈ 𝐾 ) )
24 20 snid ( 2nd𝑥 ) ∈ { ( 2nd𝑥 ) }
25 opelxp ( ⟨ ( 1st𝑥 ) , ( 2nd𝑥 ) ⟩ ∈ ( ( 𝐹 ‘ ( 2nd𝑥 ) ) × { ( 2nd𝑥 ) } ) ↔ ( ( 1st𝑥 ) ∈ ( 𝐹 ‘ ( 2nd𝑥 ) ) ∧ ( 2nd𝑥 ) ∈ { ( 2nd𝑥 ) } ) )
26 24 25 mpbiran2 ( ⟨ ( 1st𝑥 ) , ( 2nd𝑥 ) ⟩ ∈ ( ( 𝐹 ‘ ( 2nd𝑥 ) ) × { ( 2nd𝑥 ) } ) ↔ ( 1st𝑥 ) ∈ ( 𝐹 ‘ ( 2nd𝑥 ) ) )
27 fveq2 ( 𝑡 = ( 2nd𝑥 ) → ( 𝐹𝑡 ) = ( 𝐹 ‘ ( 2nd𝑥 ) ) )
28 sneq ( 𝑡 = ( 2nd𝑥 ) → { 𝑡 } = { ( 2nd𝑥 ) } )
29 27 28 xpeq12d ( 𝑡 = ( 2nd𝑥 ) → ( ( 𝐹𝑡 ) × { 𝑡 } ) = ( ( 𝐹 ‘ ( 2nd𝑥 ) ) × { ( 2nd𝑥 ) } ) )
30 29 eleq2d ( 𝑡 = ( 2nd𝑥 ) → ( ⟨ ( 1st𝑥 ) , ( 2nd𝑥 ) ⟩ ∈ ( ( 𝐹𝑡 ) × { 𝑡 } ) ↔ ⟨ ( 1st𝑥 ) , ( 2nd𝑥 ) ⟩ ∈ ( ( 𝐹 ‘ ( 2nd𝑥 ) ) × { ( 2nd𝑥 ) } ) ) )
31 30 rspcev ( ( ( 2nd𝑥 ) ∈ ℕ0 ∧ ⟨ ( 1st𝑥 ) , ( 2nd𝑥 ) ⟩ ∈ ( ( 𝐹 ‘ ( 2nd𝑥 ) ) × { ( 2nd𝑥 ) } ) ) → ∃ 𝑡 ∈ ℕ0 ⟨ ( 1st𝑥 ) , ( 2nd𝑥 ) ⟩ ∈ ( ( 𝐹𝑡 ) × { 𝑡 } ) )
32 26 31 sylan2br ( ( ( 2nd𝑥 ) ∈ ℕ0 ∧ ( 1st𝑥 ) ∈ ( 𝐹 ‘ ( 2nd𝑥 ) ) ) → ∃ 𝑡 ∈ ℕ0 ⟨ ( 1st𝑥 ) , ( 2nd𝑥 ) ⟩ ∈ ( ( 𝐹𝑡 ) × { 𝑡 } ) )
33 eliun ( ⟨ ( 1st𝑥 ) , ( 2nd𝑥 ) ⟩ ∈ 𝑡 ∈ ℕ0 ( ( 𝐹𝑡 ) × { 𝑡 } ) ↔ ∃ 𝑡 ∈ ℕ0 ⟨ ( 1st𝑥 ) , ( 2nd𝑥 ) ⟩ ∈ ( ( 𝐹𝑡 ) × { 𝑡 } ) )
34 32 33 sylibr ( ( ( 2nd𝑥 ) ∈ ℕ0 ∧ ( 1st𝑥 ) ∈ ( 𝐹 ‘ ( 2nd𝑥 ) ) ) → ⟨ ( 1st𝑥 ) , ( 2nd𝑥 ) ⟩ ∈ 𝑡 ∈ ℕ0 ( ( 𝐹𝑡 ) × { 𝑡 } ) )
35 34 3adant3 ( ( ( 2nd𝑥 ) ∈ ℕ0 ∧ ( 1st𝑥 ) ∈ ( 𝐹 ‘ ( 2nd𝑥 ) ) ∧ ( ( 1st𝑥 ) 𝐵 ( 2nd𝑥 ) ) ∈ 𝐾 ) → ⟨ ( 1st𝑥 ) , ( 2nd𝑥 ) ⟩ ∈ 𝑡 ∈ ℕ0 ( ( 𝐹𝑡 ) × { 𝑡 } ) )
36 23 35 syl ( 𝑥𝐺 → ⟨ ( 1st𝑥 ) , ( 2nd𝑥 ) ⟩ ∈ 𝑡 ∈ ℕ0 ( ( 𝐹𝑡 ) × { 𝑡 } ) )
37 15 36 eqeltrd ( 𝑥𝐺𝑥 𝑡 ∈ ℕ0 ( ( 𝐹𝑡 ) × { 𝑡 } ) )
38 37 ssriv 𝐺 𝑡 ∈ ℕ0 ( ( 𝐹𝑡 ) × { 𝑡 } )
39 ssdomg ( 𝑡 ∈ ℕ0 ( ( 𝐹𝑡 ) × { 𝑡 } ) ∈ V → ( 𝐺 𝑡 ∈ ℕ0 ( ( 𝐹𝑡 ) × { 𝑡 } ) → 𝐺 𝑡 ∈ ℕ0 ( ( 𝐹𝑡 ) × { 𝑡 } ) ) )
40 12 38 39 mp2 𝐺 𝑡 ∈ ℕ0 ( ( 𝐹𝑡 ) × { 𝑡 } )
41 nn0ennn 0 ≈ ℕ
42 nnenom ℕ ≈ ω
43 41 42 entri 0 ≈ ω
44 endom ( ℕ0 ≈ ω → ℕ0 ≼ ω )
45 43 44 ax-mp 0 ≼ ω
46 vex 𝑡 ∈ V
47 9 46 xpsnen ( ( 𝐹𝑡 ) × { 𝑡 } ) ≈ ( 𝐹𝑡 )
48 inss2 ( 𝒫 𝑋 ∩ Fin ) ⊆ Fin
49 6 ffvelrnda ( ( 𝜑𝑡 ∈ ℕ0 ) → ( 𝐹𝑡 ) ∈ ( 𝒫 𝑋 ∩ Fin ) )
50 48 49 sseldi ( ( 𝜑𝑡 ∈ ℕ0 ) → ( 𝐹𝑡 ) ∈ Fin )
51 isfinite ( ( 𝐹𝑡 ) ∈ Fin ↔ ( 𝐹𝑡 ) ≺ ω )
52 sdomdom ( ( 𝐹𝑡 ) ≺ ω → ( 𝐹𝑡 ) ≼ ω )
53 51 52 sylbi ( ( 𝐹𝑡 ) ∈ Fin → ( 𝐹𝑡 ) ≼ ω )
54 50 53 syl ( ( 𝜑𝑡 ∈ ℕ0 ) → ( 𝐹𝑡 ) ≼ ω )
55 endomtr ( ( ( ( 𝐹𝑡 ) × { 𝑡 } ) ≈ ( 𝐹𝑡 ) ∧ ( 𝐹𝑡 ) ≼ ω ) → ( ( 𝐹𝑡 ) × { 𝑡 } ) ≼ ω )
56 47 54 55 sylancr ( ( 𝜑𝑡 ∈ ℕ0 ) → ( ( 𝐹𝑡 ) × { 𝑡 } ) ≼ ω )
57 56 ralrimiva ( 𝜑 → ∀ 𝑡 ∈ ℕ0 ( ( 𝐹𝑡 ) × { 𝑡 } ) ≼ ω )
58 iunctb ( ( ℕ0 ≼ ω ∧ ∀ 𝑡 ∈ ℕ0 ( ( 𝐹𝑡 ) × { 𝑡 } ) ≼ ω ) → 𝑡 ∈ ℕ0 ( ( 𝐹𝑡 ) × { 𝑡 } ) ≼ ω )
59 45 57 58 sylancr ( 𝜑 𝑡 ∈ ℕ0 ( ( 𝐹𝑡 ) × { 𝑡 } ) ≼ ω )
60 domtr ( ( 𝐺 𝑡 ∈ ℕ0 ( ( 𝐹𝑡 ) × { 𝑡 } ) ∧ 𝑡 ∈ ℕ0 ( ( 𝐹𝑡 ) × { 𝑡 } ) ≼ ω ) → 𝐺 ≼ ω )
61 40 59 60 sylancr ( 𝜑𝐺 ≼ ω )
62 23 simp1d ( 𝑥𝐺 → ( 2nd𝑥 ) ∈ ℕ0 )
63 peano2nn0 ( ( 2nd𝑥 ) ∈ ℕ0 → ( ( 2nd𝑥 ) + 1 ) ∈ ℕ0 )
64 62 63 syl ( 𝑥𝐺 → ( ( 2nd𝑥 ) + 1 ) ∈ ℕ0 )
65 ffvelrn ( ( 𝐹 : ℕ0 ⟶ ( 𝒫 𝑋 ∩ Fin ) ∧ ( ( 2nd𝑥 ) + 1 ) ∈ ℕ0 ) → ( 𝐹 ‘ ( ( 2nd𝑥 ) + 1 ) ) ∈ ( 𝒫 𝑋 ∩ Fin ) )
66 6 64 65 syl2an ( ( 𝜑𝑥𝐺 ) → ( 𝐹 ‘ ( ( 2nd𝑥 ) + 1 ) ) ∈ ( 𝒫 𝑋 ∩ Fin ) )
67 48 66 sseldi ( ( 𝜑𝑥𝐺 ) → ( 𝐹 ‘ ( ( 2nd𝑥 ) + 1 ) ) ∈ Fin )
68 iunin2 𝑡 ∈ ( 𝐹 ‘ ( ( 2nd𝑥 ) + 1 ) ) ( ( 𝐵𝑥 ) ∩ ( 𝑡 𝐵 ( ( 2nd𝑥 ) + 1 ) ) ) = ( ( 𝐵𝑥 ) ∩ 𝑡 ∈ ( 𝐹 ‘ ( ( 2nd𝑥 ) + 1 ) ) ( 𝑡 𝐵 ( ( 2nd𝑥 ) + 1 ) ) )
69 oveq1 ( 𝑦 = 𝑡 → ( 𝑦 𝐵 𝑛 ) = ( 𝑡 𝐵 𝑛 ) )
70 69 cbviunv 𝑦 ∈ ( 𝐹𝑛 ) ( 𝑦 𝐵 𝑛 ) = 𝑡 ∈ ( 𝐹𝑛 ) ( 𝑡 𝐵 𝑛 )
71 fveq2 ( 𝑛 = ( ( 2nd𝑥 ) + 1 ) → ( 𝐹𝑛 ) = ( 𝐹 ‘ ( ( 2nd𝑥 ) + 1 ) ) )
72 71 iuneq1d ( 𝑛 = ( ( 2nd𝑥 ) + 1 ) → 𝑡 ∈ ( 𝐹𝑛 ) ( 𝑡 𝐵 𝑛 ) = 𝑡 ∈ ( 𝐹 ‘ ( ( 2nd𝑥 ) + 1 ) ) ( 𝑡 𝐵 𝑛 ) )
73 70 72 syl5eq ( 𝑛 = ( ( 2nd𝑥 ) + 1 ) → 𝑦 ∈ ( 𝐹𝑛 ) ( 𝑦 𝐵 𝑛 ) = 𝑡 ∈ ( 𝐹 ‘ ( ( 2nd𝑥 ) + 1 ) ) ( 𝑡 𝐵 𝑛 ) )
74 oveq2 ( 𝑛 = ( ( 2nd𝑥 ) + 1 ) → ( 𝑡 𝐵 𝑛 ) = ( 𝑡 𝐵 ( ( 2nd𝑥 ) + 1 ) ) )
75 74 iuneq2d ( 𝑛 = ( ( 2nd𝑥 ) + 1 ) → 𝑡 ∈ ( 𝐹 ‘ ( ( 2nd𝑥 ) + 1 ) ) ( 𝑡 𝐵 𝑛 ) = 𝑡 ∈ ( 𝐹 ‘ ( ( 2nd𝑥 ) + 1 ) ) ( 𝑡 𝐵 ( ( 2nd𝑥 ) + 1 ) ) )
76 73 75 eqtrd ( 𝑛 = ( ( 2nd𝑥 ) + 1 ) → 𝑦 ∈ ( 𝐹𝑛 ) ( 𝑦 𝐵 𝑛 ) = 𝑡 ∈ ( 𝐹 ‘ ( ( 2nd𝑥 ) + 1 ) ) ( 𝑡 𝐵 ( ( 2nd𝑥 ) + 1 ) ) )
77 76 eqeq2d ( 𝑛 = ( ( 2nd𝑥 ) + 1 ) → ( 𝑋 = 𝑦 ∈ ( 𝐹𝑛 ) ( 𝑦 𝐵 𝑛 ) ↔ 𝑋 = 𝑡 ∈ ( 𝐹 ‘ ( ( 2nd𝑥 ) + 1 ) ) ( 𝑡 𝐵 ( ( 2nd𝑥 ) + 1 ) ) ) )
78 77 rspccva ( ( ∀ 𝑛 ∈ ℕ0 𝑋 = 𝑦 ∈ ( 𝐹𝑛 ) ( 𝑦 𝐵 𝑛 ) ∧ ( ( 2nd𝑥 ) + 1 ) ∈ ℕ0 ) → 𝑋 = 𝑡 ∈ ( 𝐹 ‘ ( ( 2nd𝑥 ) + 1 ) ) ( 𝑡 𝐵 ( ( 2nd𝑥 ) + 1 ) ) )
79 7 64 78 syl2an ( ( 𝜑𝑥𝐺 ) → 𝑋 = 𝑡 ∈ ( 𝐹 ‘ ( ( 2nd𝑥 ) + 1 ) ) ( 𝑡 𝐵 ( ( 2nd𝑥 ) + 1 ) ) )
80 79 ineq2d ( ( 𝜑𝑥𝐺 ) → ( ( 𝐵𝑥 ) ∩ 𝑋 ) = ( ( 𝐵𝑥 ) ∩ 𝑡 ∈ ( 𝐹 ‘ ( ( 2nd𝑥 ) + 1 ) ) ( 𝑡 𝐵 ( ( 2nd𝑥 ) + 1 ) ) ) )
81 15 fveq2d ( 𝑥𝐺 → ( 𝐵𝑥 ) = ( 𝐵 ‘ ⟨ ( 1st𝑥 ) , ( 2nd𝑥 ) ⟩ ) )
82 df-ov ( ( 1st𝑥 ) 𝐵 ( 2nd𝑥 ) ) = ( 𝐵 ‘ ⟨ ( 1st𝑥 ) , ( 2nd𝑥 ) ⟩ )
83 81 82 eqtr4di ( 𝑥𝐺 → ( 𝐵𝑥 ) = ( ( 1st𝑥 ) 𝐵 ( 2nd𝑥 ) ) )
84 83 adantl ( ( 𝜑𝑥𝐺 ) → ( 𝐵𝑥 ) = ( ( 1st𝑥 ) 𝐵 ( 2nd𝑥 ) ) )
85 inss1 ( 𝒫 𝑋 ∩ Fin ) ⊆ 𝒫 𝑋
86 ffvelrn ( ( 𝐹 : ℕ0 ⟶ ( 𝒫 𝑋 ∩ Fin ) ∧ ( 2nd𝑥 ) ∈ ℕ0 ) → ( 𝐹 ‘ ( 2nd𝑥 ) ) ∈ ( 𝒫 𝑋 ∩ Fin ) )
87 6 62 86 syl2an ( ( 𝜑𝑥𝐺 ) → ( 𝐹 ‘ ( 2nd𝑥 ) ) ∈ ( 𝒫 𝑋 ∩ Fin ) )
88 85 87 sseldi ( ( 𝜑𝑥𝐺 ) → ( 𝐹 ‘ ( 2nd𝑥 ) ) ∈ 𝒫 𝑋 )
89 88 elpwid ( ( 𝜑𝑥𝐺 ) → ( 𝐹 ‘ ( 2nd𝑥 ) ) ⊆ 𝑋 )
90 23 simp2d ( 𝑥𝐺 → ( 1st𝑥 ) ∈ ( 𝐹 ‘ ( 2nd𝑥 ) ) )
91 90 adantl ( ( 𝜑𝑥𝐺 ) → ( 1st𝑥 ) ∈ ( 𝐹 ‘ ( 2nd𝑥 ) ) )
92 89 91 sseldd ( ( 𝜑𝑥𝐺 ) → ( 1st𝑥 ) ∈ 𝑋 )
93 62 adantl ( ( 𝜑𝑥𝐺 ) → ( 2nd𝑥 ) ∈ ℕ0 )
94 oveq1 ( 𝑧 = ( 1st𝑥 ) → ( 𝑧 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑚 ) ) ) = ( ( 1st𝑥 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑚 ) ) ) )
95 oveq2 ( 𝑚 = ( 2nd𝑥 ) → ( 2 ↑ 𝑚 ) = ( 2 ↑ ( 2nd𝑥 ) ) )
96 95 oveq2d ( 𝑚 = ( 2nd𝑥 ) → ( 1 / ( 2 ↑ 𝑚 ) ) = ( 1 / ( 2 ↑ ( 2nd𝑥 ) ) ) )
97 96 oveq2d ( 𝑚 = ( 2nd𝑥 ) → ( ( 1st𝑥 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑚 ) ) ) = ( ( 1st𝑥 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ ( 2nd𝑥 ) ) ) ) )
98 ovex ( ( 1st𝑥 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ ( 2nd𝑥 ) ) ) ) ∈ V
99 94 97 4 98 ovmpo ( ( ( 1st𝑥 ) ∈ 𝑋 ∧ ( 2nd𝑥 ) ∈ ℕ0 ) → ( ( 1st𝑥 ) 𝐵 ( 2nd𝑥 ) ) = ( ( 1st𝑥 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ ( 2nd𝑥 ) ) ) ) )
100 92 93 99 syl2anc ( ( 𝜑𝑥𝐺 ) → ( ( 1st𝑥 ) 𝐵 ( 2nd𝑥 ) ) = ( ( 1st𝑥 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ ( 2nd𝑥 ) ) ) ) )
101 84 100 eqtrd ( ( 𝜑𝑥𝐺 ) → ( 𝐵𝑥 ) = ( ( 1st𝑥 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ ( 2nd𝑥 ) ) ) ) )
102 cmetmet ( 𝐷 ∈ ( CMet ‘ 𝑋 ) → 𝐷 ∈ ( Met ‘ 𝑋 ) )
103 5 102 syl ( 𝜑𝐷 ∈ ( Met ‘ 𝑋 ) )
104 metxmet ( 𝐷 ∈ ( Met ‘ 𝑋 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
105 103 104 syl ( 𝜑𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
106 105 adantr ( ( 𝜑𝑥𝐺 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
107 2nn 2 ∈ ℕ
108 nnexpcl ( ( 2 ∈ ℕ ∧ ( 2nd𝑥 ) ∈ ℕ0 ) → ( 2 ↑ ( 2nd𝑥 ) ) ∈ ℕ )
109 107 93 108 sylancr ( ( 𝜑𝑥𝐺 ) → ( 2 ↑ ( 2nd𝑥 ) ) ∈ ℕ )
110 109 nnrpd ( ( 𝜑𝑥𝐺 ) → ( 2 ↑ ( 2nd𝑥 ) ) ∈ ℝ+ )
111 110 rpreccld ( ( 𝜑𝑥𝐺 ) → ( 1 / ( 2 ↑ ( 2nd𝑥 ) ) ) ∈ ℝ+ )
112 111 rpxrd ( ( 𝜑𝑥𝐺 ) → ( 1 / ( 2 ↑ ( 2nd𝑥 ) ) ) ∈ ℝ* )
113 blssm ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 1st𝑥 ) ∈ 𝑋 ∧ ( 1 / ( 2 ↑ ( 2nd𝑥 ) ) ) ∈ ℝ* ) → ( ( 1st𝑥 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ ( 2nd𝑥 ) ) ) ) ⊆ 𝑋 )
114 106 92 112 113 syl3anc ( ( 𝜑𝑥𝐺 ) → ( ( 1st𝑥 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ ( 2nd𝑥 ) ) ) ) ⊆ 𝑋 )
115 101 114 eqsstrd ( ( 𝜑𝑥𝐺 ) → ( 𝐵𝑥 ) ⊆ 𝑋 )
116 df-ss ( ( 𝐵𝑥 ) ⊆ 𝑋 ↔ ( ( 𝐵𝑥 ) ∩ 𝑋 ) = ( 𝐵𝑥 ) )
117 115 116 sylib ( ( 𝜑𝑥𝐺 ) → ( ( 𝐵𝑥 ) ∩ 𝑋 ) = ( 𝐵𝑥 ) )
118 80 117 eqtr3d ( ( 𝜑𝑥𝐺 ) → ( ( 𝐵𝑥 ) ∩ 𝑡 ∈ ( 𝐹 ‘ ( ( 2nd𝑥 ) + 1 ) ) ( 𝑡 𝐵 ( ( 2nd𝑥 ) + 1 ) ) ) = ( 𝐵𝑥 ) )
119 68 118 syl5eq ( ( 𝜑𝑥𝐺 ) → 𝑡 ∈ ( 𝐹 ‘ ( ( 2nd𝑥 ) + 1 ) ) ( ( 𝐵𝑥 ) ∩ ( 𝑡 𝐵 ( ( 2nd𝑥 ) + 1 ) ) ) = ( 𝐵𝑥 ) )
120 eqimss2 ( 𝑡 ∈ ( 𝐹 ‘ ( ( 2nd𝑥 ) + 1 ) ) ( ( 𝐵𝑥 ) ∩ ( 𝑡 𝐵 ( ( 2nd𝑥 ) + 1 ) ) ) = ( 𝐵𝑥 ) → ( 𝐵𝑥 ) ⊆ 𝑡 ∈ ( 𝐹 ‘ ( ( 2nd𝑥 ) + 1 ) ) ( ( 𝐵𝑥 ) ∩ ( 𝑡 𝐵 ( ( 2nd𝑥 ) + 1 ) ) ) )
121 119 120 syl ( ( 𝜑𝑥𝐺 ) → ( 𝐵𝑥 ) ⊆ 𝑡 ∈ ( 𝐹 ‘ ( ( 2nd𝑥 ) + 1 ) ) ( ( 𝐵𝑥 ) ∩ ( 𝑡 𝐵 ( ( 2nd𝑥 ) + 1 ) ) ) )
122 23 simp3d ( 𝑥𝐺 → ( ( 1st𝑥 ) 𝐵 ( 2nd𝑥 ) ) ∈ 𝐾 )
123 83 122 eqeltrd ( 𝑥𝐺 → ( 𝐵𝑥 ) ∈ 𝐾 )
124 123 adantl ( ( 𝜑𝑥𝐺 ) → ( 𝐵𝑥 ) ∈ 𝐾 )
125 fvex ( 𝐵𝑥 ) ∈ V
126 125 inex1 ( ( 𝐵𝑥 ) ∩ ( 𝑡 𝐵 ( ( 2nd𝑥 ) + 1 ) ) ) ∈ V
127 1 2 126 heiborlem1 ( ( ( 𝐹 ‘ ( ( 2nd𝑥 ) + 1 ) ) ∈ Fin ∧ ( 𝐵𝑥 ) ⊆ 𝑡 ∈ ( 𝐹 ‘ ( ( 2nd𝑥 ) + 1 ) ) ( ( 𝐵𝑥 ) ∩ ( 𝑡 𝐵 ( ( 2nd𝑥 ) + 1 ) ) ) ∧ ( 𝐵𝑥 ) ∈ 𝐾 ) → ∃ 𝑡 ∈ ( 𝐹 ‘ ( ( 2nd𝑥 ) + 1 ) ) ( ( 𝐵𝑥 ) ∩ ( 𝑡 𝐵 ( ( 2nd𝑥 ) + 1 ) ) ) ∈ 𝐾 )
128 67 121 124 127 syl3anc ( ( 𝜑𝑥𝐺 ) → ∃ 𝑡 ∈ ( 𝐹 ‘ ( ( 2nd𝑥 ) + 1 ) ) ( ( 𝐵𝑥 ) ∩ ( 𝑡 𝐵 ( ( 2nd𝑥 ) + 1 ) ) ) ∈ 𝐾 )
129 85 66 sseldi ( ( 𝜑𝑥𝐺 ) → ( 𝐹 ‘ ( ( 2nd𝑥 ) + 1 ) ) ∈ 𝒫 𝑋 )
130 129 elpwid ( ( 𝜑𝑥𝐺 ) → ( 𝐹 ‘ ( ( 2nd𝑥 ) + 1 ) ) ⊆ 𝑋 )
131 1 mopnuni ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝑋 = 𝐽 )
132 105 131 syl ( 𝜑𝑋 = 𝐽 )
133 132 adantr ( ( 𝜑𝑥𝐺 ) → 𝑋 = 𝐽 )
134 130 133 sseqtrd ( ( 𝜑𝑥𝐺 ) → ( 𝐹 ‘ ( ( 2nd𝑥 ) + 1 ) ) ⊆ 𝐽 )
135 134 sselda ( ( ( 𝜑𝑥𝐺 ) ∧ 𝑡 ∈ ( 𝐹 ‘ ( ( 2nd𝑥 ) + 1 ) ) ) → 𝑡 𝐽 )
136 135 adantrr ( ( ( 𝜑𝑥𝐺 ) ∧ ( 𝑡 ∈ ( 𝐹 ‘ ( ( 2nd𝑥 ) + 1 ) ) ∧ ( ( 𝐵𝑥 ) ∩ ( 𝑡 𝐵 ( ( 2nd𝑥 ) + 1 ) ) ) ∈ 𝐾 ) ) → 𝑡 𝐽 )
137 64 adantl ( ( 𝜑𝑥𝐺 ) → ( ( 2nd𝑥 ) + 1 ) ∈ ℕ0 )
138 id ( 𝑡 ∈ ( 𝐹 ‘ ( ( 2nd𝑥 ) + 1 ) ) → 𝑡 ∈ ( 𝐹 ‘ ( ( 2nd𝑥 ) + 1 ) ) )
139 snfi { ( 𝑡 𝐵 ( ( 2nd𝑥 ) + 1 ) ) } ∈ Fin
140 inss2 ( ( 𝐵𝑥 ) ∩ ( 𝑡 𝐵 ( ( 2nd𝑥 ) + 1 ) ) ) ⊆ ( 𝑡 𝐵 ( ( 2nd𝑥 ) + 1 ) )
141 ovex ( 𝑡 𝐵 ( ( 2nd𝑥 ) + 1 ) ) ∈ V
142 141 unisn { ( 𝑡 𝐵 ( ( 2nd𝑥 ) + 1 ) ) } = ( 𝑡 𝐵 ( ( 2nd𝑥 ) + 1 ) )
143 uniiun { ( 𝑡 𝐵 ( ( 2nd𝑥 ) + 1 ) ) } = 𝑔 ∈ { ( 𝑡 𝐵 ( ( 2nd𝑥 ) + 1 ) ) } 𝑔
144 142 143 eqtr3i ( 𝑡 𝐵 ( ( 2nd𝑥 ) + 1 ) ) = 𝑔 ∈ { ( 𝑡 𝐵 ( ( 2nd𝑥 ) + 1 ) ) } 𝑔
145 140 144 sseqtri ( ( 𝐵𝑥 ) ∩ ( 𝑡 𝐵 ( ( 2nd𝑥 ) + 1 ) ) ) ⊆ 𝑔 ∈ { ( 𝑡 𝐵 ( ( 2nd𝑥 ) + 1 ) ) } 𝑔
146 vex 𝑔 ∈ V
147 1 2 146 heiborlem1 ( ( { ( 𝑡 𝐵 ( ( 2nd𝑥 ) + 1 ) ) } ∈ Fin ∧ ( ( 𝐵𝑥 ) ∩ ( 𝑡 𝐵 ( ( 2nd𝑥 ) + 1 ) ) ) ⊆ 𝑔 ∈ { ( 𝑡 𝐵 ( ( 2nd𝑥 ) + 1 ) ) } 𝑔 ∧ ( ( 𝐵𝑥 ) ∩ ( 𝑡 𝐵 ( ( 2nd𝑥 ) + 1 ) ) ) ∈ 𝐾 ) → ∃ 𝑔 ∈ { ( 𝑡 𝐵 ( ( 2nd𝑥 ) + 1 ) ) } 𝑔𝐾 )
148 139 145 147 mp3an12 ( ( ( 𝐵𝑥 ) ∩ ( 𝑡 𝐵 ( ( 2nd𝑥 ) + 1 ) ) ) ∈ 𝐾 → ∃ 𝑔 ∈ { ( 𝑡 𝐵 ( ( 2nd𝑥 ) + 1 ) ) } 𝑔𝐾 )
149 eleq1 ( 𝑔 = ( 𝑡 𝐵 ( ( 2nd𝑥 ) + 1 ) ) → ( 𝑔𝐾 ↔ ( 𝑡 𝐵 ( ( 2nd𝑥 ) + 1 ) ) ∈ 𝐾 ) )
150 141 149 rexsn ( ∃ 𝑔 ∈ { ( 𝑡 𝐵 ( ( 2nd𝑥 ) + 1 ) ) } 𝑔𝐾 ↔ ( 𝑡 𝐵 ( ( 2nd𝑥 ) + 1 ) ) ∈ 𝐾 )
151 148 150 sylib ( ( ( 𝐵𝑥 ) ∩ ( 𝑡 𝐵 ( ( 2nd𝑥 ) + 1 ) ) ) ∈ 𝐾 → ( 𝑡 𝐵 ( ( 2nd𝑥 ) + 1 ) ) ∈ 𝐾 )
152 ovex ( ( 2nd𝑥 ) + 1 ) ∈ V
153 1 2 3 46 152 heiborlem2 ( 𝑡 𝐺 ( ( 2nd𝑥 ) + 1 ) ↔ ( ( ( 2nd𝑥 ) + 1 ) ∈ ℕ0𝑡 ∈ ( 𝐹 ‘ ( ( 2nd𝑥 ) + 1 ) ) ∧ ( 𝑡 𝐵 ( ( 2nd𝑥 ) + 1 ) ) ∈ 𝐾 ) )
154 153 biimpri ( ( ( ( 2nd𝑥 ) + 1 ) ∈ ℕ0𝑡 ∈ ( 𝐹 ‘ ( ( 2nd𝑥 ) + 1 ) ) ∧ ( 𝑡 𝐵 ( ( 2nd𝑥 ) + 1 ) ) ∈ 𝐾 ) → 𝑡 𝐺 ( ( 2nd𝑥 ) + 1 ) )
155 137 138 151 154 syl3an ( ( ( 𝜑𝑥𝐺 ) ∧ 𝑡 ∈ ( 𝐹 ‘ ( ( 2nd𝑥 ) + 1 ) ) ∧ ( ( 𝐵𝑥 ) ∩ ( 𝑡 𝐵 ( ( 2nd𝑥 ) + 1 ) ) ) ∈ 𝐾 ) → 𝑡 𝐺 ( ( 2nd𝑥 ) + 1 ) )
156 155 3expb ( ( ( 𝜑𝑥𝐺 ) ∧ ( 𝑡 ∈ ( 𝐹 ‘ ( ( 2nd𝑥 ) + 1 ) ) ∧ ( ( 𝐵𝑥 ) ∩ ( 𝑡 𝐵 ( ( 2nd𝑥 ) + 1 ) ) ) ∈ 𝐾 ) ) → 𝑡 𝐺 ( ( 2nd𝑥 ) + 1 ) )
157 simprr ( ( ( 𝜑𝑥𝐺 ) ∧ ( 𝑡 ∈ ( 𝐹 ‘ ( ( 2nd𝑥 ) + 1 ) ) ∧ ( ( 𝐵𝑥 ) ∩ ( 𝑡 𝐵 ( ( 2nd𝑥 ) + 1 ) ) ) ∈ 𝐾 ) ) → ( ( 𝐵𝑥 ) ∩ ( 𝑡 𝐵 ( ( 2nd𝑥 ) + 1 ) ) ) ∈ 𝐾 )
158 136 156 157 jca32 ( ( ( 𝜑𝑥𝐺 ) ∧ ( 𝑡 ∈ ( 𝐹 ‘ ( ( 2nd𝑥 ) + 1 ) ) ∧ ( ( 𝐵𝑥 ) ∩ ( 𝑡 𝐵 ( ( 2nd𝑥 ) + 1 ) ) ) ∈ 𝐾 ) ) → ( 𝑡 𝐽 ∧ ( 𝑡 𝐺 ( ( 2nd𝑥 ) + 1 ) ∧ ( ( 𝐵𝑥 ) ∩ ( 𝑡 𝐵 ( ( 2nd𝑥 ) + 1 ) ) ) ∈ 𝐾 ) ) )
159 158 ex ( ( 𝜑𝑥𝐺 ) → ( ( 𝑡 ∈ ( 𝐹 ‘ ( ( 2nd𝑥 ) + 1 ) ) ∧ ( ( 𝐵𝑥 ) ∩ ( 𝑡 𝐵 ( ( 2nd𝑥 ) + 1 ) ) ) ∈ 𝐾 ) → ( 𝑡 𝐽 ∧ ( 𝑡 𝐺 ( ( 2nd𝑥 ) + 1 ) ∧ ( ( 𝐵𝑥 ) ∩ ( 𝑡 𝐵 ( ( 2nd𝑥 ) + 1 ) ) ) ∈ 𝐾 ) ) ) )
160 159 reximdv2 ( ( 𝜑𝑥𝐺 ) → ( ∃ 𝑡 ∈ ( 𝐹 ‘ ( ( 2nd𝑥 ) + 1 ) ) ( ( 𝐵𝑥 ) ∩ ( 𝑡 𝐵 ( ( 2nd𝑥 ) + 1 ) ) ) ∈ 𝐾 → ∃ 𝑡 𝐽 ( 𝑡 𝐺 ( ( 2nd𝑥 ) + 1 ) ∧ ( ( 𝐵𝑥 ) ∩ ( 𝑡 𝐵 ( ( 2nd𝑥 ) + 1 ) ) ) ∈ 𝐾 ) ) )
161 128 160 mpd ( ( 𝜑𝑥𝐺 ) → ∃ 𝑡 𝐽 ( 𝑡 𝐺 ( ( 2nd𝑥 ) + 1 ) ∧ ( ( 𝐵𝑥 ) ∩ ( 𝑡 𝐵 ( ( 2nd𝑥 ) + 1 ) ) ) ∈ 𝐾 ) )
162 161 ralrimiva ( 𝜑 → ∀ 𝑥𝐺𝑡 𝐽 ( 𝑡 𝐺 ( ( 2nd𝑥 ) + 1 ) ∧ ( ( 𝐵𝑥 ) ∩ ( 𝑡 𝐵 ( ( 2nd𝑥 ) + 1 ) ) ) ∈ 𝐾 ) )
163 1 fvexi 𝐽 ∈ V
164 163 uniex 𝐽 ∈ V
165 breq1 ( 𝑡 = ( 𝑔𝑥 ) → ( 𝑡 𝐺 ( ( 2nd𝑥 ) + 1 ) ↔ ( 𝑔𝑥 ) 𝐺 ( ( 2nd𝑥 ) + 1 ) ) )
166 oveq1 ( 𝑡 = ( 𝑔𝑥 ) → ( 𝑡 𝐵 ( ( 2nd𝑥 ) + 1 ) ) = ( ( 𝑔𝑥 ) 𝐵 ( ( 2nd𝑥 ) + 1 ) ) )
167 166 ineq2d ( 𝑡 = ( 𝑔𝑥 ) → ( ( 𝐵𝑥 ) ∩ ( 𝑡 𝐵 ( ( 2nd𝑥 ) + 1 ) ) ) = ( ( 𝐵𝑥 ) ∩ ( ( 𝑔𝑥 ) 𝐵 ( ( 2nd𝑥 ) + 1 ) ) ) )
168 167 eleq1d ( 𝑡 = ( 𝑔𝑥 ) → ( ( ( 𝐵𝑥 ) ∩ ( 𝑡 𝐵 ( ( 2nd𝑥 ) + 1 ) ) ) ∈ 𝐾 ↔ ( ( 𝐵𝑥 ) ∩ ( ( 𝑔𝑥 ) 𝐵 ( ( 2nd𝑥 ) + 1 ) ) ) ∈ 𝐾 ) )
169 165 168 anbi12d ( 𝑡 = ( 𝑔𝑥 ) → ( ( 𝑡 𝐺 ( ( 2nd𝑥 ) + 1 ) ∧ ( ( 𝐵𝑥 ) ∩ ( 𝑡 𝐵 ( ( 2nd𝑥 ) + 1 ) ) ) ∈ 𝐾 ) ↔ ( ( 𝑔𝑥 ) 𝐺 ( ( 2nd𝑥 ) + 1 ) ∧ ( ( 𝐵𝑥 ) ∩ ( ( 𝑔𝑥 ) 𝐵 ( ( 2nd𝑥 ) + 1 ) ) ) ∈ 𝐾 ) ) )
170 164 169 axcc4dom ( ( 𝐺 ≼ ω ∧ ∀ 𝑥𝐺𝑡 𝐽 ( 𝑡 𝐺 ( ( 2nd𝑥 ) + 1 ) ∧ ( ( 𝐵𝑥 ) ∩ ( 𝑡 𝐵 ( ( 2nd𝑥 ) + 1 ) ) ) ∈ 𝐾 ) ) → ∃ 𝑔 ( 𝑔 : 𝐺 𝐽 ∧ ∀ 𝑥𝐺 ( ( 𝑔𝑥 ) 𝐺 ( ( 2nd𝑥 ) + 1 ) ∧ ( ( 𝐵𝑥 ) ∩ ( ( 𝑔𝑥 ) 𝐵 ( ( 2nd𝑥 ) + 1 ) ) ) ∈ 𝐾 ) ) )
171 61 162 170 syl2anc ( 𝜑 → ∃ 𝑔 ( 𝑔 : 𝐺 𝐽 ∧ ∀ 𝑥𝐺 ( ( 𝑔𝑥 ) 𝐺 ( ( 2nd𝑥 ) + 1 ) ∧ ( ( 𝐵𝑥 ) ∩ ( ( 𝑔𝑥 ) 𝐵 ( ( 2nd𝑥 ) + 1 ) ) ) ∈ 𝐾 ) ) )
172 exsimpr ( ∃ 𝑔 ( 𝑔 : 𝐺 𝐽 ∧ ∀ 𝑥𝐺 ( ( 𝑔𝑥 ) 𝐺 ( ( 2nd𝑥 ) + 1 ) ∧ ( ( 𝐵𝑥 ) ∩ ( ( 𝑔𝑥 ) 𝐵 ( ( 2nd𝑥 ) + 1 ) ) ) ∈ 𝐾 ) ) → ∃ 𝑔𝑥𝐺 ( ( 𝑔𝑥 ) 𝐺 ( ( 2nd𝑥 ) + 1 ) ∧ ( ( 𝐵𝑥 ) ∩ ( ( 𝑔𝑥 ) 𝐵 ( ( 2nd𝑥 ) + 1 ) ) ) ∈ 𝐾 ) )
173 171 172 syl ( 𝜑 → ∃ 𝑔𝑥𝐺 ( ( 𝑔𝑥 ) 𝐺 ( ( 2nd𝑥 ) + 1 ) ∧ ( ( 𝐵𝑥 ) ∩ ( ( 𝑔𝑥 ) 𝐵 ( ( 2nd𝑥 ) + 1 ) ) ) ∈ 𝐾 ) )