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 36681
Description: Lemma for heibor 36689. Using countable choice ax-cc 10430, 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 36679 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 10430 via iunctb 10569), and so we can apply ax-cc 10430 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 12478 . . . . . 6 β„•0 ∈ V
2 fvex 6905 . . . . . . 7 (πΉβ€˜π‘‘) ∈ V
3 vsnex 5430 . . . . . . 7 {𝑑} ∈ V
42, 3xpex 7740 . . . . . 6 ((πΉβ€˜π‘‘) Γ— {𝑑}) ∈ V
51, 4iunex 7955 . . . . 5 βˆͺ 𝑑 ∈ β„•0 ((πΉβ€˜π‘‘) Γ— {𝑑}) ∈ V
6 heibor.4 . . . . . . . . 9 𝐺 = {βŸ¨π‘¦, π‘›βŸ© ∣ (𝑛 ∈ β„•0 ∧ 𝑦 ∈ (πΉβ€˜π‘›) ∧ (𝑦𝐡𝑛) ∈ 𝐾)}
76relopabiv 5821 . . . . . . . 8 Rel 𝐺
8 1st2nd 8025 . . . . . . . 8 ((Rel 𝐺 ∧ π‘₯ ∈ 𝐺) β†’ π‘₯ = ⟨(1st β€˜π‘₯), (2nd β€˜π‘₯)⟩)
97, 8mpan 689 . . . . . . 7 (π‘₯ ∈ 𝐺 β†’ π‘₯ = ⟨(1st β€˜π‘₯), (2nd β€˜π‘₯)⟩)
109eleq1d 2819 . . . . . . . . . . 11 (π‘₯ ∈ 𝐺 β†’ (π‘₯ ∈ 𝐺 ↔ ⟨(1st β€˜π‘₯), (2nd β€˜π‘₯)⟩ ∈ 𝐺))
11 df-br 5150 . . . . . . . . . . 11 ((1st β€˜π‘₯)𝐺(2nd β€˜π‘₯) ↔ ⟨(1st β€˜π‘₯), (2nd β€˜π‘₯)⟩ ∈ 𝐺)
1210, 11bitr4di 289 . . . . . . . . . 10 (π‘₯ ∈ 𝐺 β†’ (π‘₯ ∈ 𝐺 ↔ (1st β€˜π‘₯)𝐺(2nd β€˜π‘₯)))
13 heibor.1 . . . . . . . . . . 11 𝐽 = (MetOpenβ€˜π·)
14 heibor.3 . . . . . . . . . . 11 𝐾 = {𝑒 ∣ Β¬ βˆƒπ‘£ ∈ (𝒫 π‘ˆ ∩ Fin)𝑒 βŠ† βˆͺ 𝑣}
15 fvex 6905 . . . . . . . . . . 11 (1st β€˜π‘₯) ∈ V
16 fvex 6905 . . . . . . . . . . 11 (2nd β€˜π‘₯) ∈ V
1713, 14, 6, 15, 16heiborlem2 36680 . . . . . . . . . 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 4665 . . . . . . . . . . . 12 (2nd β€˜π‘₯) ∈ {(2nd β€˜π‘₯)}
21 opelxp 5713 . . . . . . . . . . . 12 (⟨(1st β€˜π‘₯), (2nd β€˜π‘₯)⟩ ∈ ((πΉβ€˜(2nd β€˜π‘₯)) Γ— {(2nd β€˜π‘₯)}) ↔ ((1st β€˜π‘₯) ∈ (πΉβ€˜(2nd β€˜π‘₯)) ∧ (2nd β€˜π‘₯) ∈ {(2nd β€˜π‘₯)}))
2220, 21mpbiran2 709 . . . . . . . . . . 11 (⟨(1st β€˜π‘₯), (2nd β€˜π‘₯)⟩ ∈ ((πΉβ€˜(2nd β€˜π‘₯)) Γ— {(2nd β€˜π‘₯)}) ↔ (1st β€˜π‘₯) ∈ (πΉβ€˜(2nd β€˜π‘₯)))
23 fveq2 6892 . . . . . . . . . . . . . 14 (𝑑 = (2nd β€˜π‘₯) β†’ (πΉβ€˜π‘‘) = (πΉβ€˜(2nd β€˜π‘₯)))
24 sneq 4639 . . . . . . . . . . . . . 14 (𝑑 = (2nd β€˜π‘₯) β†’ {𝑑} = {(2nd β€˜π‘₯)})
2523, 24xpeq12d 5708 . . . . . . . . . . . . 13 (𝑑 = (2nd β€˜π‘₯) β†’ ((πΉβ€˜π‘‘) Γ— {𝑑}) = ((πΉβ€˜(2nd β€˜π‘₯)) Γ— {(2nd β€˜π‘₯)}))
2625eleq2d 2820 . . . . . . . . . . . 12 (𝑑 = (2nd β€˜π‘₯) β†’ (⟨(1st β€˜π‘₯), (2nd β€˜π‘₯)⟩ ∈ ((πΉβ€˜π‘‘) Γ— {𝑑}) ↔ ⟨(1st β€˜π‘₯), (2nd β€˜π‘₯)⟩ ∈ ((πΉβ€˜(2nd β€˜π‘₯)) Γ— {(2nd β€˜π‘₯)})))
2726rspcev 3613 . . . . . . . . . . 11 (((2nd β€˜π‘₯) ∈ β„•0 ∧ ⟨(1st β€˜π‘₯), (2nd β€˜π‘₯)⟩ ∈ ((πΉβ€˜(2nd β€˜π‘₯)) Γ— {(2nd β€˜π‘₯)})) β†’ βˆƒπ‘‘ ∈ β„•0 ⟨(1st β€˜π‘₯), (2nd β€˜π‘₯)⟩ ∈ ((πΉβ€˜π‘‘) Γ— {𝑑}))
2822, 27sylan2br 596 . . . . . . . . . 10 (((2nd β€˜π‘₯) ∈ β„•0 ∧ (1st β€˜π‘₯) ∈ (πΉβ€˜(2nd β€˜π‘₯))) β†’ βˆƒπ‘‘ ∈ β„•0 ⟨(1st β€˜π‘₯), (2nd β€˜π‘₯)⟩ ∈ ((πΉβ€˜π‘‘) Γ— {𝑑}))
29 eliun 5002 . . . . . . . . . 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 3987 . . . . 5 𝐺 βŠ† βˆͺ 𝑑 ∈ β„•0 ((πΉβ€˜π‘‘) Γ— {𝑑})
35 ssdomg 8996 . . . . 5 (βˆͺ 𝑑 ∈ β„•0 ((πΉβ€˜π‘‘) Γ— {𝑑}) ∈ V β†’ (𝐺 βŠ† βˆͺ 𝑑 ∈ β„•0 ((πΉβ€˜π‘‘) Γ— {𝑑}) β†’ 𝐺 β‰Ό βˆͺ 𝑑 ∈ β„•0 ((πΉβ€˜π‘‘) Γ— {𝑑})))
365, 34, 35mp2 9 . . . 4 𝐺 β‰Ό βˆͺ 𝑑 ∈ β„•0 ((πΉβ€˜π‘‘) Γ— {𝑑})
37 nn0ennn 13944 . . . . . . 7 β„•0 β‰ˆ β„•
38 nnenom 13945 . . . . . . 7 β„• β‰ˆ Ο‰
3937, 38entri 9004 . . . . . 6 β„•0 β‰ˆ Ο‰
40 endom 8975 . . . . . 6 (β„•0 β‰ˆ Ο‰ β†’ β„•0 β‰Ό Ο‰)
4139, 40ax-mp 5 . . . . 5 β„•0 β‰Ό Ο‰
42 vex 3479 . . . . . . . 8 𝑑 ∈ V
432, 42xpsnen 9055 . . . . . . 7 ((πΉβ€˜π‘‘) Γ— {𝑑}) β‰ˆ (πΉβ€˜π‘‘)
44 inss2 4230 . . . . . . . . 9 (𝒫 𝑋 ∩ Fin) βŠ† Fin
45 heibor.7 . . . . . . . . . 10 (πœ‘ β†’ 𝐹:β„•0⟢(𝒫 𝑋 ∩ Fin))
4645ffvelcdmda 7087 . . . . . . . . 9 ((πœ‘ ∧ 𝑑 ∈ β„•0) β†’ (πΉβ€˜π‘‘) ∈ (𝒫 𝑋 ∩ Fin))
4744, 46sselid 3981 . . . . . . . 8 ((πœ‘ ∧ 𝑑 ∈ β„•0) β†’ (πΉβ€˜π‘‘) ∈ Fin)
48 isfinite 9647 . . . . . . . . 9 ((πΉβ€˜π‘‘) ∈ Fin ↔ (πΉβ€˜π‘‘) β‰Ί Ο‰)
49 sdomdom 8976 . . . . . . . . 9 ((πΉβ€˜π‘‘) β‰Ί Ο‰ β†’ (πΉβ€˜π‘‘) β‰Ό Ο‰)
5048, 49sylbi 216 . . . . . . . 8 ((πΉβ€˜π‘‘) ∈ Fin β†’ (πΉβ€˜π‘‘) β‰Ό Ο‰)
5147, 50syl 17 . . . . . . 7 ((πœ‘ ∧ 𝑑 ∈ β„•0) β†’ (πΉβ€˜π‘‘) β‰Ό Ο‰)
52 endomtr 9008 . . . . . . 7 ((((πΉβ€˜π‘‘) Γ— {𝑑}) β‰ˆ (πΉβ€˜π‘‘) ∧ (πΉβ€˜π‘‘) β‰Ό Ο‰) β†’ ((πΉβ€˜π‘‘) Γ— {𝑑}) β‰Ό Ο‰)
5343, 51, 52sylancr 588 . . . . . 6 ((πœ‘ ∧ 𝑑 ∈ β„•0) β†’ ((πΉβ€˜π‘‘) Γ— {𝑑}) β‰Ό Ο‰)
5453ralrimiva 3147 . . . . 5 (πœ‘ β†’ βˆ€π‘‘ ∈ β„•0 ((πΉβ€˜π‘‘) Γ— {𝑑}) β‰Ό Ο‰)
55 iunctb 10569 . . . . 5 ((β„•0 β‰Ό Ο‰ ∧ βˆ€π‘‘ ∈ β„•0 ((πΉβ€˜π‘‘) Γ— {𝑑}) β‰Ό Ο‰) β†’ βˆͺ 𝑑 ∈ β„•0 ((πΉβ€˜π‘‘) Γ— {𝑑}) β‰Ό Ο‰)
5641, 54, 55sylancr 588 . . . 4 (πœ‘ β†’ βˆͺ 𝑑 ∈ β„•0 ((πΉβ€˜π‘‘) Γ— {𝑑}) β‰Ό Ο‰)
57 domtr 9003 . . . 4 ((𝐺 β‰Ό βˆͺ 𝑑 ∈ β„•0 ((πΉβ€˜π‘‘) Γ— {𝑑}) ∧ βˆͺ 𝑑 ∈ β„•0 ((πΉβ€˜π‘‘) Γ— {𝑑}) β‰Ό Ο‰) β†’ 𝐺 β‰Ό Ο‰)
5836, 56, 57sylancr 588 . . 3 (πœ‘ β†’ 𝐺 β‰Ό Ο‰)
5919simp1d 1143 . . . . . . . . 9 (π‘₯ ∈ 𝐺 β†’ (2nd β€˜π‘₯) ∈ β„•0)
60 peano2nn0 12512 . . . . . . . . 9 ((2nd β€˜π‘₯) ∈ β„•0 β†’ ((2nd β€˜π‘₯) + 1) ∈ β„•0)
6159, 60syl 17 . . . . . . . 8 (π‘₯ ∈ 𝐺 β†’ ((2nd β€˜π‘₯) + 1) ∈ β„•0)
62 ffvelcdm 7084 . . . . . . . 8 ((𝐹:β„•0⟢(𝒫 𝑋 ∩ Fin) ∧ ((2nd β€˜π‘₯) + 1) ∈ β„•0) β†’ (πΉβ€˜((2nd β€˜π‘₯) + 1)) ∈ (𝒫 𝑋 ∩ Fin))
6345, 61, 62syl2an 597 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ 𝐺) β†’ (πΉβ€˜((2nd β€˜π‘₯) + 1)) ∈ (𝒫 𝑋 ∩ Fin))
6444, 63sselid 3981 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ 𝐺) β†’ (πΉβ€˜((2nd β€˜π‘₯) + 1)) ∈ Fin)
65 iunin2 5075 . . . . . . . 8 βˆͺ 𝑑 ∈ (πΉβ€˜((2nd β€˜π‘₯) + 1))((π΅β€˜π‘₯) ∩ (𝑑𝐡((2nd β€˜π‘₯) + 1))) = ((π΅β€˜π‘₯) ∩ βˆͺ 𝑑 ∈ (πΉβ€˜((2nd β€˜π‘₯) + 1))(𝑑𝐡((2nd β€˜π‘₯) + 1)))
66 heibor.8 . . . . . . . . . . 11 (πœ‘ β†’ βˆ€π‘› ∈ β„•0 𝑋 = βˆͺ 𝑦 ∈ (πΉβ€˜π‘›)(𝑦𝐡𝑛))
67 oveq1 7416 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑑 β†’ (𝑦𝐡𝑛) = (𝑑𝐡𝑛))
6867cbviunv 5044 . . . . . . . . . . . . . . 15 βˆͺ 𝑦 ∈ (πΉβ€˜π‘›)(𝑦𝐡𝑛) = βˆͺ 𝑑 ∈ (πΉβ€˜π‘›)(𝑑𝐡𝑛)
69 fveq2 6892 . . . . . . . . . . . . . . . 16 (𝑛 = ((2nd β€˜π‘₯) + 1) β†’ (πΉβ€˜π‘›) = (πΉβ€˜((2nd β€˜π‘₯) + 1)))
7069iuneq1d 5025 . . . . . . . . . . . . . . 15 (𝑛 = ((2nd β€˜π‘₯) + 1) β†’ βˆͺ 𝑑 ∈ (πΉβ€˜π‘›)(𝑑𝐡𝑛) = βˆͺ 𝑑 ∈ (πΉβ€˜((2nd β€˜π‘₯) + 1))(𝑑𝐡𝑛))
7168, 70eqtrid 2785 . . . . . . . . . . . . . 14 (𝑛 = ((2nd β€˜π‘₯) + 1) β†’ βˆͺ 𝑦 ∈ (πΉβ€˜π‘›)(𝑦𝐡𝑛) = βˆͺ 𝑑 ∈ (πΉβ€˜((2nd β€˜π‘₯) + 1))(𝑑𝐡𝑛))
72 oveq2 7417 . . . . . . . . . . . . . . 15 (𝑛 = ((2nd β€˜π‘₯) + 1) β†’ (𝑑𝐡𝑛) = (𝑑𝐡((2nd β€˜π‘₯) + 1)))
7372iuneq2d 5027 . . . . . . . . . . . . . 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 3612 . . . . . . . . . . 11 ((βˆ€π‘› ∈ β„•0 𝑋 = βˆͺ 𝑦 ∈ (πΉβ€˜π‘›)(𝑦𝐡𝑛) ∧ ((2nd β€˜π‘₯) + 1) ∈ β„•0) β†’ 𝑋 = βˆͺ 𝑑 ∈ (πΉβ€˜((2nd β€˜π‘₯) + 1))(𝑑𝐡((2nd β€˜π‘₯) + 1)))
7766, 61, 76syl2an 597 . . . . . . . . . 10 ((πœ‘ ∧ π‘₯ ∈ 𝐺) β†’ 𝑋 = βˆͺ 𝑑 ∈ (πΉβ€˜((2nd β€˜π‘₯) + 1))(𝑑𝐡((2nd β€˜π‘₯) + 1)))
7877ineq2d 4213 . . . . . . . . 9 ((πœ‘ ∧ π‘₯ ∈ 𝐺) β†’ ((π΅β€˜π‘₯) ∩ 𝑋) = ((π΅β€˜π‘₯) ∩ βˆͺ 𝑑 ∈ (πΉβ€˜((2nd β€˜π‘₯) + 1))(𝑑𝐡((2nd β€˜π‘₯) + 1))))
799fveq2d 6896 . . . . . . . . . . . . . 14 (π‘₯ ∈ 𝐺 β†’ (π΅β€˜π‘₯) = (π΅β€˜βŸ¨(1st β€˜π‘₯), (2nd β€˜π‘₯)⟩))
80 df-ov 7412 . . . . . . . . . . . . . 14 ((1st β€˜π‘₯)𝐡(2nd β€˜π‘₯)) = (π΅β€˜βŸ¨(1st β€˜π‘₯), (2nd β€˜π‘₯)⟩)
8179, 80eqtr4di 2791 . . . . . . . . . . . . 13 (π‘₯ ∈ 𝐺 β†’ (π΅β€˜π‘₯) = ((1st β€˜π‘₯)𝐡(2nd β€˜π‘₯)))
8281adantl 483 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘₯ ∈ 𝐺) β†’ (π΅β€˜π‘₯) = ((1st β€˜π‘₯)𝐡(2nd β€˜π‘₯)))
83 inss1 4229 . . . . . . . . . . . . . . . 16 (𝒫 𝑋 ∩ Fin) βŠ† 𝒫 𝑋
84 ffvelcdm 7084 . . . . . . . . . . . . . . . . 17 ((𝐹:β„•0⟢(𝒫 𝑋 ∩ Fin) ∧ (2nd β€˜π‘₯) ∈ β„•0) β†’ (πΉβ€˜(2nd β€˜π‘₯)) ∈ (𝒫 𝑋 ∩ Fin))
8545, 59, 84syl2an 597 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘₯ ∈ 𝐺) β†’ (πΉβ€˜(2nd β€˜π‘₯)) ∈ (𝒫 𝑋 ∩ Fin))
8683, 85sselid 3981 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘₯ ∈ 𝐺) β†’ (πΉβ€˜(2nd β€˜π‘₯)) ∈ 𝒫 𝑋)
8786elpwid 4612 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘₯ ∈ 𝐺) β†’ (πΉβ€˜(2nd β€˜π‘₯)) βŠ† 𝑋)
8819simp2d 1144 . . . . . . . . . . . . . . 15 (π‘₯ ∈ 𝐺 β†’ (1st β€˜π‘₯) ∈ (πΉβ€˜(2nd β€˜π‘₯)))
8988adantl 483 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘₯ ∈ 𝐺) β†’ (1st β€˜π‘₯) ∈ (πΉβ€˜(2nd β€˜π‘₯)))
9087, 89sseldd 3984 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘₯ ∈ 𝐺) β†’ (1st β€˜π‘₯) ∈ 𝑋)
9159adantl 483 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘₯ ∈ 𝐺) β†’ (2nd β€˜π‘₯) ∈ β„•0)
92 oveq1 7416 . . . . . . . . . . . . . 14 (𝑧 = (1st β€˜π‘₯) β†’ (𝑧(ballβ€˜π·)(1 / (2β†‘π‘š))) = ((1st β€˜π‘₯)(ballβ€˜π·)(1 / (2β†‘π‘š))))
93 oveq2 7417 . . . . . . . . . . . . . . . 16 (π‘š = (2nd β€˜π‘₯) β†’ (2β†‘π‘š) = (2↑(2nd β€˜π‘₯)))
9493oveq2d 7425 . . . . . . . . . . . . . . 15 (π‘š = (2nd β€˜π‘₯) β†’ (1 / (2β†‘π‘š)) = (1 / (2↑(2nd β€˜π‘₯))))
9594oveq2d 7425 . . . . . . . . . . . . . 14 (π‘š = (2nd β€˜π‘₯) β†’ ((1st β€˜π‘₯)(ballβ€˜π·)(1 / (2β†‘π‘š))) = ((1st β€˜π‘₯)(ballβ€˜π·)(1 / (2↑(2nd β€˜π‘₯)))))
96 heibor.5 . . . . . . . . . . . . . 14 𝐡 = (𝑧 ∈ 𝑋, π‘š ∈ β„•0 ↦ (𝑧(ballβ€˜π·)(1 / (2β†‘π‘š))))
97 ovex 7442 . . . . . . . . . . . . . 14 ((1st β€˜π‘₯)(ballβ€˜π·)(1 / (2↑(2nd β€˜π‘₯)))) ∈ V
9892, 95, 96, 97ovmpo 7568 . . . . . . . . . . . . 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 24803 . . . . . . . . . . . . . . 15 (𝐷 ∈ (CMetβ€˜π‘‹) β†’ 𝐷 ∈ (Metβ€˜π‘‹))
103101, 102syl 17 . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝐷 ∈ (Metβ€˜π‘‹))
104 metxmet 23840 . . . . . . . . . . . . . 14 (𝐷 ∈ (Metβ€˜π‘‹) β†’ 𝐷 ∈ (∞Metβ€˜π‘‹))
105103, 104syl 17 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝐷 ∈ (∞Metβ€˜π‘‹))
106105adantr 482 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘₯ ∈ 𝐺) β†’ 𝐷 ∈ (∞Metβ€˜π‘‹))
107 2nn 12285 . . . . . . . . . . . . . . . 16 2 ∈ β„•
108 nnexpcl 14040 . . . . . . . . . . . . . . . 16 ((2 ∈ β„• ∧ (2nd β€˜π‘₯) ∈ β„•0) β†’ (2↑(2nd β€˜π‘₯)) ∈ β„•)
109107, 91, 108sylancr 588 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘₯ ∈ 𝐺) β†’ (2↑(2nd β€˜π‘₯)) ∈ β„•)
110109nnrpd 13014 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘₯ ∈ 𝐺) β†’ (2↑(2nd β€˜π‘₯)) ∈ ℝ+)
111110rpreccld 13026 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘₯ ∈ 𝐺) β†’ (1 / (2↑(2nd β€˜π‘₯))) ∈ ℝ+)
112111rpxrd 13017 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘₯ ∈ 𝐺) β†’ (1 / (2↑(2nd β€˜π‘₯))) ∈ ℝ*)
113 blssm 23924 . . . . . . . . . . . 12 ((𝐷 ∈ (∞Metβ€˜π‘‹) ∧ (1st β€˜π‘₯) ∈ 𝑋 ∧ (1 / (2↑(2nd β€˜π‘₯))) ∈ ℝ*) β†’ ((1st β€˜π‘₯)(ballβ€˜π·)(1 / (2↑(2nd β€˜π‘₯)))) βŠ† 𝑋)
114106, 90, 112, 113syl3anc 1372 . . . . . . . . . . 11 ((πœ‘ ∧ π‘₯ ∈ 𝐺) β†’ ((1st β€˜π‘₯)(ballβ€˜π·)(1 / (2↑(2nd β€˜π‘₯)))) βŠ† 𝑋)
115100, 114eqsstrd 4021 . . . . . . . . . 10 ((πœ‘ ∧ π‘₯ ∈ 𝐺) β†’ (π΅β€˜π‘₯) βŠ† 𝑋)
116 df-ss 3966 . . . . . . . . . 10 ((π΅β€˜π‘₯) βŠ† 𝑋 ↔ ((π΅β€˜π‘₯) ∩ 𝑋) = (π΅β€˜π‘₯))
117115, 116sylib 217 . . . . . . . . 9 ((πœ‘ ∧ π‘₯ ∈ 𝐺) β†’ ((π΅β€˜π‘₯) ∩ 𝑋) = (π΅β€˜π‘₯))
11878, 117eqtr3d 2775 . . . . . . . 8 ((πœ‘ ∧ π‘₯ ∈ 𝐺) β†’ ((π΅β€˜π‘₯) ∩ βˆͺ 𝑑 ∈ (πΉβ€˜((2nd β€˜π‘₯) + 1))(𝑑𝐡((2nd β€˜π‘₯) + 1))) = (π΅β€˜π‘₯))
11965, 118eqtrid 2785 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ 𝐺) β†’ βˆͺ 𝑑 ∈ (πΉβ€˜((2nd β€˜π‘₯) + 1))((π΅β€˜π‘₯) ∩ (𝑑𝐡((2nd β€˜π‘₯) + 1))) = (π΅β€˜π‘₯))
120 eqimss2 4042 . . . . . . 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 6905 . . . . . . . 8 (π΅β€˜π‘₯) ∈ V
126125inex1 5318 . . . . . . 7 ((π΅β€˜π‘₯) ∩ (𝑑𝐡((2nd β€˜π‘₯) + 1))) ∈ V
12713, 14, 126heiborlem1 36679 . . . . . 6 (((πΉβ€˜((2nd β€˜π‘₯) + 1)) ∈ Fin ∧ (π΅β€˜π‘₯) βŠ† βˆͺ 𝑑 ∈ (πΉβ€˜((2nd β€˜π‘₯) + 1))((π΅β€˜π‘₯) ∩ (𝑑𝐡((2nd β€˜π‘₯) + 1))) ∧ (π΅β€˜π‘₯) ∈ 𝐾) β†’ βˆƒπ‘‘ ∈ (πΉβ€˜((2nd β€˜π‘₯) + 1))((π΅β€˜π‘₯) ∩ (𝑑𝐡((2nd β€˜π‘₯) + 1))) ∈ 𝐾)
12864, 121, 124, 127syl3anc 1372 . . . . 5 ((πœ‘ ∧ π‘₯ ∈ 𝐺) β†’ βˆƒπ‘‘ ∈ (πΉβ€˜((2nd β€˜π‘₯) + 1))((π΅β€˜π‘₯) ∩ (𝑑𝐡((2nd β€˜π‘₯) + 1))) ∈ 𝐾)
12983, 63sselid 3981 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘₯ ∈ 𝐺) β†’ (πΉβ€˜((2nd β€˜π‘₯) + 1)) ∈ 𝒫 𝑋)
130129elpwid 4612 . . . . . . . . . . 11 ((πœ‘ ∧ π‘₯ ∈ 𝐺) β†’ (πΉβ€˜((2nd β€˜π‘₯) + 1)) βŠ† 𝑋)
13113mopnuni 23947 . . . . . . . . . . . . 13 (𝐷 ∈ (∞Metβ€˜π‘‹) β†’ 𝑋 = βˆͺ 𝐽)
132105, 131syl 17 . . . . . . . . . . . 12 (πœ‘ β†’ 𝑋 = βˆͺ 𝐽)
133132adantr 482 . . . . . . . . . . 11 ((πœ‘ ∧ π‘₯ ∈ 𝐺) β†’ 𝑋 = βˆͺ 𝐽)
134130, 133sseqtrd 4023 . . . . . . . . . 10 ((πœ‘ ∧ π‘₯ ∈ 𝐺) β†’ (πΉβ€˜((2nd β€˜π‘₯) + 1)) βŠ† βˆͺ 𝐽)
135134sselda 3983 . . . . . . . . 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 9044 . . . . . . . . . . . 12 {(𝑑𝐡((2nd β€˜π‘₯) + 1))} ∈ Fin
140 inss2 4230 . . . . . . . . . . . . 13 ((π΅β€˜π‘₯) ∩ (𝑑𝐡((2nd β€˜π‘₯) + 1))) βŠ† (𝑑𝐡((2nd β€˜π‘₯) + 1))
141 ovex 7442 . . . . . . . . . . . . . . 15 (𝑑𝐡((2nd β€˜π‘₯) + 1)) ∈ V
142141unisn 4931 . . . . . . . . . . . . . 14 βˆͺ {(𝑑𝐡((2nd β€˜π‘₯) + 1))} = (𝑑𝐡((2nd β€˜π‘₯) + 1))
143 uniiun 5062 . . . . . . . . . . . . . 14 βˆͺ {(𝑑𝐡((2nd β€˜π‘₯) + 1))} = βˆͺ 𝑔 ∈ {(𝑑𝐡((2nd β€˜π‘₯) + 1))}𝑔
144142, 143eqtr3i 2763 . . . . . . . . . . . . 13 (𝑑𝐡((2nd β€˜π‘₯) + 1)) = βˆͺ 𝑔 ∈ {(𝑑𝐡((2nd β€˜π‘₯) + 1))}𝑔
145140, 144sseqtri 4019 . . . . . . . . . . . 12 ((π΅β€˜π‘₯) ∩ (𝑑𝐡((2nd β€˜π‘₯) + 1))) βŠ† βˆͺ 𝑔 ∈ {(𝑑𝐡((2nd β€˜π‘₯) + 1))}𝑔
146 vex 3479 . . . . . . . . . . . . 13 𝑔 ∈ V
14713, 14, 146heiborlem1 36679 . . . . . . . . . . . 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 4687 . . . . . . . . . . 11 (βˆƒπ‘” ∈ {(𝑑𝐡((2nd β€˜π‘₯) + 1))}𝑔 ∈ 𝐾 ↔ (𝑑𝐡((2nd β€˜π‘₯) + 1)) ∈ 𝐾)
151148, 150sylib 217 . . . . . . . . . 10 (((π΅β€˜π‘₯) ∩ (𝑑𝐡((2nd β€˜π‘₯) + 1))) ∈ 𝐾 β†’ (𝑑𝐡((2nd β€˜π‘₯) + 1)) ∈ 𝐾)
152 ovex 7442 . . . . . . . . . . . 12 ((2nd β€˜π‘₯) + 1) ∈ V
15313, 14, 6, 42, 152heiborlem2 36680 . . . . . . . . . . 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 3165 . . . . 5 ((πœ‘ ∧ π‘₯ ∈ 𝐺) β†’ (βˆƒπ‘‘ ∈ (πΉβ€˜((2nd β€˜π‘₯) + 1))((π΅β€˜π‘₯) ∩ (𝑑𝐡((2nd β€˜π‘₯) + 1))) ∈ 𝐾 β†’ βˆƒπ‘‘ ∈ βˆͺ 𝐽(𝑑𝐺((2nd β€˜π‘₯) + 1) ∧ ((π΅β€˜π‘₯) ∩ (𝑑𝐡((2nd β€˜π‘₯) + 1))) ∈ 𝐾)))
161128, 160mpd 15 . . . 4 ((πœ‘ ∧ π‘₯ ∈ 𝐺) β†’ βˆƒπ‘‘ ∈ βˆͺ 𝐽(𝑑𝐺((2nd β€˜π‘₯) + 1) ∧ ((π΅β€˜π‘₯) ∩ (𝑑𝐡((2nd β€˜π‘₯) + 1))) ∈ 𝐾))
162161ralrimiva 3147 . . 3 (πœ‘ β†’ βˆ€π‘₯ ∈ 𝐺 βˆƒπ‘‘ ∈ βˆͺ 𝐽(𝑑𝐺((2nd β€˜π‘₯) + 1) ∧ ((π΅β€˜π‘₯) ∩ (𝑑𝐡((2nd β€˜π‘₯) + 1))) ∈ 𝐾))
16313fvexi 6906 . . . . 5 𝐽 ∈ V
164163uniex 7731 . . . 4 βˆͺ 𝐽 ∈ V
165 breq1 5152 . . . . 5 (𝑑 = (π‘”β€˜π‘₯) β†’ (𝑑𝐺((2nd β€˜π‘₯) + 1) ↔ (π‘”β€˜π‘₯)𝐺((2nd β€˜π‘₯) + 1)))
166 oveq1 7416 . . . . . . 7 (𝑑 = (π‘”β€˜π‘₯) β†’ (𝑑𝐡((2nd β€˜π‘₯) + 1)) = ((π‘”β€˜π‘₯)𝐡((2nd β€˜π‘₯) + 1)))
167166ineq2d 4213 . . . . . 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 10436 . . 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 3062  βˆƒwrex 3071  Vcvv 3475   ∩ cin 3948   βŠ† wss 3949  π’« cpw 4603  {csn 4629  βŸ¨cop 4635  βˆͺ cuni 4909  βˆͺ ciun 4998   class class class wbr 5149  {copab 5211   Γ— cxp 5675  Rel wrel 5682  βŸΆwf 6540  β€˜cfv 6544  (class class class)co 7409   ∈ cmpo 7411  Ο‰com 7855  1st c1st 7973  2nd c2nd 7974   β‰ˆ cen 8936   β‰Ό cdom 8937   β‰Ί csdm 8938  Fincfn 8939  1c1 11111   + caddc 11113  β„*cxr 11247   / cdiv 11871  β„•cn 12212  2c2 12267  β„•0cn0 12472  β†‘cexp 14027  βˆžMetcxmet 20929  Metcmet 20930  ballcbl 20931  MetOpencmopn 20934  CMetccmet 24771
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 5286  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725  ax-inf2 9636  ax-cc 10430  ax-cnex 11166  ax-resscn 11167  ax-1cn 11168  ax-icn 11169  ax-addcl 11170  ax-addrcl 11171  ax-mulcl 11172  ax-mulrcl 11173  ax-mulcom 11174  ax-addass 11175  ax-mulass 11176  ax-distr 11177  ax-i2m1 11178  ax-1ne0 11179  ax-1rid 11180  ax-rnegex 11181  ax-rrecex 11182  ax-cnre 11183  ax-pre-lttri 11184  ax-pre-lttrn 11185  ax-pre-ltadd 11186  ax-pre-mulgt0 11187  ax-pre-sup 11188
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 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-int 4952  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-se 5633  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-isom 6553  df-riota 7365  df-ov 7412  df-oprab 7413  df-mpo 7414  df-om 7856  df-1st 7975  df-2nd 7976  df-frecs 8266  df-wrecs 8297  df-recs 8371  df-rdg 8410  df-1o 8466  df-er 8703  df-map 8822  df-en 8940  df-dom 8941  df-sdom 8942  df-fin 8943  df-sup 9437  df-inf 9438  df-oi 9505  df-card 9934  df-acn 9937  df-pnf 11250  df-mnf 11251  df-xr 11252  df-ltxr 11253  df-le 11254  df-sub 11446  df-neg 11447  df-div 11872  df-nn 12213  df-2 12275  df-n0 12473  df-z 12559  df-uz 12823  df-q 12933  df-rp 12975  df-xneg 13092  df-xadd 13093  df-xmul 13094  df-seq 13967  df-exp 14028  df-topgen 17389  df-psmet 20936  df-xmet 20937  df-met 20938  df-bl 20939  df-mopn 20940  df-top 22396  df-topon 22413  df-bases 22449  df-cmet 24774
This theorem is referenced by:  heiborlem10  36688
  Copyright terms: Public domain W3C validator