Users' Mathboxes Mathbox for Jeff Madsen < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  heiborlem3 Structured version   Visualization version   GIF version

Theorem heiborlem3 36322
Description: Lemma for heibor 36330. Using countable choice ax-cc 10379, we have fixed in advance a collection of finite 2↑-𝑛 nets (πΉβ€˜π‘›) for 𝑋 (note that an π‘Ÿ-net is a set of points in 𝑋 whose π‘Ÿ -balls cover 𝑋). The set 𝐺 is the subset of these points whose corresponding balls have no finite subcover (i.e. in the set 𝐾). If the theorem was false, then 𝑋 would be in 𝐾, and so some ball at each level would also be in 𝐾. But we can say more than this; given a ball (𝑦𝐡𝑛) on level 𝑛, since level 𝑛 + 1 covers the space and thus also (𝑦𝐡𝑛), using heiborlem1 36320 there is a ball on the next level whose intersection with (𝑦𝐡𝑛) also has no finite subcover. Now since the set 𝐺 is a countable union of finite sets, it is countable (which needs ax-cc 10379 via iunctb 10518), and so we can apply ax-cc 10379 to 𝐺 directly to get a function from 𝐺 to itself, which points from each ball in 𝐾 to a ball on the next level in 𝐾, and such that the intersection between these balls is also in 𝐾. (Contributed by Jeff Madsen, 18-Jan-2014.)
Hypotheses
Ref Expression
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
Ref Expression
heiborlem3 (πœ‘ β†’ βˆƒπ‘”βˆ€π‘₯ ∈ 𝐺 ((π‘”β€˜π‘₯)𝐺((2nd β€˜π‘₯) + 1) ∧ ((π΅β€˜π‘₯) ∩ ((π‘”β€˜π‘₯)𝐡((2nd β€˜π‘₯) + 1))) ∈ 𝐾))
Distinct variable groups:   π‘₯,𝑛,𝑦,𝑒,𝐹   π‘₯,𝑔,𝐺   πœ‘,𝑔,π‘₯   𝑔,π‘š,𝑛,𝑒,𝑣,𝑦,𝑧,𝐷,π‘₯   𝐡,𝑔,𝑛,𝑒,𝑣,𝑦   𝑔,𝐽,π‘š,𝑛,𝑒,𝑣,π‘₯,𝑦,𝑧   π‘ˆ,𝑔,𝑛,𝑒,𝑣,π‘₯,𝑦,𝑧   𝑔,𝑋,π‘š,𝑛,𝑒,𝑣,π‘₯,𝑦,𝑧   𝑔,𝐾,𝑛,π‘₯,𝑦,𝑧   π‘₯,𝐡
Allowed substitution hints:   πœ‘(𝑦,𝑧,𝑣,𝑒,π‘š,𝑛)   𝐡(𝑧,π‘š)   π‘ˆ(π‘š)   𝐹(𝑧,𝑣,𝑔,π‘š)   𝐺(𝑦,𝑧,𝑣,𝑒,π‘š,𝑛)   𝐾(𝑣,𝑒,π‘š)

