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

Theorem heiborlem3 34539
 Description: Lemma for heibor 34547. Using countable choice ax-cc 9655, 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 34537 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 9655 via iunctb 9794), and so we can apply ax-cc 9655 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 11714 . . . . . 6 0 ∈ V
2 fvex 6512 . . . . . . 7 (𝐹𝑡) ∈ V
3 snex 5188 . . . . . . 7 {𝑡} ∈ V
42, 3xpex 7293 . . . . . 6 ((𝐹𝑡) × {𝑡}) ∈ V
51, 4iunex 7481 . . . . 5 𝑡 ∈ ℕ0 ((𝐹𝑡) × {𝑡}) ∈ V
6 heibor.4 . . . . . . . . 9 𝐺 = {⟨𝑦, 𝑛⟩ ∣ (𝑛 ∈ ℕ0𝑦 ∈ (𝐹𝑛) ∧ (𝑦𝐵𝑛) ∈ 𝐾)}
76relopabi 5544 . . . . . . . 8 Rel 𝐺
8 1st2nd 7550 . . . . . . . 8 ((Rel 𝐺𝑥𝐺) → 𝑥 = ⟨(1st𝑥), (2nd𝑥)⟩)
97, 8mpan 677 . . . . . . 7 (𝑥𝐺𝑥 = ⟨(1st𝑥), (2nd𝑥)⟩)
109eleq1d 2850 . . . . . . . . . . 11 (𝑥𝐺 → (𝑥𝐺 ↔ ⟨(1st𝑥), (2nd𝑥)⟩ ∈ 𝐺))
11 df-br 4930 . . . . . . . . . . 11 ((1st𝑥)𝐺(2nd𝑥) ↔ ⟨(1st𝑥), (2nd𝑥)⟩ ∈ 𝐺)
1210, 11syl6bbr 281 . . . . . . . . . 10 (𝑥𝐺 → (𝑥𝐺 ↔ (1st𝑥)𝐺(2nd𝑥)))
13 heibor.1 . . . . . . . . . . 11 𝐽 = (MetOpen‘𝐷)
14 heibor.3 . . . . . . . . . . 11 𝐾 = {𝑢 ∣ ¬ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝑢 𝑣}
15 fvex 6512 . . . . . . . . . . 11 (1st𝑥) ∈ V
16 fvex 6512 . . . . . . . . . . 11 (2nd𝑥) ∈ V
1713, 14, 6, 15, 16heiborlem2 34538 . . . . . . . . . 10 ((1st𝑥)𝐺(2nd𝑥) ↔ ((2nd𝑥) ∈ ℕ0 ∧ (1st𝑥) ∈ (𝐹‘(2nd𝑥)) ∧ ((1st𝑥)𝐵(2nd𝑥)) ∈ 𝐾))
1812, 17syl6bb 279 . . . . . . . . 9 (𝑥𝐺 → (𝑥𝐺 ↔ ((2nd𝑥) ∈ ℕ0 ∧ (1st𝑥) ∈ (𝐹‘(2nd𝑥)) ∧ ((1st𝑥)𝐵(2nd𝑥)) ∈ 𝐾)))
1918ibi 259 . . . . . . . 8 (𝑥𝐺 → ((2nd𝑥) ∈ ℕ0 ∧ (1st𝑥) ∈ (𝐹‘(2nd𝑥)) ∧ ((1st𝑥)𝐵(2nd𝑥)) ∈ 𝐾))
2016snid 4473 . . . . . . . . . . . 12 (2nd𝑥) ∈ {(2nd𝑥)}
21 opelxp 5443 . . . . . . . . . . . 12 (⟨(1st𝑥), (2nd𝑥)⟩ ∈ ((𝐹‘(2nd𝑥)) × {(2nd𝑥)}) ↔ ((1st𝑥) ∈ (𝐹‘(2nd𝑥)) ∧ (2nd𝑥) ∈ {(2nd𝑥)}))
2220, 21mpbiran2 697 . . . . . . . . . . 11 (⟨(1st𝑥), (2nd𝑥)⟩ ∈ ((𝐹‘(2nd𝑥)) × {(2nd𝑥)}) ↔ (1st𝑥) ∈ (𝐹‘(2nd𝑥)))
23 fveq2 6499 . . . . . . . . . . . . . 14 (𝑡 = (2nd𝑥) → (𝐹𝑡) = (𝐹‘(2nd𝑥)))
24 sneq 4451 . . . . . . . . . . . . . 14 (𝑡 = (2nd𝑥) → {𝑡} = {(2nd𝑥)})
2523, 24xpeq12d 5438 . . . . . . . . . . . . 13 (𝑡 = (2nd𝑥) → ((𝐹𝑡) × {𝑡}) = ((𝐹‘(2nd𝑥)) × {(2nd𝑥)}))
2625eleq2d 2851 . . . . . . . . . . . 12 (𝑡 = (2nd𝑥) → (⟨(1st𝑥), (2nd𝑥)⟩ ∈ ((𝐹𝑡) × {𝑡}) ↔ ⟨(1st𝑥), (2nd𝑥)⟩ ∈ ((𝐹‘(2nd𝑥)) × {(2nd𝑥)})))
2726rspcev 3535 . . . . . . . . . . 11 (((2nd𝑥) ∈ ℕ0 ∧ ⟨(1st𝑥), (2nd𝑥)⟩ ∈ ((𝐹‘(2nd𝑥)) × {(2nd𝑥)})) → ∃𝑡 ∈ ℕ0 ⟨(1st𝑥), (2nd𝑥)⟩ ∈ ((𝐹𝑡) × {𝑡}))
2822, 27sylan2br 585 . . . . . . . . . 10 (((2nd𝑥) ∈ ℕ0 ∧ (1st𝑥) ∈ (𝐹‘(2nd𝑥))) → ∃𝑡 ∈ ℕ0 ⟨(1st𝑥), (2nd𝑥)⟩ ∈ ((𝐹𝑡) × {𝑡}))
29 eliun 4796 . . . . . . . . . 10 (⟨(1st𝑥), (2nd𝑥)⟩ ∈ 𝑡 ∈ ℕ0 ((𝐹𝑡) × {𝑡}) ↔ ∃𝑡 ∈ ℕ0 ⟨(1st𝑥), (2nd𝑥)⟩ ∈ ((𝐹𝑡) × {𝑡}))
3028, 29sylibr 226 . . . . . . . . 9 (((2nd𝑥) ∈ ℕ0 ∧ (1st𝑥) ∈ (𝐹‘(2nd𝑥))) → ⟨(1st𝑥), (2nd𝑥)⟩ ∈ 𝑡 ∈ ℕ0 ((𝐹𝑡) × {𝑡}))
31303adant3 1112 . . . . . . . 8 (((2nd𝑥) ∈ ℕ0 ∧ (1st𝑥) ∈ (𝐹‘(2nd𝑥)) ∧ ((1st𝑥)𝐵(2nd𝑥)) ∈ 𝐾) → ⟨(1st𝑥), (2nd𝑥)⟩ ∈ 𝑡 ∈ ℕ0 ((𝐹𝑡) × {𝑡}))
3219, 31syl 17 . . . . . . 7 (𝑥𝐺 → ⟨(1st𝑥), (2nd𝑥)⟩ ∈ 𝑡 ∈ ℕ0 ((𝐹𝑡) × {𝑡}))
339, 32eqeltrd 2866 . . . . . 6 (𝑥𝐺𝑥 𝑡 ∈ ℕ0 ((𝐹𝑡) × {𝑡}))
3433ssriv 3862 . . . . 5 𝐺 𝑡 ∈ ℕ0 ((𝐹𝑡) × {𝑡})
35 ssdomg 8352 . . . . 5 ( 𝑡 ∈ ℕ0 ((𝐹𝑡) × {𝑡}) ∈ V → (𝐺 𝑡 ∈ ℕ0 ((𝐹𝑡) × {𝑡}) → 𝐺 𝑡 ∈ ℕ0 ((𝐹𝑡) × {𝑡})))
365, 34, 35mp2 9 . . . 4 𝐺 𝑡 ∈ ℕ0 ((𝐹𝑡) × {𝑡})
37 nn0ennn 13162 . . . . . . 7 0 ≈ ℕ
38 nnenom 13163 . . . . . . 7 ℕ ≈ ω
3937, 38entri 8360 . . . . . 6 0 ≈ ω
40 endom 8333 . . . . . 6 (ℕ0 ≈ ω → ℕ0 ≼ ω)
4139, 40ax-mp 5 . . . . 5 0 ≼ ω
42 vex 3418 . . . . . . . 8 𝑡 ∈ V
432, 42xpsnen 8397 . . . . . . 7 ((𝐹𝑡) × {𝑡}) ≈ (𝐹𝑡)
44 inss2 4093 . . . . . . . . 9 (𝒫 𝑋 ∩ Fin) ⊆ Fin
45 heibor.7 . . . . . . . . . 10 (𝜑𝐹:ℕ0⟶(𝒫 𝑋 ∩ Fin))
4645ffvelrnda 6676 . . . . . . . . 9 ((𝜑𝑡 ∈ ℕ0) → (𝐹𝑡) ∈ (𝒫 𝑋 ∩ Fin))
4744, 46sseldi 3856 . . . . . . . 8 ((𝜑𝑡 ∈ ℕ0) → (𝐹𝑡) ∈ Fin)
48 isfinite 8909 . . . . . . . . 9 ((𝐹𝑡) ∈ Fin ↔ (𝐹𝑡) ≺ ω)
49 sdomdom 8334 . . . . . . . . 9 ((𝐹𝑡) ≺ ω → (𝐹𝑡) ≼ ω)
5048, 49sylbi 209 . . . . . . . 8 ((𝐹𝑡) ∈ Fin → (𝐹𝑡) ≼ ω)
5147, 50syl 17 . . . . . . 7 ((𝜑𝑡 ∈ ℕ0) → (𝐹𝑡) ≼ ω)
52 endomtr 8364 . . . . . . 7 ((((𝐹𝑡) × {𝑡}) ≈ (𝐹𝑡) ∧ (𝐹𝑡) ≼ ω) → ((𝐹𝑡) × {𝑡}) ≼ ω)
5343, 51, 52sylancr 578 . . . . . 6 ((𝜑𝑡 ∈ ℕ0) → ((𝐹𝑡) × {𝑡}) ≼ ω)
5453ralrimiva 3132 . . . . 5 (𝜑 → ∀𝑡 ∈ ℕ0 ((𝐹𝑡) × {𝑡}) ≼ ω)
55 iunctb 9794 . . . . 5 ((ℕ0 ≼ ω ∧ ∀𝑡 ∈ ℕ0 ((𝐹𝑡) × {𝑡}) ≼ ω) → 𝑡 ∈ ℕ0 ((𝐹𝑡) × {𝑡}) ≼ ω)
5641, 54, 55sylancr 578 . . . 4 (𝜑 𝑡 ∈ ℕ0 ((𝐹𝑡) × {𝑡}) ≼ ω)
57 domtr 8359 . . . 4 ((𝐺 𝑡 ∈ ℕ0 ((𝐹𝑡) × {𝑡}) ∧ 𝑡 ∈ ℕ0 ((𝐹𝑡) × {𝑡}) ≼ ω) → 𝐺 ≼ ω)
5836, 56, 57sylancr 578 . . 3 (𝜑𝐺 ≼ ω)
5919simp1d 1122 . . . . . . . . 9 (𝑥𝐺 → (2nd𝑥) ∈ ℕ0)
60 peano2nn0 11749 . . . . . . . . 9 ((2nd𝑥) ∈ ℕ0 → ((2nd𝑥) + 1) ∈ ℕ0)
6159, 60syl 17 . . . . . . . 8 (𝑥𝐺 → ((2nd𝑥) + 1) ∈ ℕ0)
62 ffvelrn 6674 . . . . . . . 8 ((𝐹:ℕ0⟶(𝒫 𝑋 ∩ Fin) ∧ ((2nd𝑥) + 1) ∈ ℕ0) → (𝐹‘((2nd𝑥) + 1)) ∈ (𝒫 𝑋 ∩ Fin))
6345, 61, 62syl2an 586 . . . . . . 7 ((𝜑𝑥𝐺) → (𝐹‘((2nd𝑥) + 1)) ∈ (𝒫 𝑋 ∩ Fin))
6444, 63sseldi 3856 . . . . . 6 ((𝜑𝑥𝐺) → (𝐹‘((2nd𝑥) + 1)) ∈ Fin)
65 iunin2 4859 . . . . . . . 8 𝑡 ∈ (𝐹‘((2nd𝑥) + 1))((𝐵𝑥) ∩ (𝑡𝐵((2nd𝑥) + 1))) = ((𝐵𝑥) ∩ 𝑡 ∈ (𝐹‘((2nd𝑥) + 1))(𝑡𝐵((2nd𝑥) + 1)))
66 heibor.8 . . . . . . . . . . 11 (𝜑 → ∀𝑛 ∈ ℕ0 𝑋 = 𝑦 ∈ (𝐹𝑛)(𝑦𝐵𝑛))
67 oveq1 6983 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑡 → (𝑦𝐵𝑛) = (𝑡𝐵𝑛))
6867cbviunv 4833 . . . . . . . . . . . . . . 15 𝑦 ∈ (𝐹𝑛)(𝑦𝐵𝑛) = 𝑡 ∈ (𝐹𝑛)(𝑡𝐵𝑛)
69 fveq2 6499 . . . . . . . . . . . . . . . 16 (𝑛 = ((2nd𝑥) + 1) → (𝐹𝑛) = (𝐹‘((2nd𝑥) + 1)))
7069iuneq1d 4818 . . . . . . . . . . . . . . 15 (𝑛 = ((2nd𝑥) + 1) → 𝑡 ∈ (𝐹𝑛)(𝑡𝐵𝑛) = 𝑡 ∈ (𝐹‘((2nd𝑥) + 1))(𝑡𝐵𝑛))
7168, 70syl5eq 2826 . . . . . . . . . . . . . 14 (𝑛 = ((2nd𝑥) + 1) → 𝑦 ∈ (𝐹𝑛)(𝑦𝐵𝑛) = 𝑡 ∈ (𝐹‘((2nd𝑥) + 1))(𝑡𝐵𝑛))
72 oveq2 6984 . . . . . . . . . . . . . . 15 (𝑛 = ((2nd𝑥) + 1) → (𝑡𝐵𝑛) = (𝑡𝐵((2nd𝑥) + 1)))
7372iuneq2d 4820 . . . . . . . . . . . . . 14 (𝑛 = ((2nd𝑥) + 1) → 𝑡 ∈ (𝐹‘((2nd𝑥) + 1))(𝑡𝐵𝑛) = 𝑡 ∈ (𝐹‘((2nd𝑥) + 1))(𝑡𝐵((2nd𝑥) + 1)))
7471, 73eqtrd 2814 . . . . . . . . . . . . 13 (𝑛 = ((2nd𝑥) + 1) → 𝑦 ∈ (𝐹𝑛)(𝑦𝐵𝑛) = 𝑡 ∈ (𝐹‘((2nd𝑥) + 1))(𝑡𝐵((2nd𝑥) + 1)))
7574eqeq2d 2788 . . . . . . . . . . . 12 (𝑛 = ((2nd𝑥) + 1) → (𝑋 = 𝑦 ∈ (𝐹𝑛)(𝑦𝐵𝑛) ↔ 𝑋 = 𝑡 ∈ (𝐹‘((2nd𝑥) + 1))(𝑡𝐵((2nd𝑥) + 1))))
7675rspccva 3534 . . . . . . . . . . 11 ((∀𝑛 ∈ ℕ0 𝑋 = 𝑦 ∈ (𝐹𝑛)(𝑦𝐵𝑛) ∧ ((2nd𝑥) + 1) ∈ ℕ0) → 𝑋 = 𝑡 ∈ (𝐹‘((2nd𝑥) + 1))(𝑡𝐵((2nd𝑥) + 1)))
7766, 61, 76syl2an 586 . . . . . . . . . 10 ((𝜑𝑥𝐺) → 𝑋 = 𝑡 ∈ (𝐹‘((2nd𝑥) + 1))(𝑡𝐵((2nd𝑥) + 1)))
7877ineq2d 4076 . . . . . . . . 9 ((𝜑𝑥𝐺) → ((𝐵𝑥) ∩ 𝑋) = ((𝐵𝑥) ∩ 𝑡 ∈ (𝐹‘((2nd𝑥) + 1))(𝑡𝐵((2nd𝑥) + 1))))
799fveq2d 6503 . . . . . . . . . . . . . 14 (𝑥𝐺 → (𝐵𝑥) = (𝐵‘⟨(1st𝑥), (2nd𝑥)⟩))
80 df-ov 6979 . . . . . . . . . . . . . 14 ((1st𝑥)𝐵(2nd𝑥)) = (𝐵‘⟨(1st𝑥), (2nd𝑥)⟩)
8179, 80syl6eqr 2832 . . . . . . . . . . . . 13 (𝑥𝐺 → (𝐵𝑥) = ((1st𝑥)𝐵(2nd𝑥)))
8281adantl 474 . . . . . . . . . . . 12 ((𝜑𝑥𝐺) → (𝐵𝑥) = ((1st𝑥)𝐵(2nd𝑥)))
83 inss1 4092 . . . . . . . . . . . . . . . 16 (𝒫 𝑋 ∩ Fin) ⊆ 𝒫 𝑋
84 ffvelrn 6674 . . . . . . . . . . . . . . . . 17 ((𝐹:ℕ0⟶(𝒫 𝑋 ∩ Fin) ∧ (2nd𝑥) ∈ ℕ0) → (𝐹‘(2nd𝑥)) ∈ (𝒫 𝑋 ∩ Fin))
8545, 59, 84syl2an 586 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝐺) → (𝐹‘(2nd𝑥)) ∈ (𝒫 𝑋 ∩ Fin))
8683, 85sseldi 3856 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝐺) → (𝐹‘(2nd𝑥)) ∈ 𝒫 𝑋)
8786elpwid 4434 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐺) → (𝐹‘(2nd𝑥)) ⊆ 𝑋)
8819simp2d 1123 . . . . . . . . . . . . . . 15 (𝑥𝐺 → (1st𝑥) ∈ (𝐹‘(2nd𝑥)))
8988adantl 474 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐺) → (1st𝑥) ∈ (𝐹‘(2nd𝑥)))
9087, 89sseldd 3859 . . . . . . . . . . . . 13 ((𝜑𝑥𝐺) → (1st𝑥) ∈ 𝑋)
9159adantl 474 . . . . . . . . . . . . 13 ((𝜑𝑥𝐺) → (2nd𝑥) ∈ ℕ0)
92 oveq1 6983 . . . . . . . . . . . . . 14 (𝑧 = (1st𝑥) → (𝑧(ball‘𝐷)(1 / (2↑𝑚))) = ((1st𝑥)(ball‘𝐷)(1 / (2↑𝑚))))
93 oveq2 6984 . . . . . . . . . . . . . . . 16 (𝑚 = (2nd𝑥) → (2↑𝑚) = (2↑(2nd𝑥)))
9493oveq2d 6992 . . . . . . . . . . . . . . 15 (𝑚 = (2nd𝑥) → (1 / (2↑𝑚)) = (1 / (2↑(2nd𝑥))))
9594oveq2d 6992 . . . . . . . . . . . . . 14 (𝑚 = (2nd𝑥) → ((1st𝑥)(ball‘𝐷)(1 / (2↑𝑚))) = ((1st𝑥)(ball‘𝐷)(1 / (2↑(2nd𝑥)))))
96 heibor.5 . . . . . . . . . . . . . 14 𝐵 = (𝑧𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))
97 ovex 7008 . . . . . . . . . . . . . 14 ((1st𝑥)(ball‘𝐷)(1 / (2↑(2nd𝑥)))) ∈ V
9892, 95, 96, 97ovmpo 7126 . . . . . . . . . . . . 13 (((1st𝑥) ∈ 𝑋 ∧ (2nd𝑥) ∈ ℕ0) → ((1st𝑥)𝐵(2nd𝑥)) = ((1st𝑥)(ball‘𝐷)(1 / (2↑(2nd𝑥)))))
9990, 91, 98syl2anc 576 . . . . . . . . . . . 12 ((𝜑𝑥𝐺) → ((1st𝑥)𝐵(2nd𝑥)) = ((1st𝑥)(ball‘𝐷)(1 / (2↑(2nd𝑥)))))
10082, 99eqtrd 2814 . . . . . . . . . . 11 ((𝜑𝑥𝐺) → (𝐵𝑥) = ((1st𝑥)(ball‘𝐷)(1 / (2↑(2nd𝑥)))))
101 heibor.6 . . . . . . . . . . . . . . 15 (𝜑𝐷 ∈ (CMet‘𝑋))
102 cmetmet 23592 . . . . . . . . . . . . . . 15 (𝐷 ∈ (CMet‘𝑋) → 𝐷 ∈ (Met‘𝑋))
103101, 102syl 17 . . . . . . . . . . . . . 14 (𝜑𝐷 ∈ (Met‘𝑋))
104 metxmet 22647 . . . . . . . . . . . . . 14 (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ (∞Met‘𝑋))
105103, 104syl 17 . . . . . . . . . . . . 13 (𝜑𝐷 ∈ (∞Met‘𝑋))
106105adantr 473 . . . . . . . . . . . 12 ((𝜑𝑥𝐺) → 𝐷 ∈ (∞Met‘𝑋))
107 2nn 11513 . . . . . . . . . . . . . . . 16 2 ∈ ℕ
108 nnexpcl 13257 . . . . . . . . . . . . . . . 16 ((2 ∈ ℕ ∧ (2nd𝑥) ∈ ℕ0) → (2↑(2nd𝑥)) ∈ ℕ)
109107, 91, 108sylancr 578 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝐺) → (2↑(2nd𝑥)) ∈ ℕ)
110109nnrpd 12246 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐺) → (2↑(2nd𝑥)) ∈ ℝ+)
111110rpreccld 12258 . . . . . . . . . . . . 13 ((𝜑𝑥𝐺) → (1 / (2↑(2nd𝑥))) ∈ ℝ+)
112111rpxrd 12249 . . . . . . . . . . . 12 ((𝜑𝑥𝐺) → (1 / (2↑(2nd𝑥))) ∈ ℝ*)
113 blssm 22731 . . . . . . . . . . . 12 ((𝐷 ∈ (∞Met‘𝑋) ∧ (1st𝑥) ∈ 𝑋 ∧ (1 / (2↑(2nd𝑥))) ∈ ℝ*) → ((1st𝑥)(ball‘𝐷)(1 / (2↑(2nd𝑥)))) ⊆ 𝑋)
114106, 90, 112, 113syl3anc 1351 . . . . . . . . . . 11 ((𝜑𝑥𝐺) → ((1st𝑥)(ball‘𝐷)(1 / (2↑(2nd𝑥)))) ⊆ 𝑋)
115100, 114eqsstrd 3895 . . . . . . . . . 10 ((𝜑𝑥𝐺) → (𝐵𝑥) ⊆ 𝑋)
116 df-ss 3843 . . . . . . . . . 10 ((𝐵𝑥) ⊆ 𝑋 ↔ ((𝐵𝑥) ∩ 𝑋) = (𝐵𝑥))
117115, 116sylib 210 . . . . . . . . 9 ((𝜑𝑥𝐺) → ((𝐵𝑥) ∩ 𝑋) = (𝐵𝑥))
11878, 117eqtr3d 2816 . . . . . . . 8 ((𝜑𝑥𝐺) → ((𝐵𝑥) ∩ 𝑡 ∈ (𝐹‘((2nd𝑥) + 1))(𝑡𝐵((2nd𝑥) + 1))) = (𝐵𝑥))
11965, 118syl5eq 2826 . . . . . . 7 ((𝜑𝑥𝐺) → 𝑡 ∈ (𝐹‘((2nd𝑥) + 1))((𝐵𝑥) ∩ (𝑡𝐵((2nd𝑥) + 1))) = (𝐵𝑥))
120 eqimss2 3914 . . . . . . 7 ( 𝑡 ∈ (𝐹‘((2nd𝑥) + 1))((𝐵𝑥) ∩ (𝑡𝐵((2nd𝑥) + 1))) = (𝐵𝑥) → (𝐵𝑥) ⊆ 𝑡 ∈ (𝐹‘((2nd𝑥) + 1))((𝐵𝑥) ∩ (𝑡𝐵((2nd𝑥) + 1))))
121119, 120syl 17 . . . . . 6 ((𝜑𝑥𝐺) → (𝐵𝑥) ⊆ 𝑡 ∈ (𝐹‘((2nd𝑥) + 1))((𝐵𝑥) ∩ (𝑡𝐵((2nd𝑥) + 1))))
12219simp3d 1124 . . . . . . . 8 (𝑥𝐺 → ((1st𝑥)𝐵(2nd𝑥)) ∈ 𝐾)
12381, 122eqeltrd 2866 . . . . . . 7 (𝑥𝐺 → (𝐵𝑥) ∈ 𝐾)
124123adantl 474 . . . . . 6 ((𝜑𝑥𝐺) → (𝐵𝑥) ∈ 𝐾)
125 fvex 6512 . . . . . . . 8 (𝐵𝑥) ∈ V
126125inex1 5078 . . . . . . 7 ((𝐵𝑥) ∩ (𝑡𝐵((2nd𝑥) + 1))) ∈ V
12713, 14, 126heiborlem1 34537 . . . . . 6 (((𝐹‘((2nd𝑥) + 1)) ∈ Fin ∧ (𝐵𝑥) ⊆ 𝑡 ∈ (𝐹‘((2nd𝑥) + 1))((𝐵𝑥) ∩ (𝑡𝐵((2nd𝑥) + 1))) ∧ (𝐵𝑥) ∈ 𝐾) → ∃𝑡 ∈ (𝐹‘((2nd𝑥) + 1))((𝐵𝑥) ∩ (𝑡𝐵((2nd𝑥) + 1))) ∈ 𝐾)
12864, 121, 124, 127syl3anc 1351 . . . . 5 ((𝜑𝑥𝐺) → ∃𝑡 ∈ (𝐹‘((2nd𝑥) + 1))((𝐵𝑥) ∩ (𝑡𝐵((2nd𝑥) + 1))) ∈ 𝐾)
12983, 63sseldi 3856 . . . . . . . . . . . 12 ((𝜑𝑥𝐺) → (𝐹‘((2nd𝑥) + 1)) ∈ 𝒫 𝑋)
130129elpwid 4434 . . . . . . . . . . 11 ((𝜑𝑥𝐺) → (𝐹‘((2nd𝑥) + 1)) ⊆ 𝑋)
13113mopnuni 22754 . . . . . . . . . . . . 13 (𝐷 ∈ (∞Met‘𝑋) → 𝑋 = 𝐽)
132105, 131syl 17 . . . . . . . . . . . 12 (𝜑𝑋 = 𝐽)
133132adantr 473 . . . . . . . . . . 11 ((𝜑𝑥𝐺) → 𝑋 = 𝐽)
134130, 133sseqtrd 3897 . . . . . . . . . 10 ((𝜑𝑥𝐺) → (𝐹‘((2nd𝑥) + 1)) ⊆ 𝐽)
135134sselda 3858 . . . . . . . . 9 (((𝜑𝑥𝐺) ∧ 𝑡 ∈ (𝐹‘((2nd𝑥) + 1))) → 𝑡 𝐽)
136135adantrr 704 . . . . . . . 8 (((𝜑𝑥𝐺) ∧ (𝑡 ∈ (𝐹‘((2nd𝑥) + 1)) ∧ ((𝐵𝑥) ∩ (𝑡𝐵((2nd𝑥) + 1))) ∈ 𝐾)) → 𝑡 𝐽)
13761adantl 474 . . . . . . . . . 10 ((𝜑𝑥𝐺) → ((2nd𝑥) + 1) ∈ ℕ0)
138 id 22 . . . . . . . . . 10 (𝑡 ∈ (𝐹‘((2nd𝑥) + 1)) → 𝑡 ∈ (𝐹‘((2nd𝑥) + 1)))
139 snfi 8391 . . . . . . . . . . . 12 {(𝑡𝐵((2nd𝑥) + 1))} ∈ Fin
140 inss2 4093 . . . . . . . . . . . . 13 ((𝐵𝑥) ∩ (𝑡𝐵((2nd𝑥) + 1))) ⊆ (𝑡𝐵((2nd𝑥) + 1))
141 ovex 7008 . . . . . . . . . . . . . . 15 (𝑡𝐵((2nd𝑥) + 1)) ∈ V
142141unisn 4728 . . . . . . . . . . . . . 14 {(𝑡𝐵((2nd𝑥) + 1))} = (𝑡𝐵((2nd𝑥) + 1))
143 uniiun 4848 . . . . . . . . . . . . . 14 {(𝑡𝐵((2nd𝑥) + 1))} = 𝑔 ∈ {(𝑡𝐵((2nd𝑥) + 1))}𝑔
144142, 143eqtr3i 2804 . . . . . . . . . . . . 13 (𝑡𝐵((2nd𝑥) + 1)) = 𝑔 ∈ {(𝑡𝐵((2nd𝑥) + 1))}𝑔
145140, 144sseqtri 3893 . . . . . . . . . . . 12 ((𝐵𝑥) ∩ (𝑡𝐵((2nd𝑥) + 1))) ⊆ 𝑔 ∈ {(𝑡𝐵((2nd𝑥) + 1))}𝑔
146 vex 3418 . . . . . . . . . . . . 13 𝑔 ∈ V
14713, 14, 146heiborlem1 34537 . . . . . . . . . . . 12 (({(𝑡𝐵((2nd𝑥) + 1))} ∈ Fin ∧ ((𝐵𝑥) ∩ (𝑡𝐵((2nd𝑥) + 1))) ⊆ 𝑔 ∈ {(𝑡𝐵((2nd𝑥) + 1))}𝑔 ∧ ((𝐵𝑥) ∩ (𝑡𝐵((2nd𝑥) + 1))) ∈ 𝐾) → ∃𝑔 ∈ {(𝑡𝐵((2nd𝑥) + 1))}𝑔𝐾)
148139, 145, 147mp3an12 1430 . . . . . . . . . . 11 (((𝐵𝑥) ∩ (𝑡𝐵((2nd𝑥) + 1))) ∈ 𝐾 → ∃𝑔 ∈ {(𝑡𝐵((2nd𝑥) + 1))}𝑔𝐾)
149 eleq1 2853 . . . . . . . . . . . 12 (𝑔 = (𝑡𝐵((2nd𝑥) + 1)) → (𝑔𝐾 ↔ (𝑡𝐵((2nd𝑥) + 1)) ∈ 𝐾))
150141, 149rexsn 4494 . . . . . . . . . . 11 (∃𝑔 ∈ {(𝑡𝐵((2nd𝑥) + 1))}𝑔𝐾 ↔ (𝑡𝐵((2nd𝑥) + 1)) ∈ 𝐾)
151148, 150sylib 210 . . . . . . . . . 10 (((𝐵𝑥) ∩ (𝑡𝐵((2nd𝑥) + 1))) ∈ 𝐾 → (𝑡𝐵((2nd𝑥) + 1)) ∈ 𝐾)
152 ovex 7008 . . . . . . . . . . . 12 ((2nd𝑥) + 1) ∈ V
15313, 14, 6, 42, 152heiborlem2 34538 . . . . . . . . . . 11 (𝑡𝐺((2nd𝑥) + 1) ↔ (((2nd𝑥) + 1) ∈ ℕ0𝑡 ∈ (𝐹‘((2nd𝑥) + 1)) ∧ (𝑡𝐵((2nd𝑥) + 1)) ∈ 𝐾))
154153biimpri 220 . . . . . . . . . 10 ((((2nd𝑥) + 1) ∈ ℕ0𝑡 ∈ (𝐹‘((2nd𝑥) + 1)) ∧ (𝑡𝐵((2nd𝑥) + 1)) ∈ 𝐾) → 𝑡𝐺((2nd𝑥) + 1))
155137, 138, 151, 154syl3an 1140 . . . . . . . . 9 (((𝜑𝑥𝐺) ∧ 𝑡 ∈ (𝐹‘((2nd𝑥) + 1)) ∧ ((𝐵𝑥) ∩ (𝑡𝐵((2nd𝑥) + 1))) ∈ 𝐾) → 𝑡𝐺((2nd𝑥) + 1))
1561553expb 1100 . . . . . . . 8 (((𝜑𝑥𝐺) ∧ (𝑡 ∈ (𝐹‘((2nd𝑥) + 1)) ∧ ((𝐵𝑥) ∩ (𝑡𝐵((2nd𝑥) + 1))) ∈ 𝐾)) → 𝑡𝐺((2nd𝑥) + 1))
157 simprr 760 . . . . . . . 8 (((𝜑𝑥𝐺) ∧ (𝑡 ∈ (𝐹‘((2nd𝑥) + 1)) ∧ ((𝐵𝑥) ∩ (𝑡𝐵((2nd𝑥) + 1))) ∈ 𝐾)) → ((𝐵𝑥) ∩ (𝑡𝐵((2nd𝑥) + 1))) ∈ 𝐾)
158136, 156, 157jca32 508 . . . . . . 7 (((𝜑𝑥𝐺) ∧ (𝑡 ∈ (𝐹‘((2nd𝑥) + 1)) ∧ ((𝐵𝑥) ∩ (𝑡𝐵((2nd𝑥) + 1))) ∈ 𝐾)) → (𝑡 𝐽 ∧ (𝑡𝐺((2nd𝑥) + 1) ∧ ((𝐵𝑥) ∩ (𝑡𝐵((2nd𝑥) + 1))) ∈ 𝐾)))
159158ex 405 . . . . . 6 ((𝜑𝑥𝐺) → ((𝑡 ∈ (𝐹‘((2nd𝑥) + 1)) ∧ ((𝐵𝑥) ∩ (𝑡𝐵((2nd𝑥) + 1))) ∈ 𝐾) → (𝑡 𝐽 ∧ (𝑡𝐺((2nd𝑥) + 1) ∧ ((𝐵𝑥) ∩ (𝑡𝐵((2nd𝑥) + 1))) ∈ 𝐾))))
160159reximdv2 3216 . . . . 5 ((𝜑𝑥𝐺) → (∃𝑡 ∈ (𝐹‘((2nd𝑥) + 1))((𝐵𝑥) ∩ (𝑡𝐵((2nd𝑥) + 1))) ∈ 𝐾 → ∃𝑡 𝐽(𝑡𝐺((2nd𝑥) + 1) ∧ ((𝐵𝑥) ∩ (𝑡𝐵((2nd𝑥) + 1))) ∈ 𝐾)))
161128, 160mpd 15 . . . 4 ((𝜑𝑥𝐺) → ∃𝑡 𝐽(𝑡𝐺((2nd𝑥) + 1) ∧ ((𝐵𝑥) ∩ (𝑡𝐵((2nd𝑥) + 1))) ∈ 𝐾))
162161ralrimiva 3132 . . 3 (𝜑 → ∀𝑥𝐺𝑡 𝐽(𝑡𝐺((2nd𝑥) + 1) ∧ ((𝐵𝑥) ∩ (𝑡𝐵((2nd𝑥) + 1))) ∈ 𝐾))
16313fvexi 6513 . . . . 5 𝐽 ∈ V
164163uniex 7283 . . . 4 𝐽 ∈ V
165 breq1 4932 . . . . 5 (𝑡 = (𝑔𝑥) → (𝑡𝐺((2nd𝑥) + 1) ↔ (𝑔𝑥)𝐺((2nd𝑥) + 1)))
166 oveq1 6983 . . . . . . 7 (𝑡 = (𝑔𝑥) → (𝑡𝐵((2nd𝑥) + 1)) = ((𝑔𝑥)𝐵((2nd𝑥) + 1)))
167166ineq2d 4076 . . . . . 6 (𝑡 = (𝑔𝑥) → ((𝐵𝑥) ∩ (𝑡𝐵((2nd𝑥) + 1))) = ((𝐵𝑥) ∩ ((𝑔𝑥)𝐵((2nd𝑥) + 1))))
168167eleq1d 2850 . . . . 5 (𝑡 = (𝑔𝑥) → (((𝐵𝑥) ∩ (𝑡𝐵((2nd𝑥) + 1))) ∈ 𝐾 ↔ ((𝐵𝑥) ∩ ((𝑔𝑥)𝐵((2nd𝑥) + 1))) ∈ 𝐾))
169165, 168anbi12d 621 . . . 4 (𝑡 = (𝑔𝑥) → ((𝑡𝐺((2nd𝑥) + 1) ∧ ((𝐵𝑥) ∩ (𝑡𝐵((2nd𝑥) + 1))) ∈ 𝐾) ↔ ((𝑔𝑥)𝐺((2nd𝑥) + 1) ∧ ((𝐵𝑥) ∩ ((𝑔𝑥)𝐵((2nd𝑥) + 1))) ∈ 𝐾)))
170164, 169axcc4dom 9661 . . 3 ((𝐺 ≼ ω ∧ ∀𝑥𝐺𝑡 𝐽(𝑡𝐺((2nd𝑥) + 1) ∧ ((𝐵𝑥) ∩ (𝑡𝐵((2nd𝑥) + 1))) ∈ 𝐾)) → ∃𝑔(𝑔:𝐺 𝐽 ∧ ∀𝑥𝐺 ((𝑔𝑥)𝐺((2nd𝑥) + 1) ∧ ((𝐵𝑥) ∩ ((𝑔𝑥)𝐵((2nd𝑥) + 1))) ∈ 𝐾)))
17158, 162, 170syl2anc 576 . 2 (𝜑 → ∃𝑔(𝑔:𝐺 𝐽 ∧ ∀𝑥𝐺 ((𝑔𝑥)𝐺((2nd𝑥) + 1) ∧ ((𝐵𝑥) ∩ ((𝑔𝑥)𝐵((2nd𝑥) + 1))) ∈ 𝐾)))
172 exsimpr 1832 . 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 387   ∧ w3a 1068   = wceq 1507  ∃wex 1742   ∈ wcel 2050  {cab 2758  ∀wral 3088  ∃wrex 3089  Vcvv 3415   ∩ cin 3828   ⊆ wss 3829  𝒫 cpw 4422  {csn 4441  ⟨cop 4447  ∪ cuni 4712  ∪ ciun 4792   class class class wbr 4929  {copab 4991   × cxp 5405  Rel wrel 5412  ⟶wf 6184  ‘cfv 6188  (class class class)co 6976   ∈ cmpo 6978  ωcom 7396  1st c1st 7499  2nd c2nd 7500   ≈ cen 8303   ≼ cdom 8304   ≺ csdm 8305  Fincfn 8306  1c1 10336   + caddc 10338  ℝ*cxr 10473   / cdiv 11098  ℕcn 11439  2c2 11495  ℕ0cn0 11707  ↑cexp 13244  ∞Metcxmet 20232  Metcmet 20233  ballcbl 20234  MetOpencmopn 20237  CMetccmet 23560 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2750  ax-rep 5049  ax-sep 5060  ax-nul 5067  ax-pow 5119  ax-pr 5186  ax-un 7279  ax-inf2 8898  ax-cc 9655  ax-cnex 10391  ax-resscn 10392  ax-1cn 10393  ax-icn 10394  ax-addcl 10395  ax-addrcl 10396  ax-mulcl 10397  ax-mulrcl 10398  ax-mulcom 10399  ax-addass 10400  ax-mulass 10401  ax-distr 10402  ax-i2m1 10403  ax-1ne0 10404  ax-1rid 10405  ax-rnegex 10406  ax-rrecex 10407  ax-cnre 10408  ax-pre-lttri 10409  ax-pre-lttrn 10410  ax-pre-ltadd 10411  ax-pre-mulgt0 10412  ax-pre-sup 10413 This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3or 1069  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2584  df-clab 2759  df-cleq 2771  df-clel 2846  df-nfc 2918  df-ne 2968  df-nel 3074  df-ral 3093  df-rex 3094  df-reu 3095  df-rmo 3096  df-rab 3097  df-v 3417  df-sbc 3682  df-csb 3787  df-dif 3832  df-un 3834  df-in 3836  df-ss 3843  df-pss 3845  df-nul 4179  df-if 4351  df-pw 4424  df-sn 4442  df-pr 4444  df-tp 4446  df-op 4448  df-uni 4713  df-int 4750  df-iun 4794  df-br 4930  df-opab 4992  df-mpt 5009  df-tr 5031  df-id 5312  df-eprel 5317  df-po 5326  df-so 5327  df-fr 5366  df-se 5367  df-we 5368  df-xp 5413  df-rel 5414  df-cnv 5415  df-co 5416  df-dm 5417  df-rn 5418  df-res 5419  df-ima 5420  df-pred 5986  df-ord 6032  df-on 6033  df-lim 6034  df-suc 6035  df-iota 6152  df-fun 6190  df-fn 6191  df-f 6192  df-f1 6193  df-fo 6194  df-f1o 6195  df-fv 6196  df-isom 6197  df-riota 6937  df-ov 6979  df-oprab 6980  df-mpo 6981  df-om 7397  df-1st 7501  df-2nd 7502  df-wrecs 7750  df-recs 7812  df-rdg 7850  df-1o 7905  df-oadd 7909  df-er 8089  df-map 8208  df-en 8307  df-dom 8308  df-sdom 8309  df-fin 8310  df-sup 8701  df-inf 8702  df-oi 8769  df-card 9162  df-acn 9165  df-pnf 10476  df-mnf 10477  df-xr 10478  df-ltxr 10479  df-le 10480  df-sub 10672  df-neg 10673  df-div 11099  df-nn 11440  df-2 11503  df-n0 11708  df-z 11794  df-uz 12059  df-q 12163  df-rp 12205  df-xneg 12324  df-xadd 12325  df-xmul 12326  df-seq 13185  df-exp 13245  df-topgen 16573  df-psmet 20239  df-xmet 20240  df-met 20241  df-bl 20242  df-mopn 20243  df-top 21206  df-topon 21223  df-bases 21258  df-cmet 23563 This theorem is referenced by:  heiborlem10  34546
 Copyright terms: Public domain W3C validator