Proof of Theorem heiborlem3
Dummy variable 𝑑 is distinct from all other variables.
StepHypRef Expression
1 nn0ex 12427 . . . . . 6 β„•0 ∈ V
2 fvex 6859 . . . . . . 7 (πΉβ€˜π‘‘) ∈ V
3 vsnex 5390 . . . . . . 7 {𝑑} ∈ V
42, 3xpex 7691 . . . . . 6 ((πΉβ€˜π‘‘) Γ— {𝑑}) ∈ V
51, 4iunex 7905 . . . . 5 βˆͺ 𝑑 ∈ β„•0 ((πΉβ€˜π‘‘) Γ— {𝑑}) ∈ V
6 heibor.4 . . . . . . . . 9 𝐺 = {βŸ¨π‘¦, π‘›βŸ© ∣ (𝑛 ∈ β„•0 ∧ 𝑦 ∈ (πΉβ€˜π‘›) ∧ (𝑦𝐡𝑛) ∈ 𝐾)}
76relopabiv 5780 . . . . . . . 8 Rel 𝐺
8 1st2nd 7975 . . . . . . . 8 ((Rel 𝐺 ∧ π‘₯ ∈ 𝐺) β†’ π‘₯ = ⟨(1st β€˜π‘₯), (2nd β€˜π‘₯)⟩)
97, 8mpan 689 . . . . . . 7 (π‘₯ ∈ 𝐺 β†’ π‘₯ = ⟨(1st β€˜π‘₯), (2nd β€˜π‘₯)⟩)
109eleq1d 2819 . . . . . . . . . . 11 (π‘₯ ∈ 𝐺 β†’ (π‘₯ ∈ 𝐺 ↔ ⟨(1st β€˜π‘₯), (2nd β€˜π‘₯)⟩ ∈ 𝐺))
11 df-br 5110 . . . . . . . . . . 11 ((1st β€˜π‘₯)𝐺(2nd β€˜π‘₯) ↔ ⟨(1st β€˜π‘₯), (2nd β€˜π‘₯)⟩ ∈ 𝐺)
1210, 11bitr4di 289 . . . . . . . . . 10 (π‘₯ ∈ 𝐺 β†’ (π‘₯ ∈ 𝐺 ↔ (1st β€˜π‘₯)𝐺(2nd β€˜π‘₯)))
13 heibor.1 . . . . . . . . . . 11 𝐽 = (MetOpenβ€˜π·)
14 heibor.3 . . . . . . . . . . 11 𝐾 = {𝑒 ∣ Β¬ βˆƒπ‘£ ∈ (𝒫 π‘ˆ ∩ Fin)𝑒 βŠ† βˆͺ 𝑣}
15 fvex 6859 . . . . . . . . . . 11 (1st β€˜π‘₯) ∈ V
16 fvex 6859 . . . . . . . . . . 11 (2nd β€˜π‘₯) ∈ V
1713, 14, 6, 15, 16heiborlem2 36321 . . . . . . . . . 10 ((1st β€˜π‘₯)𝐺(2nd β€˜π‘₯) ↔ ((2nd β€˜π‘₯) ∈ β„•0 ∧ (1st β€˜π‘₯) ∈ (πΉβ€˜(2nd β€˜π‘₯)) ∧ ((1st β€˜π‘₯)𝐡(2nd β€˜π‘₯)) ∈ 𝐾))
1812, 17bitrdi 287 . . . . . . . . 9 (π‘₯ ∈ 𝐺 β†’ (π‘₯ ∈ 𝐺 ↔ ((2nd β€˜π‘₯) ∈ β„•0 ∧ (1st β€˜π‘₯) ∈ (πΉβ€˜(2nd β€˜π‘₯)) ∧ ((1st β€˜π‘₯)𝐡(2nd β€˜π‘₯)) ∈ 𝐾)))
1918ibi 267 . . . . . . . 8 (π‘₯ ∈ 𝐺 β†’ ((2nd β€˜π‘₯) ∈ β„•0 ∧ (1st β€˜π‘₯) ∈ (πΉβ€˜(2nd β€˜π‘₯)) ∧ ((1st β€˜π‘₯)𝐡(2nd β€˜π‘₯)) ∈ 𝐾))
2016snid 4626 . . . . . . . . . . . 12 (2nd β€˜π‘₯) ∈ {(2nd β€˜π‘₯)}
21 opelxp 5673 . . . . . . . . . . . 12 (⟨(1st β€˜π‘₯), (2nd β€˜π‘₯)⟩ ∈ ((πΉβ€˜(2nd β€˜π‘₯)) Γ— {(2nd β€˜π‘₯)}) ↔ ((1st β€˜π‘₯) ∈ (πΉβ€˜(2nd β€˜π‘₯)) ∧ (2nd β€˜π‘₯) ∈ {(2nd β€˜π‘₯)}))
2220, 21mpbiran2 709 . . . . . . . . . . 11 (⟨(1st β€˜π‘₯), (2nd β€˜π‘₯)⟩ ∈ ((πΉβ€˜(2nd β€˜π‘₯)) Γ— {(2nd β€˜π‘₯)}) ↔ (1st β€˜π‘₯) ∈ (πΉβ€˜(2nd β€˜π‘₯)))
23 fveq2 6846 . . . . . . . . . . . . . 14 (𝑑 = (2nd β€˜π‘₯) β†’ (πΉβ€˜π‘‘) = (πΉβ€˜(2nd β€˜π‘₯)))
24 sneq 4600 . . . . . . . . . . . . . 14 (𝑑 = (2nd β€˜π‘₯) β†’ {𝑑} = {(2nd β€˜π‘₯)})
2523, 24xpeq12d 5668 . . . . . . . . . . . . 13 (𝑑 = (2nd β€˜π‘₯) β†’ ((πΉβ€˜π‘‘) Γ— {𝑑}) = ((πΉβ€˜(2nd β€˜π‘₯)) Γ— {(2nd β€˜π‘₯)}))
2625eleq2d 2820 . . . . . . . . . . . 12 (𝑑 = (2nd β€˜π‘₯) β†’ (⟨(1st β€˜π‘₯), (2nd β€˜π‘₯)⟩ ∈ ((πΉβ€˜π‘‘) Γ— {𝑑}) ↔ ⟨(1st β€˜π‘₯), (2nd β€˜π‘₯)⟩ ∈ ((πΉβ€˜(2nd β€˜π‘₯)) Γ— {(2nd β€˜π‘₯)})))
2726rspcev 3583 . . . . . . . . . . 11 (((2nd β€˜π‘₯) ∈ β„•0 ∧ ⟨(1st β€˜π‘₯), (2nd β€˜π‘₯)⟩ ∈ ((πΉβ€˜(2nd β€˜π‘₯)) Γ— {(2nd β€˜π‘₯)})) β†’ βˆƒπ‘‘ ∈ β„•0 ⟨(1st β€˜π‘₯), (2nd β€˜π‘₯)⟩ ∈ ((πΉβ€˜π‘‘) Γ— {𝑑}))
2822, 27sylan2br 596 . . . . . . . . . 10 (((2nd β€˜π‘₯) ∈ β„•0 ∧ (1st β€˜π‘₯) ∈ (πΉβ€˜(2nd β€˜π‘₯))) β†’ βˆƒπ‘‘ ∈ β„•0 ⟨(1st β€˜π‘₯), (2nd β€˜π‘₯)⟩ ∈ ((πΉβ€˜π‘‘) Γ— {𝑑}))
29 eliun 4962 . . . . . . . . . 10 (⟨(1st β€˜π‘₯), (2nd β€˜π‘₯)⟩ ∈ βˆͺ 𝑑 ∈ β„•0 ((πΉβ€˜π‘‘) Γ— {𝑑}) ↔ βˆƒπ‘‘ ∈ β„•0 ⟨(1st β€˜π‘₯), (2nd β€˜π‘₯)⟩ ∈ ((πΉβ€˜π‘‘) Γ— {𝑑}))
3028, 29sylibr 233 . . . . . . . . 9 (((2nd β€˜π‘₯) ∈ β„•0 ∧ (1st β€˜π‘₯) ∈ (πΉβ€˜(2nd β€˜π‘₯))) β†’ ⟨(1st β€˜π‘₯), (2nd β€˜π‘₯)⟩ ∈ βˆͺ 𝑑 ∈ β„•0 ((πΉβ€˜π‘‘) Γ— {𝑑}))
31303adant3 1133 . . . . . . . 8 (((2nd β€˜π‘₯) ∈ β„•0 ∧ (1st β€˜π‘₯) ∈ (πΉβ€˜(2nd β€˜π‘₯)) ∧ ((1st β€˜π‘₯)𝐡(2nd β€˜π‘₯)) ∈ 𝐾) β†’ ⟨(1st β€˜π‘₯), (2nd β€˜π‘₯)⟩ ∈ βˆͺ 𝑑 ∈ β„•0 ((πΉβ€˜π‘‘) Γ— {𝑑}))
3219, 31syl 17 . . . . . . 7 (π‘₯ ∈ 𝐺 β†’ ⟨(1st β€˜π‘₯), (2nd β€˜π‘₯)⟩ ∈ βˆͺ 𝑑 ∈ β„•0 ((πΉβ€˜π‘‘) Γ— {𝑑}))
339, 32eqeltrd 2834 . . . . . 6 (π‘₯ ∈ 𝐺 β†’ π‘₯ ∈ βˆͺ 𝑑 ∈ β„•0 ((πΉβ€˜π‘‘) Γ— {𝑑}))
3433ssriv 3952 . . . . 5 𝐺 βŠ† βˆͺ 𝑑 ∈ β„•0 ((πΉβ€˜π‘‘) Γ— {𝑑})
35 ssdomg 8946 . . . . 5 (βˆͺ 𝑑 ∈ β„•0 ((πΉβ€˜π‘‘) Γ— {𝑑}) ∈ V β†’ (𝐺 βŠ† βˆͺ 𝑑 ∈ β„•0 ((πΉβ€˜π‘‘) Γ— {𝑑}) β†’ 𝐺 β‰Ό βˆͺ 𝑑 ∈ β„•0 ((πΉβ€˜π‘‘) Γ— {𝑑})))
365, 34, 35mp2 9 . . . 4 𝐺 β‰Ό βˆͺ 𝑑 ∈ β„•0 ((πΉβ€˜π‘‘) Γ— {𝑑})
37 nn0ennn 13893 . . . . . . 7 β„•0 β‰ˆ β„•
38 nnenom 13894 . . . . . . 7 β„• β‰ˆ Ο‰
3937, 38entri 8954 . . . . . 6 β„•0 β‰ˆ Ο‰
40 endom 8925 . . . . . 6 (β„•0 β‰ˆ Ο‰ β†’ β„•0 β‰Ό Ο‰)
4139, 40ax-mp 5 . . . . 5 β„•0 β‰Ό Ο‰
42 vex 3451 . . . . . . . 8 𝑑 ∈ V
432, 42xpsnen 9005 . . . . . . 7 ((πΉβ€˜π‘‘) Γ— {𝑑}) β‰ˆ (πΉβ€˜π‘‘)
44 inss2 4193 . . . . . . . . 9 (𝒫 𝑋 ∩ Fin) βŠ† Fin
45 heibor.7 . . . . . . . . . 10 (πœ‘ β†’ 𝐹:β„•0⟢(𝒫 𝑋 ∩ Fin))
4645ffvelcdmda 7039 . . . . . . . . 9 ((πœ‘ ∧ 𝑑 ∈ β„•0) β†’ (πΉβ€˜π‘‘) ∈ (𝒫 𝑋 ∩ Fin))
4744, 46sselid 3946 . . . . . . . 8 ((πœ‘ ∧ 𝑑 ∈ β„•0) β†’ (πΉβ€˜π‘‘) ∈ Fin)
48 isfinite 9596 . . . . . . . . 9 ((πΉβ€˜π‘‘) ∈ Fin ↔ (πΉβ€˜π‘‘) β‰Ί Ο‰)
49 sdomdom 8926 . . . . . . . . 9 ((πΉβ€˜π‘‘) β‰Ί Ο‰ β†’ (πΉβ€˜π‘‘) β‰Ό Ο‰)
5048, 49sylbi 216 . . . . . . . 8 ((πΉβ€˜π‘‘) ∈ Fin β†’ (πΉβ€˜π‘‘) β‰Ό Ο‰)
5147, 50syl 17 . . . . . . 7 ((πœ‘ ∧ 𝑑 ∈ β„•0) β†’ (πΉβ€˜π‘‘) β‰Ό Ο‰)
52 endomtr 8958 . . . . . . 7 ((((πΉβ€˜π‘‘) Γ— {𝑑}) β‰ˆ (πΉβ€˜π‘‘) ∧ (πΉβ€˜π‘‘) β‰Ό Ο‰) β†’ ((πΉβ€˜π‘‘) Γ— {𝑑}) β‰Ό Ο‰)
5343, 51, 52sylancr 588 . . . . . 6 ((πœ‘ ∧ 𝑑 ∈ β„•0) β†’ ((πΉβ€˜π‘‘) Γ— {𝑑}) β‰Ό Ο‰)
5453ralrimiva 3140 . . . . 5 (πœ‘ β†’ βˆ€π‘‘ ∈ β„•0 ((πΉβ€˜π‘‘) Γ— {𝑑}) β‰Ό Ο‰)
55 iunctb 10518 . . . . 5 ((β„•0 β‰Ό Ο‰ ∧ βˆ€π‘‘ ∈ β„•0 ((πΉβ€˜π‘‘) Γ— {𝑑}) β‰Ό Ο‰) β†’ βˆͺ 𝑑 ∈ β„•0 ((πΉβ€˜π‘‘) Γ— {𝑑}) β‰Ό Ο‰)
5641, 54, 55sylancr 588 . . . 4 (πœ‘ β†’ βˆͺ 𝑑 ∈ β„•0 ((πΉβ€˜π‘‘) Γ— {𝑑}) β‰Ό Ο‰)
57 domtr 8953 . . . 4 ((𝐺 β‰Ό βˆͺ 𝑑 ∈ β„•0 ((πΉβ€˜π‘‘) Γ— {𝑑}) ∧ βˆͺ 𝑑 ∈ β„•0 ((πΉβ€˜π‘‘) Γ— {𝑑}) β‰Ό Ο‰) β†’ 𝐺 β‰Ό Ο‰)
5836, 56, 57sylancr 588 . . 3 (πœ‘ β†’ 𝐺 β‰Ό Ο‰)
5919simp1d 1143 . . . . . . . . 9 (π‘₯ ∈ 𝐺 β†’ (2nd β€˜π‘₯) ∈ β„•0)
60 peano2nn0 12461 . . . . . . . . 9 ((2nd β€˜π‘₯) ∈ β„•0 β†’ ((2nd β€˜π‘₯) + 1) ∈ β„•0)
6159, 60syl 17 . . . . . . . 8 (π‘₯ ∈ 𝐺 β†’ ((2nd β€˜π‘₯) + 1) ∈ β„•0)
62 ffvelcdm 7036 . . . . . . . 8 ((𝐹:β„•0⟢(𝒫 𝑋 ∩ Fin) ∧ ((2nd β€˜π‘₯) + 1) ∈ β„•0) β†’ (πΉβ€˜((2nd β€˜π‘₯) + 1)) ∈ (𝒫 𝑋 ∩ Fin))
6345, 61, 62syl2an 597 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ 𝐺) β†’ (πΉβ€˜((2nd β€˜π‘₯) + 1)) ∈ (𝒫 𝑋 ∩ Fin))
6444, 63sselid 3946 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ 𝐺) β†’ (πΉβ€˜((2nd β€˜π‘₯) + 1)) ∈ Fin)
65 iunin2 5035 . . . . . . . 8 βˆͺ 𝑑 ∈ (πΉβ€˜((2nd β€˜π‘₯) + 1))((π΅β€˜π‘₯) ∩ (𝑑𝐡((2nd β€˜π‘₯) + 1))) = ((π΅β€˜π‘₯) ∩ βˆͺ 𝑑 ∈ (πΉβ€˜((2nd β€˜π‘₯) + 1))(𝑑𝐡((2nd β€˜π‘₯) + 1)))
66 heibor.8 . . . . . . . . . . 11 (πœ‘ β†’ βˆ€π‘› ∈ β„•0 𝑋 = βˆͺ 𝑦 ∈ (πΉβ€˜π‘›)(𝑦𝐡𝑛))
67 oveq1 7368 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑑 β†’ (𝑦𝐡𝑛) = (𝑑𝐡𝑛))
6867cbviunv 5004 . . . . . . . . . . . . . . 15 βˆͺ 𝑦 ∈ (πΉβ€˜π‘›)(𝑦𝐡𝑛) = βˆͺ 𝑑 ∈ (πΉβ€˜π‘›)(𝑑𝐡𝑛)
69 fveq2 6846 . . . . . . . . . . . . . . . 16 (𝑛 = ((2nd β€˜π‘₯) + 1) β†’ (πΉβ€˜π‘›) = (πΉβ€˜((2nd β€˜π‘₯) + 1)))
7069iuneq1d 4985 . . . . . . . . . . . . . . 15 (𝑛 = ((2nd β€˜π‘₯) + 1) β†’ βˆͺ 𝑑 ∈ (πΉβ€˜π‘›)(𝑑𝐡𝑛) = βˆͺ 𝑑 ∈ (πΉβ€˜((2nd β€˜π‘₯) + 1))(𝑑𝐡𝑛))
7168, 70eqtrid 2785 . . . . . . . . . . . . . 14 (𝑛 = ((2nd β€˜π‘₯) + 1) β†’ βˆͺ 𝑦 ∈ (πΉβ€˜π‘›)(𝑦𝐡𝑛) = βˆͺ 𝑑 ∈ (πΉβ€˜((2nd β€˜π‘₯) + 1))(𝑑𝐡𝑛))
72 oveq2 7369 . . . . . . . . . . . . . . 15 (𝑛 = ((2nd β€˜π‘₯) + 1) β†’ (𝑑𝐡𝑛) = (𝑑𝐡((2nd β€˜π‘₯) + 1)))
7372iuneq2d 4987 . . . . . . . . . . . . . 14 (𝑛 = ((2nd β€˜π‘₯) + 1) β†’ βˆͺ 𝑑 ∈ (πΉβ€˜((2nd β€˜π‘₯) + 1))(𝑑𝐡𝑛) = βˆͺ 𝑑 ∈ (πΉβ€˜((2nd β€˜π‘₯) + 1))(𝑑𝐡((2nd β€˜π‘₯) + 1)))
7471, 73eqtrd 2773 . . . . . . . . . . . . 13 (𝑛 = ((2nd β€˜π‘₯) + 1) β†’ βˆͺ 𝑦 ∈ (πΉβ€˜π‘›)(𝑦𝐡𝑛) = βˆͺ 𝑑 ∈ (πΉβ€˜((2nd β€˜π‘₯) + 1))(𝑑𝐡((2nd β€˜π‘₯) + 1)))
7574eqeq2d 2744 . . . . . . . . . . . 12 (𝑛 = ((2nd β€˜π‘₯) + 1) β†’ (𝑋 = βˆͺ 𝑦 ∈ (πΉβ€˜π‘›)(𝑦𝐡𝑛) ↔ 𝑋 = βˆͺ 𝑑 ∈ (πΉβ€˜((2nd β€˜π‘₯) + 1))(𝑑𝐡((2nd β€˜π‘₯) + 1))))
7675rspccva 3582 . . . . . . . . . . 11 ((βˆ€π‘› ∈ β„•0 𝑋 = βˆͺ 𝑦 ∈ (πΉβ€˜π‘›)(𝑦𝐡𝑛) ∧ ((2nd β€˜π‘₯) + 1) ∈ β„•0) β†’ 𝑋 = βˆͺ 𝑑 ∈ (πΉβ€˜((2nd β€˜π‘₯) + 1))(𝑑𝐡((2nd β€˜π‘₯) + 1)))
7766, 61, 76syl2an 597 . . . . . . . . . 10 ((πœ‘ ∧ π‘₯ ∈ 𝐺) β†’ 𝑋 = βˆͺ 𝑑 ∈ (πΉβ€˜((2nd β€˜π‘₯) + 1))(𝑑𝐡((2nd β€˜π‘₯) + 1)))
7877ineq2d 4176 . . . . . . . . 9 ((πœ‘ ∧ π‘₯ ∈ 𝐺) β†’ ((π΅β€˜π‘₯) ∩ 𝑋) = ((π΅β€˜π‘₯) ∩ βˆͺ 𝑑 ∈ (πΉβ€˜((2nd β€˜π‘₯) + 1))(𝑑𝐡((2nd β€˜π‘₯) + 1))))
799fveq2d 6850 . . . . . . . . . . . . . 14 (π‘₯ ∈ 𝐺 β†’ (π΅β€˜π‘₯) = (π΅β€˜βŸ¨(1st β€˜π‘₯), (2nd β€˜π‘₯)⟩))
80 df-ov 7364 . . . . . . . . . . . . . 14 ((1st β€˜π‘₯)𝐡(2nd β€˜π‘₯)) = (π΅β€˜βŸ¨(1st β€˜π‘₯), (2nd β€˜π‘₯)⟩)
8179, 80eqtr4di 2791 . . . . . . . . . . . . 13 (π‘₯ ∈ 𝐺 β†’ (π΅β€˜π‘₯) = ((1st β€˜π‘₯)𝐡(2nd β€˜π‘₯)))
8281adantl 483 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘₯ ∈ 𝐺) β†’ (π΅β€˜π‘₯) = ((1st β€˜π‘₯)𝐡(2nd β€˜π‘₯)))
83 inss1 4192 . . . . . . . . . . . . . . . 16 (𝒫 𝑋 ∩ Fin) βŠ† 𝒫 𝑋
84 ffvelcdm 7036 . . . . . . . . . . . . . . . . 17 ((𝐹:β„•0⟢(𝒫 𝑋 ∩ Fin) ∧ (2nd β€˜π‘₯) ∈ β„•0) β†’ (πΉβ€˜(2nd β€˜π‘₯)) ∈ (𝒫 𝑋 ∩ Fin))
8545, 59, 84syl2an 597 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘₯ ∈ 𝐺) β†’ (πΉβ€˜(2nd β€˜π‘₯)) ∈ (𝒫 𝑋 ∩ Fin))
8683, 85sselid 3946 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘₯ ∈ 𝐺) β†’ (πΉβ€˜(2nd β€˜π‘₯)) ∈ 𝒫 𝑋)
8786elpwid 4573 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘₯ ∈ 𝐺) β†’ (πΉβ€˜(2nd β€˜π‘₯)) βŠ† 𝑋)
8819simp2d 1144 . . . . . . . . . . . . . . 15 (π‘₯ ∈ 𝐺 β†’ (1st β€˜π‘₯) ∈ (πΉβ€˜(2nd β€˜π‘₯)))
8988adantl 483 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘₯ ∈ 𝐺) β†’ (1st β€˜π‘₯) ∈ (πΉβ€˜(2nd β€˜π‘₯)))
9087, 89sseldd 3949 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘₯ ∈ 𝐺) β†’ (1st β€˜π‘₯) ∈ 𝑋)
9159adantl 483 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘₯ ∈ 𝐺) β†’ (2nd β€˜π‘₯) ∈ β„•0)
92 oveq1 7368 . . . . . . . . . . . . . 14 (𝑧 = (1st β€˜π‘₯) β†’ (𝑧(ballβ€˜π·)(1 / (2β†‘π‘š))) = ((1st β€˜π‘₯)(ballβ€˜π·)(1 / (2β†‘π‘š))))
93 oveq2 7369 . . . . . . . . . . . . . . . 16 (π‘š = (2nd β€˜π‘₯) β†’ (2β†‘π‘š) = (2↑(2nd β€˜π‘₯)))
9493oveq2d 7377 . . . . . . . . . . . . . . 15 (π‘š = (2nd β€˜π‘₯) β†’ (1 / (2β†‘π‘š)) = (1 / (2↑(2nd β€˜π‘₯))))
9594oveq2d 7377 . . . . . . . . . . . . . 14 (π‘š = (2nd β€˜π‘₯) β†’ ((1st β€˜π‘₯)(ballβ€˜π·)(1 / (2β†‘π‘š))) = ((1st β€˜π‘₯)(ballβ€˜π·)(1 / (2↑(2nd β€˜π‘₯)))))
96 heibor.5 . . . . . . . . . . . . . 14 𝐡 = (𝑧 ∈ 𝑋, π‘š ∈ β„•0 ↦ (𝑧(ballβ€˜π·)(1 / (2β†‘π‘š))))
97 ovex 7394 . . . . . . . . . . . . . 14 ((1st β€˜π‘₯)(ballβ€˜π·)(1 / (2↑(2nd β€˜π‘₯)))) ∈ V
9892, 95, 96, 97ovmpo 7519 . . . . . . . . . . . . 13 (((1st β€˜π‘₯) ∈ 𝑋 ∧ (2nd β€˜π‘₯) ∈ β„•0) β†’ ((1st β€˜π‘₯)𝐡(2nd β€˜π‘₯)) = ((1st β€˜π‘₯)(ballβ€˜π·)(1 / (2↑(2nd β€˜π‘₯)))))
9990, 91, 98syl2anc 585 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘₯ ∈ 𝐺) β†’ ((1st β€˜π‘₯)𝐡(2nd β€˜π‘₯)) = ((1st β€˜π‘₯)(ballβ€˜π·)(1 / (2↑(2nd β€˜π‘₯)))))
10082, 99eqtrd 2773 . . . . . . . . . . 11 ((πœ‘ ∧ π‘₯ ∈ 𝐺) β†’ (π΅β€˜π‘₯) = ((1st β€˜π‘₯)(ballβ€˜π·)(1 / (2↑(2nd β€˜π‘₯)))))
101 heibor.6 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 𝐷 ∈ (CMetβ€˜π‘‹))
102 cmetmet 24673 . . . . . . . . . . . . . . 15 (𝐷 ∈ (CMetβ€˜π‘‹) β†’ 𝐷 ∈ (Metβ€˜π‘‹))
103101, 102syl 17 . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝐷 ∈ (Metβ€˜π‘‹))
104 metxmet 23710 . . . . . . . . . . . . . 14 (𝐷 ∈ (Metβ€˜π‘‹) β†’ 𝐷 ∈ (∞Metβ€˜π‘‹))
105103, 104syl 17 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝐷 ∈ (∞Metβ€˜π‘‹))
106105adantr 482 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘₯ ∈ 𝐺) β†’ 𝐷 ∈ (∞Metβ€˜π‘‹))
107 2nn 12234 . . . . . . . . . . . . . . . 16 2 ∈ β„•
108 nnexpcl 13989 . . . . . . . . . . . . . . . 16 ((2 ∈ β„• ∧ (2nd β€˜π‘₯) ∈ β„•0) β†’ (2↑(2nd β€˜π‘₯)) ∈ β„•)
109107, 91, 108sylancr 588 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘₯ ∈ 𝐺) β†’ (2↑(2nd β€˜π‘₯)) ∈ β„•)
110109nnrpd 12963 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘₯ ∈ 𝐺) β†’ (2↑(2nd β€˜π‘₯)) ∈ ℝ+)
111110rpreccld 12975 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘₯ ∈ 𝐺) β†’ (1 / (2↑(2nd β€˜π‘₯))) ∈ ℝ+)
112111rpxrd 12966 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘₯ ∈ 𝐺) β†’ (1 / (2↑(2nd β€˜π‘₯))) ∈ ℝ*)
113 blssm 23794 . . . . . . . . . . . 12 ((𝐷 ∈ (∞Metβ€˜π‘‹) ∧ (1st β€˜π‘₯) ∈ 𝑋 ∧ (1 / (2↑(2nd β€˜π‘₯))) ∈ ℝ*) β†’ ((1st β€˜π‘₯)(ballβ€˜π·)(1 / (2↑(2nd β€˜π‘₯)))) βŠ† 𝑋)
114106, 90, 112, 113syl3anc 1372 . . . . . . . . . . 11 ((πœ‘ ∧ π‘₯ ∈ 𝐺) β†’ ((1st β€˜π‘₯)(ballβ€˜π·)(1 / (2↑(2nd β€˜π‘₯)))) βŠ† 𝑋)
115100, 114eqsstrd 3986 . . . . . . . . . 10 ((πœ‘ ∧ π‘₯ ∈ 𝐺) β†’ (π΅β€˜π‘₯) βŠ† 𝑋)
116 df-ss 3931 . . . . . . . . . 10 ((π΅β€˜π‘₯) βŠ† 𝑋 ↔ ((π΅β€˜π‘₯) ∩ 𝑋) = (π΅β€˜π‘₯))
117115, 116sylib 217 . . . . . . . . 9 ((πœ‘ ∧ π‘₯ ∈ 𝐺) β†’ ((π΅β€˜π‘₯) ∩ 𝑋) = (π΅β€˜π‘₯))
11878, 117eqtr3d 2775 . . . . . . . 8 ((πœ‘ ∧ π‘₯ ∈ 𝐺) β†’ ((π΅β€˜π‘₯) ∩ βˆͺ 𝑑 ∈ (πΉβ€˜((2nd β€˜π‘₯) + 1))(𝑑𝐡((2nd β€˜π‘₯) + 1))) = (π΅β€˜π‘₯))
11965, 118eqtrid 2785 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ 𝐺) β†’ βˆͺ 𝑑 ∈ (πΉβ€˜((2nd β€˜π‘₯) + 1))((π΅β€˜π‘₯) ∩ (𝑑𝐡((2nd β€˜π‘₯) + 1))) = (π΅β€˜π‘₯))
120 eqimss2 4005 . . . . . . 7 (βˆͺ 𝑑 ∈ (πΉβ€˜((2nd β€˜π‘₯) + 1))((π΅β€˜π‘₯) ∩ (𝑑𝐡((2nd β€˜π‘₯) + 1))) = (π΅β€˜π‘₯) β†’ (π΅β€˜π‘₯) βŠ† βˆͺ 𝑑 ∈ (πΉβ€˜((2nd β€˜π‘₯) + 1))((π΅β€˜π‘₯) ∩ (𝑑𝐡((2nd β€˜π‘₯) + 1))))
121119, 120syl 17 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ 𝐺) β†’ (π΅β€˜π‘₯) βŠ† βˆͺ 𝑑 ∈ (πΉβ€˜((2nd β€˜π‘₯) + 1))((π΅β€˜π‘₯) ∩ (𝑑𝐡((2nd β€˜π‘₯) + 1))))
12219simp3d 1145 . . . . . . . 8 (π‘₯ ∈ 𝐺 β†’ ((1st β€˜π‘₯)𝐡(2nd β€˜π‘₯)) ∈ 𝐾)
12381, 122eqeltrd 2834 . . . . . . 7 (π‘₯ ∈ 𝐺 β†’ (π΅β€˜π‘₯) ∈ 𝐾)
124123adantl 483 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ 𝐺) β†’ (π΅β€˜π‘₯) ∈ 𝐾)
125 fvex 6859 . . . . . . . 8 (π΅β€˜π‘₯) ∈ V
126125inex1 5278 . . . . . . 7 ((π΅β€˜π‘₯) ∩ (𝑑𝐡((2nd β€˜π‘₯) + 1))) ∈ V
12713, 14, 126heiborlem1 36320 . . . . . 6 (((πΉβ€˜((2nd β€˜π‘₯) + 1)) ∈ Fin ∧ (π΅β€˜π‘₯) βŠ† βˆͺ 𝑑 ∈ (πΉβ€˜((2nd β€˜π‘₯) + 1))((π΅β€˜π‘₯) ∩ (𝑑𝐡((2nd β€˜π‘₯) + 1))) ∧ (π΅β€˜π‘₯) ∈ 𝐾) β†’ βˆƒπ‘‘ ∈ (πΉβ€˜((2nd β€˜π‘₯) + 1))((π΅β€˜π‘₯) ∩ (𝑑𝐡((2nd β€˜π‘₯) + 1))) ∈ 𝐾)
12864, 121, 124, 127syl3anc 1372 . . . . 5 ((πœ‘ ∧ π‘₯ ∈ 𝐺) β†’ βˆƒπ‘‘ ∈ (πΉβ€˜((2nd β€˜π‘₯) + 1))((π΅β€˜π‘₯) ∩ (𝑑𝐡((2nd β€˜π‘₯) + 1))) ∈ 𝐾)
12983, 63sselid 3946 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘₯ ∈ 𝐺) β†’ (πΉβ€˜((2nd β€˜π‘₯) + 1)) ∈ 𝒫 𝑋)
130129elpwid 4573 . . . . . . . . . . 11 ((πœ‘ ∧ π‘₯ ∈ 𝐺) β†’ (πΉβ€˜((2nd β€˜π‘₯) + 1)) βŠ† 𝑋)
13113mopnuni 23817 . . . . . . . . . . . . 13 (𝐷 ∈ (∞Metβ€˜π‘‹) β†’ 𝑋 = βˆͺ 𝐽)
132105, 131syl 17 . . . . . . . . . . . 12 (πœ‘ β†’ 𝑋 = βˆͺ 𝐽)
133132adantr 482 . . . . . . . . . . 11 ((πœ‘ ∧ π‘₯ ∈ 𝐺) β†’ 𝑋 = βˆͺ 𝐽)
134130, 133sseqtrd 3988 . . . . . . . . . 10 ((πœ‘ ∧ π‘₯ ∈ 𝐺) β†’ (πΉβ€˜((2nd β€˜π‘₯) + 1)) βŠ† βˆͺ 𝐽)
135134sselda 3948 . . . . . . . . 9 (((πœ‘ ∧ π‘₯ ∈ 𝐺) ∧ 𝑑 ∈ (πΉβ€˜((2nd β€˜π‘₯) + 1))) β†’ 𝑑 ∈ βˆͺ 𝐽)
136135adantrr 716 . . . . . . . 8 (((πœ‘ ∧ π‘₯ ∈ 𝐺) ∧ (𝑑 ∈ (πΉβ€˜((2nd β€˜π‘₯) + 1)) ∧ ((π΅β€˜π‘₯) ∩ (𝑑𝐡((2nd β€˜π‘₯) + 1))) ∈ 𝐾)) β†’ 𝑑 ∈ βˆͺ 𝐽)
13761adantl 483 . . . . . . . . . 10 ((πœ‘ ∧ π‘₯ ∈ 𝐺) β†’ ((2nd β€˜π‘₯) + 1) ∈ β„•0)
138 id 22 . . . . . . . . . 10 (𝑑 ∈ (πΉβ€˜((2nd β€˜π‘₯) + 1)) β†’ 𝑑 ∈ (πΉβ€˜((2nd β€˜π‘₯) + 1)))
139 snfi 8994 . . . . . . . . . . . 12 {(𝑑𝐡((2nd β€˜π‘₯) + 1))} ∈ Fin
140 inss2 4193 . . . . . . . . . . . . 13 ((π΅β€˜π‘₯) ∩ (𝑑𝐡((2nd β€˜π‘₯) + 1))) βŠ† (𝑑𝐡((2nd β€˜π‘₯) + 1))
141 ovex 7394 . . . . . . . . . . . . . . 15 (𝑑𝐡((2nd β€˜π‘₯) + 1)) ∈ V
142141unisn 4891 . . . . . . . . . . . . . 14 βˆͺ {(𝑑𝐡((2nd β€˜π‘₯) + 1))} = (𝑑𝐡((2nd β€˜π‘₯) + 1))
143 uniiun 5022 . . . . . . . . . . . . . 14 βˆͺ {(𝑑𝐡((2nd β€˜π‘₯) + 1))} = βˆͺ 𝑔 ∈ {(𝑑𝐡((2nd β€˜π‘₯) + 1))}𝑔
144142, 143eqtr3i 2763 . . . . . . . . . . . . 13 (𝑑𝐡((2nd β€˜π‘₯) + 1)) = βˆͺ 𝑔 ∈ {(𝑑𝐡((2nd β€˜π‘₯) + 1))}𝑔
145140, 144sseqtri 3984 . . . . . . . . . . . 12 ((π΅β€˜π‘₯) ∩ (𝑑𝐡((2nd β€˜π‘₯) + 1))) βŠ† βˆͺ 𝑔 ∈ {(𝑑𝐡((2nd β€˜π‘₯) + 1))}𝑔
146 vex 3451 . . . . . . . . . . . . 13 𝑔 ∈ V
14713, 14, 146heiborlem1 36320 . . . . . . . . . . . 12 (({(𝑑𝐡((2nd β€˜π‘₯) + 1))} ∈ Fin ∧ ((π΅β€˜π‘₯) ∩ (𝑑𝐡((2nd β€˜π‘₯) + 1))) βŠ† βˆͺ 𝑔 ∈ {(𝑑𝐡((2nd β€˜π‘₯) + 1))}𝑔 ∧ ((π΅β€˜π‘₯) ∩ (𝑑𝐡((2nd β€˜π‘₯) + 1))) ∈ 𝐾) β†’ βˆƒπ‘” ∈ {(𝑑𝐡((2nd β€˜π‘₯) + 1))}𝑔 ∈ 𝐾)
148139, 145, 147mp3an12 1452 . . . . . . . . . . 11 (((π΅β€˜π‘₯) ∩ (𝑑𝐡((2nd β€˜π‘₯) + 1))) ∈ 𝐾 β†’ βˆƒπ‘” ∈ {(𝑑𝐡((2nd β€˜π‘₯) + 1))}𝑔 ∈ 𝐾)
149 eleq1 2822 . . . . . . . . . . . 12 (𝑔 = (𝑑𝐡((2nd β€˜π‘₯) + 1)) β†’ (𝑔 ∈ 𝐾 ↔ (𝑑𝐡((2nd β€˜π‘₯) + 1)) ∈ 𝐾))
150141, 149rexsn 4647 . . . . . . . . . . 11 (βˆƒπ‘” ∈ {(𝑑𝐡((2nd β€˜π‘₯) + 1))}𝑔 ∈ 𝐾 ↔ (𝑑𝐡((2nd β€˜π‘₯) + 1)) ∈ 𝐾)
151148, 150sylib 217 . . . . . . . . . 10 (((π΅β€˜π‘₯) ∩ (𝑑𝐡((2nd β€˜π‘₯) + 1))) ∈ 𝐾 β†’ (𝑑𝐡((2nd β€˜π‘₯) + 1)) ∈ 𝐾)
152 ovex 7394 . . . . . . . . . . . 12 ((2nd β€˜π‘₯) + 1) ∈ V
15313, 14, 6, 42, 152heiborlem2 36321 . . . . . . . . . . 11 (𝑑𝐺((2nd β€˜π‘₯) + 1) ↔ (((2nd β€˜π‘₯) + 1) ∈ β„•0 ∧ 𝑑 ∈ (πΉβ€˜((2nd β€˜π‘₯) + 1)) ∧ (𝑑𝐡((2nd β€˜π‘₯) + 1)) ∈ 𝐾))
154153biimpri 227 . . . . . . . . . 10 ((((2nd β€˜π‘₯) + 1) ∈ β„•0 ∧ 𝑑 ∈ (πΉβ€˜((2nd β€˜π‘₯) + 1)) ∧ (𝑑𝐡((2nd β€˜π‘₯) + 1)) ∈ 𝐾) β†’ 𝑑𝐺((2nd β€˜π‘₯) + 1))
155137, 138, 151, 154syl3an 1161 . . . . . . . . 9 (((πœ‘ ∧ π‘₯ ∈ 𝐺) ∧ 𝑑 ∈ (πΉβ€˜((2nd β€˜π‘₯) + 1)) ∧ ((π΅β€˜π‘₯) ∩ (𝑑𝐡((2nd β€˜π‘₯) + 1))) ∈ 𝐾) β†’ 𝑑𝐺((2nd β€˜π‘₯) + 1))
1561553expb 1121 . . . . . . . 8 (((πœ‘ ∧ π‘₯ ∈ 𝐺) ∧ (𝑑 ∈ (πΉβ€˜((2nd β€˜π‘₯) + 1)) ∧ ((π΅β€˜π‘₯) ∩ (𝑑𝐡((2nd β€˜π‘₯) + 1))) ∈ 𝐾)) β†’ 𝑑𝐺((2nd β€˜π‘₯) + 1))
157 simprr 772 . . . . . . . 8 (((πœ‘ ∧ π‘₯ ∈ 𝐺) ∧ (𝑑 ∈ (πΉβ€˜((2nd β€˜π‘₯) + 1)) ∧ ((π΅β€˜π‘₯) ∩ (𝑑𝐡((2nd β€˜π‘₯) + 1))) ∈ 𝐾)) β†’ ((π΅β€˜π‘₯) ∩ (𝑑𝐡((2nd β€˜π‘₯) + 1))) ∈ 𝐾)
158136, 156, 157jca32 517 . . . . . . 7 (((πœ‘ ∧ π‘₯ ∈ 𝐺) ∧ (𝑑 ∈ (πΉβ€˜((2nd β€˜π‘₯) + 1)) ∧ ((π΅β€˜π‘₯) ∩ (𝑑𝐡((2nd β€˜π‘₯) + 1))) ∈ 𝐾)) β†’ (𝑑 ∈ βˆͺ 𝐽 ∧ (𝑑𝐺((2nd β€˜π‘₯) + 1) ∧ ((π΅β€˜π‘₯) ∩ (𝑑𝐡((2nd β€˜π‘₯) + 1))) ∈ 𝐾)))
159158ex 414 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ 𝐺) β†’ ((𝑑 ∈ (πΉβ€˜((2nd β€˜π‘₯) + 1)) ∧ ((π΅β€˜π‘₯) ∩ (𝑑𝐡((2nd β€˜π‘₯) + 1))) ∈ 𝐾) β†’ (𝑑 ∈ βˆͺ 𝐽 ∧ (𝑑𝐺((2nd β€˜π‘₯) + 1) ∧ ((π΅β€˜π‘₯) ∩ (𝑑𝐡((2nd β€˜π‘₯) + 1))) ∈ 𝐾))))
160159reximdv2 3158 . . . . 5 ((πœ‘ ∧ π‘₯ ∈ 𝐺) β†’ (βˆƒπ‘‘ ∈ (πΉβ€˜((2nd β€˜π‘₯) + 1))((π΅β€˜π‘₯) ∩ (𝑑𝐡((2nd β€˜π‘₯) + 1))) ∈ 𝐾 β†’ βˆƒπ‘‘ ∈ βˆͺ 𝐽(𝑑𝐺((2nd β€˜π‘₯) + 1) ∧ ((π΅β€˜π‘₯) ∩ (𝑑𝐡((2nd β€˜π‘₯) + 1))) ∈ 𝐾)))
161128, 160mpd 15 . . . 4 ((πœ‘ ∧ π‘₯ ∈ 𝐺) β†’ βˆƒπ‘‘ ∈ βˆͺ 𝐽(𝑑𝐺((2nd β€˜π‘₯) + 1) ∧ ((π΅β€˜π‘₯) ∩ (𝑑𝐡((2nd β€˜π‘₯) + 1))) ∈ 𝐾))
162161ralrimiva 3140 . . 3 (πœ‘ β†’ βˆ€π‘₯ ∈ 𝐺 βˆƒπ‘‘ ∈ βˆͺ 𝐽(𝑑𝐺((2nd β€˜π‘₯) + 1) ∧ ((π΅β€˜π‘₯) ∩ (𝑑𝐡((2nd β€˜π‘₯) + 1))) ∈ 𝐾))
16313fvexi 6860 . . . . 5 𝐽 ∈ V
164163uniex 7682 . . . 4 βˆͺ 𝐽 ∈ V
165 breq1 5112 . . . . 5 (𝑑 = (π‘”β€˜π‘₯) β†’ (𝑑𝐺((2nd β€˜π‘₯) + 1) ↔ (π‘”β€˜π‘₯)𝐺((2nd β€˜π‘₯) + 1)))
166 oveq1 7368 . . . . . . 7 (𝑑 = (π‘”β€˜π‘₯) β†’ (𝑑𝐡((2nd β€˜π‘₯) + 1)) = ((π‘”β€˜π‘₯)𝐡((2nd β€˜π‘₯) + 1)))
167166ineq2d 4176 . . . . . 6 (𝑑 = (π‘”β€˜π‘₯) β†’ ((π΅β€˜π‘₯) ∩ (𝑑𝐡((2nd β€˜π‘₯) + 1))) = ((π΅β€˜π‘₯) ∩ ((π‘”β€˜π‘₯)𝐡((2nd β€˜π‘₯) + 1))))
168167eleq1d 2819 . . . . 5 (𝑑 = (π‘”β€˜π‘₯) β†’ (((π΅β€˜π‘₯) ∩ (𝑑𝐡((2nd β€˜π‘₯) + 1))) ∈ 𝐾 ↔ ((π΅β€˜π‘₯) ∩ ((π‘”β€˜π‘₯)𝐡((2nd β€˜π‘₯) + 1))) ∈ 𝐾))
169165, 168anbi12d 632 . . . 4 (𝑑 = (π‘”β€˜π‘₯) β†’ ((𝑑𝐺((2nd β€˜π‘₯) + 1) ∧ ((π΅β€˜π‘₯) ∩ (𝑑𝐡((2nd β€˜π‘₯) + 1))) ∈ 𝐾) ↔ ((π‘”β€˜π‘₯)𝐺((2nd β€˜π‘₯) + 1) ∧ ((π΅β€˜π‘₯) ∩ ((π‘”β€˜π‘₯)𝐡((2nd β€˜π‘₯) + 1))) ∈ 𝐾)))
170164, 169axcc4dom 10385 . . 3 ((𝐺 β‰Ό Ο‰ ∧ βˆ€π‘₯ ∈ 𝐺 βˆƒπ‘‘ ∈ βˆͺ 𝐽(𝑑𝐺((2nd β€˜π‘₯) + 1) ∧ ((π΅β€˜π‘₯) ∩ (𝑑𝐡((2nd β€˜π‘₯) + 1))) ∈ 𝐾)) β†’ βˆƒπ‘”(𝑔:𝐺⟢βˆͺ 𝐽 ∧ βˆ€π‘₯ ∈ 𝐺 ((π‘”β€˜π‘₯)𝐺((2nd β€˜π‘₯) + 1) ∧ ((π΅β€˜π‘₯) ∩ ((π‘”β€˜π‘₯)𝐡((2nd β€˜π‘₯) + 1))) ∈ 𝐾)))
17158, 162, 170syl2anc 585 . 2 (πœ‘ β†’ βˆƒπ‘”(𝑔:𝐺⟢βˆͺ 𝐽 ∧ βˆ€π‘₯ ∈ 𝐺 ((π‘”β€˜π‘₯)𝐺((2nd β€˜π‘₯) + 1) ∧ ((π΅β€˜π‘₯) ∩ ((π‘”β€˜π‘₯)𝐡((2nd β€˜π‘₯) + 1))) ∈ 𝐾)))
172 exsimpr 1873 . 2 (βˆƒπ‘”(𝑔:𝐺⟢βˆͺ 𝐽 ∧ βˆ€π‘₯ ∈ 𝐺 ((π‘”β€˜π‘₯)𝐺((2nd β€˜π‘₯) + 1) ∧ ((π΅β€˜π‘₯) ∩ ((π‘”β€˜π‘₯)𝐡((2nd β€˜π‘₯) + 1))) ∈ 𝐾)) β†’ βˆƒπ‘”βˆ€π‘₯ ∈ 𝐺 ((π‘”β€˜π‘₯)𝐺((2nd β€˜π‘₯) + 1) ∧ ((π΅β€˜π‘₯) ∩ ((π‘”β€˜π‘₯)𝐡((2nd β€˜π‘₯) + 1))) ∈ 𝐾))
173171, 172syl 17 1 (πœ‘ β†’ βˆƒπ‘”βˆ€π‘₯ ∈ 𝐺 ((π‘”β€˜π‘₯)𝐺((2nd β€˜π‘₯) + 1) ∧ ((π΅β€˜π‘₯) ∩ ((π‘”β€˜π‘₯)𝐡((2nd β€˜π‘₯) + 1))) ∈ 𝐾))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ∧ wa 397   ∧ w3a 1088   = wceq 1542  βˆƒwex 1782   ∈ wcel 2107  {cab 2710  βˆ€wral 3061  βˆƒwrex 3070  Vcvv 3447   ∩ cin 3913   βŠ† wss 3914  π’« cpw 4564  {csn 4590  βŸ¨cop 4596  βˆͺ cuni 4869  βˆͺ ciun 4958   class class class wbr 5109  {copab 5171   Γ— cxp 5635  Rel wrel 5642  βŸΆwf 6496  β€˜cfv 6500  (class class class)co 7361   ∈ cmpo 7363  Ο‰com 7806  1st c1st 7923  2nd c2nd 7924   β‰ˆ cen 8886   β‰Ό cdom 8887   β‰Ί csdm 8888  Fincfn 8889  1c1 11060   + caddc 11062  β„*cxr 11196   / cdiv 11820  β„•cn 12161  2c2 12216  β„•0cn0 12421  β†‘cexp 13976  βˆžMetcxmet 20804  Metcmet 20805  ballcbl 20806  MetOpencmopn 20809  CMetccmet 24641
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5246  ax-sep 5260  ax-nul 5267  ax-pow 5324  ax-pr 5388  ax-un 7676  ax-inf2 9585  ax-cc 10379  ax-cnex 11115  ax-resscn 11116  ax-1cn 11117  ax-icn 11118  ax-addcl 11119  ax-addrcl 11120  ax-mulcl 11121  ax-mulrcl 11122  ax-mulcom 11123  ax-addass 11124  ax-mulass 11125  ax-distr 11126  ax-i2m1 11127  ax-1ne0 11128  ax-1rid 11129  ax-rnegex 11130  ax-rrecex 11131  ax-cnre 11132  ax-pre-lttri 11133  ax-pre-lttrn 11134  ax-pre-ltadd 11135  ax-pre-mulgt0 11136  ax-pre-sup 11137
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3352  df-reu 3353  df-rab 3407  df-v 3449  df-sbc 3744  df-csb 3860  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3933  df-nul 4287  df-if 4491  df-pw 4566  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4870  df-int 4912  df-iun 4960  df-br 5110  df-opab 5172  df-mpt 5193  df-tr 5227  df-id 5535  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5592  df-se 5593  df-we 5594  df-xp 5643  df-rel 5644  df-cnv 5645  df-co 5646  df-dm 5647  df-rn 5648  df-res 5649  df-ima 5650  df-pred 6257  df-ord 6324  df-on 6325  df-lim 6326  df-suc 6327  df-iota 6452  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-isom 6509  df-riota 7317  df-ov 7364  df-oprab 7365  df-mpo 7366  df-om 7807  df-1st 7925  df-2nd 7926  df-frecs 8216  df-wrecs 8247  df-recs 8321  df-rdg 8360  df-1o 8416  df-er 8654  df-map 8773  df-en 8890  df-dom 8891  df-sdom 8892  df-fin 8893  df-sup 9386  df-inf 9387  df-oi 9454  df-card 9883  df-acn 9886  df-pnf 11199  df-mnf 11200  df-xr 11201  df-ltxr 11202  df-le 11203  df-sub 11395  df-neg 11396  df-div 11821  df-nn 12162  df-2 12224  df-n0 12422  df-z 12508  df-uz 12772  df-q 12882  df-rp 12924  df-xneg 13041  df-xadd 13042  df-xmul 13043  df-seq 13916  df-exp 13977  df-topgen 17333  df-psmet 20811  df-xmet 20812  df-met 20813  df-bl 20814  df-mopn 20815  df-top 22266  df-topon 22283  df-bases 22319  df-cmet 24644
This theorem is referenced by:  heiborlem10  36329
  Copyright terms: Public domain W3C validator