| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | nn0ex 12534 | . . . . . 6
⊢
ℕ0 ∈ V | 
| 2 |  | fvex 6918 | . . . . . . 7
⊢ (𝐹‘𝑡) ∈ V | 
| 3 |  | vsnex 5433 | . . . . . . 7
⊢ {𝑡} ∈ V | 
| 4 | 2, 3 | xpex 7774 | . . . . . 6
⊢ ((𝐹‘𝑡) × {𝑡}) ∈ V | 
| 5 | 1, 4 | iunex 7994 | . . . . 5
⊢ ∪ 𝑡 ∈ ℕ0 ((𝐹‘𝑡) × {𝑡}) ∈ V | 
| 6 |  | heibor.4 | . . . . . . . . 9
⊢ 𝐺 = {〈𝑦, 𝑛〉 ∣ (𝑛 ∈ ℕ0 ∧ 𝑦 ∈ (𝐹‘𝑛) ∧ (𝑦𝐵𝑛) ∈ 𝐾)} | 
| 7 | 6 | relopabiv 5829 | . . . . . . . 8
⊢ Rel 𝐺 | 
| 8 |  | 1st2nd 8065 | . . . . . . . 8
⊢ ((Rel
𝐺 ∧ 𝑥 ∈ 𝐺) → 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) | 
| 9 | 7, 8 | mpan 690 | . . . . . . 7
⊢ (𝑥 ∈ 𝐺 → 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) | 
| 10 | 9 | eleq1d 2825 | . . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐺 → (𝑥 ∈ 𝐺 ↔ 〈(1st ‘𝑥), (2nd ‘𝑥)〉 ∈ 𝐺)) | 
| 11 |  | df-br 5143 | . . . . . . . . . . 11
⊢
((1st ‘𝑥)𝐺(2nd ‘𝑥) ↔ 〈(1st ‘𝑥), (2nd ‘𝑥)〉 ∈ 𝐺) | 
| 12 | 10, 11 | bitr4di 289 | . . . . . . . . . 10
⊢ (𝑥 ∈ 𝐺 → (𝑥 ∈ 𝐺 ↔ (1st ‘𝑥)𝐺(2nd ‘𝑥))) | 
| 13 |  | heibor.1 | . . . . . . . . . . 11
⊢ 𝐽 = (MetOpen‘𝐷) | 
| 14 |  | heibor.3 | . . . . . . . . . . 11
⊢ 𝐾 = {𝑢 ∣ ¬ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝑢 ⊆ ∪ 𝑣} | 
| 15 |  | fvex 6918 | . . . . . . . . . . 11
⊢
(1st ‘𝑥) ∈ V | 
| 16 |  | fvex 6918 | . . . . . . . . . . 11
⊢
(2nd ‘𝑥) ∈ V | 
| 17 | 13, 14, 6, 15, 16 | heiborlem2 37820 | . . . . . . . . . 10
⊢
((1st ‘𝑥)𝐺(2nd ‘𝑥) ↔ ((2nd ‘𝑥) ∈ ℕ0
∧ (1st ‘𝑥) ∈ (𝐹‘(2nd ‘𝑥)) ∧ ((1st
‘𝑥)𝐵(2nd ‘𝑥)) ∈ 𝐾)) | 
| 18 | 12, 17 | bitrdi 287 | . . . . . . . . 9
⊢ (𝑥 ∈ 𝐺 → (𝑥 ∈ 𝐺 ↔ ((2nd ‘𝑥) ∈ ℕ0
∧ (1st ‘𝑥) ∈ (𝐹‘(2nd ‘𝑥)) ∧ ((1st
‘𝑥)𝐵(2nd ‘𝑥)) ∈ 𝐾))) | 
| 19 | 18 | ibi 267 | . . . . . . . 8
⊢ (𝑥 ∈ 𝐺 → ((2nd ‘𝑥) ∈ ℕ0
∧ (1st ‘𝑥) ∈ (𝐹‘(2nd ‘𝑥)) ∧ ((1st
‘𝑥)𝐵(2nd ‘𝑥)) ∈ 𝐾)) | 
| 20 | 16 | snid 4661 | . . . . . . . . . . . 12
⊢
(2nd ‘𝑥) ∈ {(2nd ‘𝑥)} | 
| 21 |  | opelxp 5720 | . . . . . . . . . . . 12
⊢
(〈(1st ‘𝑥), (2nd ‘𝑥)〉 ∈ ((𝐹‘(2nd ‘𝑥)) × {(2nd
‘𝑥)}) ↔
((1st ‘𝑥)
∈ (𝐹‘(2nd ‘𝑥)) ∧ (2nd
‘𝑥) ∈
{(2nd ‘𝑥)})) | 
| 22 | 20, 21 | mpbiran2 710 | . . . . . . . . . . 11
⊢
(〈(1st ‘𝑥), (2nd ‘𝑥)〉 ∈ ((𝐹‘(2nd ‘𝑥)) × {(2nd
‘𝑥)}) ↔
(1st ‘𝑥)
∈ (𝐹‘(2nd ‘𝑥))) | 
| 23 |  | fveq2 6905 | . . . . . . . . . . . . . 14
⊢ (𝑡 = (2nd ‘𝑥) → (𝐹‘𝑡) = (𝐹‘(2nd ‘𝑥))) | 
| 24 |  | sneq 4635 | . . . . . . . . . . . . . 14
⊢ (𝑡 = (2nd ‘𝑥) → {𝑡} = {(2nd ‘𝑥)}) | 
| 25 | 23, 24 | xpeq12d 5715 | . . . . . . . . . . . . 13
⊢ (𝑡 = (2nd ‘𝑥) → ((𝐹‘𝑡) × {𝑡}) = ((𝐹‘(2nd ‘𝑥)) × {(2nd
‘𝑥)})) | 
| 26 | 25 | eleq2d 2826 | . . . . . . . . . . . 12
⊢ (𝑡 = (2nd ‘𝑥) → (〈(1st
‘𝑥), (2nd
‘𝑥)〉 ∈
((𝐹‘𝑡) × {𝑡}) ↔ 〈(1st ‘𝑥), (2nd ‘𝑥)〉 ∈ ((𝐹‘(2nd
‘𝑥)) ×
{(2nd ‘𝑥)}))) | 
| 27 | 26 | rspcev 3621 | . . . . . . . . . . 11
⊢
(((2nd ‘𝑥) ∈ ℕ0 ∧
〈(1st ‘𝑥), (2nd ‘𝑥)〉 ∈ ((𝐹‘(2nd ‘𝑥)) × {(2nd
‘𝑥)})) →
∃𝑡 ∈
ℕ0 〈(1st ‘𝑥), (2nd ‘𝑥)〉 ∈ ((𝐹‘𝑡) × {𝑡})) | 
| 28 | 22, 27 | sylan2br 595 | . . . . . . . . . 10
⊢
(((2nd ‘𝑥) ∈ ℕ0 ∧
(1st ‘𝑥)
∈ (𝐹‘(2nd ‘𝑥))) → ∃𝑡 ∈ ℕ0
〈(1st ‘𝑥), (2nd ‘𝑥)〉 ∈ ((𝐹‘𝑡) × {𝑡})) | 
| 29 |  | eliun 4994 | . . . . . . . . . 10
⊢
(〈(1st ‘𝑥), (2nd ‘𝑥)〉 ∈ ∪ 𝑡 ∈ ℕ0 ((𝐹‘𝑡) × {𝑡}) ↔ ∃𝑡 ∈ ℕ0
〈(1st ‘𝑥), (2nd ‘𝑥)〉 ∈ ((𝐹‘𝑡) × {𝑡})) | 
| 30 | 28, 29 | sylibr 234 | . . . . . . . . 9
⊢
(((2nd ‘𝑥) ∈ ℕ0 ∧
(1st ‘𝑥)
∈ (𝐹‘(2nd ‘𝑥))) → 〈(1st
‘𝑥), (2nd
‘𝑥)〉 ∈
∪ 𝑡 ∈ ℕ0 ((𝐹‘𝑡) × {𝑡})) | 
| 31 | 30 | 3adant3 1132 | . . . . . . . 8
⊢
(((2nd ‘𝑥) ∈ ℕ0 ∧
(1st ‘𝑥)
∈ (𝐹‘(2nd ‘𝑥)) ∧ ((1st
‘𝑥)𝐵(2nd ‘𝑥)) ∈ 𝐾) → 〈(1st ‘𝑥), (2nd ‘𝑥)〉 ∈ ∪ 𝑡 ∈ ℕ0 ((𝐹‘𝑡) × {𝑡})) | 
| 32 | 19, 31 | syl 17 | . . . . . . 7
⊢ (𝑥 ∈ 𝐺 → 〈(1st ‘𝑥), (2nd ‘𝑥)〉 ∈ ∪ 𝑡 ∈ ℕ0 ((𝐹‘𝑡) × {𝑡})) | 
| 33 | 9, 32 | eqeltrd 2840 | . . . . . 6
⊢ (𝑥 ∈ 𝐺 → 𝑥 ∈ ∪
𝑡 ∈
ℕ0 ((𝐹‘𝑡) × {𝑡})) | 
| 34 | 33 | ssriv 3986 | . . . . 5
⊢ 𝐺 ⊆ ∪ 𝑡 ∈ ℕ0 ((𝐹‘𝑡) × {𝑡}) | 
| 35 |  | ssdomg 9041 | . . . . 5
⊢ (∪ 𝑡 ∈ ℕ0 ((𝐹‘𝑡) × {𝑡}) ∈ V → (𝐺 ⊆ ∪
𝑡 ∈
ℕ0 ((𝐹‘𝑡) × {𝑡}) → 𝐺 ≼ ∪
𝑡 ∈
ℕ0 ((𝐹‘𝑡) × {𝑡}))) | 
| 36 | 5, 34, 35 | mp2 9 | . . . 4
⊢ 𝐺 ≼ ∪ 𝑡 ∈ ℕ0 ((𝐹‘𝑡) × {𝑡}) | 
| 37 |  | nn0ennn 14021 | . . . . . . 7
⊢
ℕ0 ≈ ℕ | 
| 38 |  | nnenom 14022 | . . . . . . 7
⊢ ℕ
≈ ω | 
| 39 | 37, 38 | entri 9049 | . . . . . 6
⊢
ℕ0 ≈ ω | 
| 40 |  | endom 9020 | . . . . . 6
⊢
(ℕ0 ≈ ω → ℕ0 ≼
ω) | 
| 41 | 39, 40 | ax-mp 5 | . . . . 5
⊢
ℕ0 ≼ ω | 
| 42 |  | vex 3483 | . . . . . . . 8
⊢ 𝑡 ∈ V | 
| 43 | 2, 42 | xpsnen 9096 | . . . . . . 7
⊢ ((𝐹‘𝑡) × {𝑡}) ≈ (𝐹‘𝑡) | 
| 44 |  | inss2 4237 | . . . . . . . . 9
⊢
(𝒫 𝑋 ∩
Fin) ⊆ Fin | 
| 45 |  | heibor.7 | . . . . . . . . . 10
⊢ (𝜑 → 𝐹:ℕ0⟶(𝒫 𝑋 ∩ Fin)) | 
| 46 | 45 | ffvelcdmda 7103 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ ℕ0) → (𝐹‘𝑡) ∈ (𝒫 𝑋 ∩ Fin)) | 
| 47 | 44, 46 | sselid 3980 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ ℕ0) → (𝐹‘𝑡) ∈ Fin) | 
| 48 |  | isfinite 9693 | . . . . . . . . 9
⊢ ((𝐹‘𝑡) ∈ Fin ↔ (𝐹‘𝑡) ≺ ω) | 
| 49 |  | sdomdom 9021 | . . . . . . . . 9
⊢ ((𝐹‘𝑡) ≺ ω → (𝐹‘𝑡) ≼ ω) | 
| 50 | 48, 49 | sylbi 217 | . . . . . . . 8
⊢ ((𝐹‘𝑡) ∈ Fin → (𝐹‘𝑡) ≼ ω) | 
| 51 | 47, 50 | syl 17 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ ℕ0) → (𝐹‘𝑡) ≼ ω) | 
| 52 |  | endomtr 9053 | . . . . . . 7
⊢ ((((𝐹‘𝑡) × {𝑡}) ≈ (𝐹‘𝑡) ∧ (𝐹‘𝑡) ≼ ω) → ((𝐹‘𝑡) × {𝑡}) ≼ ω) | 
| 53 | 43, 51, 52 | sylancr 587 | . . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ ℕ0) → ((𝐹‘𝑡) × {𝑡}) ≼ ω) | 
| 54 | 53 | ralrimiva 3145 | . . . . 5
⊢ (𝜑 → ∀𝑡 ∈ ℕ0 ((𝐹‘𝑡) × {𝑡}) ≼ ω) | 
| 55 |  | iunctb 10615 | . . . . 5
⊢
((ℕ0 ≼ ω ∧ ∀𝑡 ∈ ℕ0 ((𝐹‘𝑡) × {𝑡}) ≼ ω) → ∪ 𝑡 ∈ ℕ0 ((𝐹‘𝑡) × {𝑡}) ≼ ω) | 
| 56 | 41, 54, 55 | sylancr 587 | . . . 4
⊢ (𝜑 → ∪ 𝑡 ∈ ℕ0 ((𝐹‘𝑡) × {𝑡}) ≼ ω) | 
| 57 |  | domtr 9048 | . . . 4
⊢ ((𝐺 ≼ ∪ 𝑡 ∈ ℕ0 ((𝐹‘𝑡) × {𝑡}) ∧ ∪
𝑡 ∈
ℕ0 ((𝐹‘𝑡) × {𝑡}) ≼ ω) → 𝐺 ≼ ω) | 
| 58 | 36, 56, 57 | sylancr 587 | . . 3
⊢ (𝜑 → 𝐺 ≼ ω) | 
| 59 | 19 | simp1d 1142 | . . . . . . . . 9
⊢ (𝑥 ∈ 𝐺 → (2nd ‘𝑥) ∈
ℕ0) | 
| 60 |  | peano2nn0 12568 | . . . . . . . . 9
⊢
((2nd ‘𝑥) ∈ ℕ0 →
((2nd ‘𝑥)
+ 1) ∈ ℕ0) | 
| 61 | 59, 60 | syl 17 | . . . . . . . 8
⊢ (𝑥 ∈ 𝐺 → ((2nd ‘𝑥) + 1) ∈
ℕ0) | 
| 62 |  | ffvelcdm 7100 | . . . . . . . 8
⊢ ((𝐹:ℕ0⟶(𝒫 𝑋 ∩ Fin) ∧
((2nd ‘𝑥)
+ 1) ∈ ℕ0) → (𝐹‘((2nd ‘𝑥) + 1)) ∈ (𝒫 𝑋 ∩ Fin)) | 
| 63 | 45, 61, 62 | syl2an 596 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (𝐹‘((2nd ‘𝑥) + 1)) ∈ (𝒫 𝑋 ∩ Fin)) | 
| 64 | 44, 63 | sselid 3980 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (𝐹‘((2nd ‘𝑥) + 1)) ∈
Fin) | 
| 65 |  | iunin2 5070 | . . . . . . . 8
⊢ ∪ 𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) = ((𝐵‘𝑥) ∩ ∪
𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))(𝑡𝐵((2nd ‘𝑥) + 1))) | 
| 66 |  | heibor.8 | . . . . . . . . . . 11
⊢ (𝜑 → ∀𝑛 ∈ ℕ0 𝑋 = ∪ 𝑦 ∈ (𝐹‘𝑛)(𝑦𝐵𝑛)) | 
| 67 |  | oveq1 7439 | . . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝑡 → (𝑦𝐵𝑛) = (𝑡𝐵𝑛)) | 
| 68 | 67 | cbviunv 5039 | . . . . . . . . . . . . . . 15
⊢ ∪ 𝑦 ∈ (𝐹‘𝑛)(𝑦𝐵𝑛) = ∪ 𝑡 ∈ (𝐹‘𝑛)(𝑡𝐵𝑛) | 
| 69 |  | fveq2 6905 | . . . . . . . . . . . . . . . 16
⊢ (𝑛 = ((2nd ‘𝑥) + 1) → (𝐹‘𝑛) = (𝐹‘((2nd ‘𝑥) + 1))) | 
| 70 | 69 | iuneq1d 5018 | . . . . . . . . . . . . . . 15
⊢ (𝑛 = ((2nd ‘𝑥) + 1) → ∪ 𝑡 ∈ (𝐹‘𝑛)(𝑡𝐵𝑛) = ∪ 𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))(𝑡𝐵𝑛)) | 
| 71 | 68, 70 | eqtrid 2788 | . . . . . . . . . . . . . 14
⊢ (𝑛 = ((2nd ‘𝑥) + 1) → ∪ 𝑦 ∈ (𝐹‘𝑛)(𝑦𝐵𝑛) = ∪ 𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))(𝑡𝐵𝑛)) | 
| 72 |  | oveq2 7440 | . . . . . . . . . . . . . . 15
⊢ (𝑛 = ((2nd ‘𝑥) + 1) → (𝑡𝐵𝑛) = (𝑡𝐵((2nd ‘𝑥) + 1))) | 
| 73 | 72 | iuneq2d 5021 | . . . . . . . . . . . . . 14
⊢ (𝑛 = ((2nd ‘𝑥) + 1) → ∪ 𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))(𝑡𝐵𝑛) = ∪ 𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))(𝑡𝐵((2nd ‘𝑥) + 1))) | 
| 74 | 71, 73 | eqtrd 2776 | . . . . . . . . . . . . 13
⊢ (𝑛 = ((2nd ‘𝑥) + 1) → ∪ 𝑦 ∈ (𝐹‘𝑛)(𝑦𝐵𝑛) = ∪ 𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))(𝑡𝐵((2nd ‘𝑥) + 1))) | 
| 75 | 74 | eqeq2d 2747 | . . . . . . . . . . . 12
⊢ (𝑛 = ((2nd ‘𝑥) + 1) → (𝑋 = ∪ 𝑦 ∈ (𝐹‘𝑛)(𝑦𝐵𝑛) ↔ 𝑋 = ∪ 𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))(𝑡𝐵((2nd ‘𝑥) + 1)))) | 
| 76 | 75 | rspccva 3620 | . . . . . . . . . . 11
⊢
((∀𝑛 ∈
ℕ0 𝑋 =
∪ 𝑦 ∈ (𝐹‘𝑛)(𝑦𝐵𝑛) ∧ ((2nd ‘𝑥) + 1) ∈
ℕ0) → 𝑋 = ∪ 𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))(𝑡𝐵((2nd ‘𝑥) + 1))) | 
| 77 | 66, 61, 76 | syl2an 596 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → 𝑋 = ∪ 𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))(𝑡𝐵((2nd ‘𝑥) + 1))) | 
| 78 | 77 | ineq2d 4219 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → ((𝐵‘𝑥) ∩ 𝑋) = ((𝐵‘𝑥) ∩ ∪
𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))(𝑡𝐵((2nd ‘𝑥) + 1)))) | 
| 79 | 9 | fveq2d 6909 | . . . . . . . . . . . . . 14
⊢ (𝑥 ∈ 𝐺 → (𝐵‘𝑥) = (𝐵‘〈(1st ‘𝑥), (2nd ‘𝑥)〉)) | 
| 80 |  | df-ov 7435 | . . . . . . . . . . . . . 14
⊢
((1st ‘𝑥)𝐵(2nd ‘𝑥)) = (𝐵‘〈(1st ‘𝑥), (2nd ‘𝑥)〉) | 
| 81 | 79, 80 | eqtr4di 2794 | . . . . . . . . . . . . 13
⊢ (𝑥 ∈ 𝐺 → (𝐵‘𝑥) = ((1st ‘𝑥)𝐵(2nd ‘𝑥))) | 
| 82 | 81 | adantl 481 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (𝐵‘𝑥) = ((1st ‘𝑥)𝐵(2nd ‘𝑥))) | 
| 83 |  | inss1 4236 | . . . . . . . . . . . . . . . 16
⊢
(𝒫 𝑋 ∩
Fin) ⊆ 𝒫 𝑋 | 
| 84 |  | ffvelcdm 7100 | . . . . . . . . . . . . . . . . 17
⊢ ((𝐹:ℕ0⟶(𝒫 𝑋 ∩ Fin) ∧
(2nd ‘𝑥)
∈ ℕ0) → (𝐹‘(2nd ‘𝑥)) ∈ (𝒫 𝑋 ∩ Fin)) | 
| 85 | 45, 59, 84 | syl2an 596 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (𝐹‘(2nd ‘𝑥)) ∈ (𝒫 𝑋 ∩ Fin)) | 
| 86 | 83, 85 | sselid 3980 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (𝐹‘(2nd ‘𝑥)) ∈ 𝒫 𝑋) | 
| 87 | 86 | elpwid 4608 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (𝐹‘(2nd ‘𝑥)) ⊆ 𝑋) | 
| 88 | 19 | simp2d 1143 | . . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ 𝐺 → (1st ‘𝑥) ∈ (𝐹‘(2nd ‘𝑥))) | 
| 89 | 88 | adantl 481 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (1st ‘𝑥) ∈ (𝐹‘(2nd ‘𝑥))) | 
| 90 | 87, 89 | sseldd 3983 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (1st ‘𝑥) ∈ 𝑋) | 
| 91 | 59 | adantl 481 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (2nd ‘𝑥) ∈
ℕ0) | 
| 92 |  | oveq1 7439 | . . . . . . . . . . . . . 14
⊢ (𝑧 = (1st ‘𝑥) → (𝑧(ball‘𝐷)(1 / (2↑𝑚))) = ((1st ‘𝑥)(ball‘𝐷)(1 / (2↑𝑚)))) | 
| 93 |  | oveq2 7440 | . . . . . . . . . . . . . . . 16
⊢ (𝑚 = (2nd ‘𝑥) → (2↑𝑚) = (2↑(2nd
‘𝑥))) | 
| 94 | 93 | oveq2d 7448 | . . . . . . . . . . . . . . 15
⊢ (𝑚 = (2nd ‘𝑥) → (1 / (2↑𝑚)) = (1 /
(2↑(2nd ‘𝑥)))) | 
| 95 | 94 | oveq2d 7448 | . . . . . . . . . . . . . 14
⊢ (𝑚 = (2nd ‘𝑥) → ((1st
‘𝑥)(ball‘𝐷)(1 / (2↑𝑚))) = ((1st ‘𝑥)(ball‘𝐷)(1 / (2↑(2nd ‘𝑥))))) | 
| 96 |  | heibor.5 | . . . . . . . . . . . . . 14
⊢ 𝐵 = (𝑧 ∈ 𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚)))) | 
| 97 |  | ovex 7465 | . . . . . . . . . . . . . 14
⊢
((1st ‘𝑥)(ball‘𝐷)(1 / (2↑(2nd ‘𝑥)))) ∈ V | 
| 98 | 92, 95, 96, 97 | ovmpo 7594 | . . . . . . . . . . . . 13
⊢
(((1st ‘𝑥) ∈ 𝑋 ∧ (2nd ‘𝑥) ∈ ℕ0)
→ ((1st ‘𝑥)𝐵(2nd ‘𝑥)) = ((1st ‘𝑥)(ball‘𝐷)(1 / (2↑(2nd ‘𝑥))))) | 
| 99 | 90, 91, 98 | syl2anc 584 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → ((1st ‘𝑥)𝐵(2nd ‘𝑥)) = ((1st ‘𝑥)(ball‘𝐷)(1 / (2↑(2nd ‘𝑥))))) | 
| 100 | 82, 99 | eqtrd 2776 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (𝐵‘𝑥) = ((1st ‘𝑥)(ball‘𝐷)(1 / (2↑(2nd ‘𝑥))))) | 
| 101 |  | heibor.6 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐷 ∈ (CMet‘𝑋)) | 
| 102 |  | cmetmet 25321 | . . . . . . . . . . . . . . 15
⊢ (𝐷 ∈ (CMet‘𝑋) → 𝐷 ∈ (Met‘𝑋)) | 
| 103 | 101, 102 | syl 17 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋)) | 
| 104 |  | metxmet 24345 | . . . . . . . . . . . . . 14
⊢ (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ (∞Met‘𝑋)) | 
| 105 | 103, 104 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋)) | 
| 106 | 105 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → 𝐷 ∈ (∞Met‘𝑋)) | 
| 107 |  | 2nn 12340 | . . . . . . . . . . . . . . . 16
⊢ 2 ∈
ℕ | 
| 108 |  | nnexpcl 14116 | . . . . . . . . . . . . . . . 16
⊢ ((2
∈ ℕ ∧ (2nd ‘𝑥) ∈ ℕ0) →
(2↑(2nd ‘𝑥)) ∈ ℕ) | 
| 109 | 107, 91, 108 | sylancr 587 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (2↑(2nd
‘𝑥)) ∈
ℕ) | 
| 110 | 109 | nnrpd 13076 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (2↑(2nd
‘𝑥)) ∈
ℝ+) | 
| 111 | 110 | rpreccld 13088 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (1 / (2↑(2nd
‘𝑥))) ∈
ℝ+) | 
| 112 | 111 | rpxrd 13079 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (1 / (2↑(2nd
‘𝑥))) ∈
ℝ*) | 
| 113 |  | blssm 24429 | . . . . . . . . . . . 12
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (1st
‘𝑥) ∈ 𝑋 ∧ (1 /
(2↑(2nd ‘𝑥))) ∈ ℝ*) →
((1st ‘𝑥)(ball‘𝐷)(1 / (2↑(2nd ‘𝑥)))) ⊆ 𝑋) | 
| 114 | 106, 90, 112, 113 | syl3anc 1372 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → ((1st ‘𝑥)(ball‘𝐷)(1 / (2↑(2nd ‘𝑥)))) ⊆ 𝑋) | 
| 115 | 100, 114 | eqsstrd 4017 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (𝐵‘𝑥) ⊆ 𝑋) | 
| 116 |  | dfss2 3968 | . . . . . . . . . 10
⊢ ((𝐵‘𝑥) ⊆ 𝑋 ↔ ((𝐵‘𝑥) ∩ 𝑋) = (𝐵‘𝑥)) | 
| 117 | 115, 116 | sylib 218 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → ((𝐵‘𝑥) ∩ 𝑋) = (𝐵‘𝑥)) | 
| 118 | 78, 117 | eqtr3d 2778 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → ((𝐵‘𝑥) ∩ ∪
𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))(𝑡𝐵((2nd ‘𝑥) + 1))) = (𝐵‘𝑥)) | 
| 119 | 65, 118 | eqtrid 2788 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → ∪
𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) = (𝐵‘𝑥)) | 
| 120 |  | eqimss2 4042 | . . . . . . 7
⊢ (∪ 𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) = (𝐵‘𝑥) → (𝐵‘𝑥) ⊆ ∪
𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1)))) | 
| 121 | 119, 120 | syl 17 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (𝐵‘𝑥) ⊆ ∪
𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1)))) | 
| 122 | 19 | simp3d 1144 | . . . . . . . 8
⊢ (𝑥 ∈ 𝐺 → ((1st ‘𝑥)𝐵(2nd ‘𝑥)) ∈ 𝐾) | 
| 123 | 81, 122 | eqeltrd 2840 | . . . . . . 7
⊢ (𝑥 ∈ 𝐺 → (𝐵‘𝑥) ∈ 𝐾) | 
| 124 | 123 | adantl 481 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (𝐵‘𝑥) ∈ 𝐾) | 
| 125 |  | fvex 6918 | . . . . . . . 8
⊢ (𝐵‘𝑥) ∈ V | 
| 126 | 125 | inex1 5316 | . . . . . . 7
⊢ ((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ∈ V | 
| 127 | 13, 14, 126 | heiborlem1 37819 | . . . . . 6
⊢ (((𝐹‘((2nd
‘𝑥) + 1)) ∈ Fin
∧ (𝐵‘𝑥) ⊆ ∪ 𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ∧ (𝐵‘𝑥) ∈ 𝐾) → ∃𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾) | 
| 128 | 64, 121, 124, 127 | syl3anc 1372 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → ∃𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾) | 
| 129 | 83, 63 | sselid 3980 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (𝐹‘((2nd ‘𝑥) + 1)) ∈ 𝒫 𝑋) | 
| 130 | 129 | elpwid 4608 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (𝐹‘((2nd ‘𝑥) + 1)) ⊆ 𝑋) | 
| 131 | 13 | mopnuni 24452 | . . . . . . . . . . . . 13
⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝑋 = ∪ 𝐽) | 
| 132 | 105, 131 | syl 17 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑋 = ∪ 𝐽) | 
| 133 | 132 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → 𝑋 = ∪ 𝐽) | 
| 134 | 130, 133 | sseqtrd 4019 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (𝐹‘((2nd ‘𝑥) + 1)) ⊆ ∪ 𝐽) | 
| 135 | 134 | sselda 3982 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐺) ∧ 𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))) → 𝑡 ∈ ∪ 𝐽) | 
| 136 | 135 | adantrr 717 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐺) ∧ (𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1)) ∧ ((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾)) → 𝑡 ∈ ∪ 𝐽) | 
| 137 | 61 | adantl 481 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → ((2nd ‘𝑥) + 1) ∈
ℕ0) | 
| 138 |  | id 22 | . . . . . . . . . 10
⊢ (𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1)) → 𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))) | 
| 139 |  | snfi 9084 | . . . . . . . . . . . 12
⊢ {(𝑡𝐵((2nd ‘𝑥) + 1))} ∈ Fin | 
| 140 |  | inss2 4237 | . . . . . . . . . . . . 13
⊢ ((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ⊆ (𝑡𝐵((2nd ‘𝑥) + 1)) | 
| 141 |  | ovex 7465 | . . . . . . . . . . . . . . 15
⊢ (𝑡𝐵((2nd ‘𝑥) + 1)) ∈ V | 
| 142 | 141 | unisn 4925 | . . . . . . . . . . . . . 14
⊢ ∪ {(𝑡𝐵((2nd ‘𝑥) + 1))} = (𝑡𝐵((2nd ‘𝑥) + 1)) | 
| 143 |  | uniiun 5057 | . . . . . . . . . . . . . 14
⊢ ∪ {(𝑡𝐵((2nd ‘𝑥) + 1))} = ∪ 𝑔 ∈ {(𝑡𝐵((2nd ‘𝑥) + 1))}𝑔 | 
| 144 | 142, 143 | eqtr3i 2766 | . . . . . . . . . . . . 13
⊢ (𝑡𝐵((2nd ‘𝑥) + 1)) = ∪
𝑔 ∈ {(𝑡𝐵((2nd ‘𝑥) + 1))}𝑔 | 
| 145 | 140, 144 | sseqtri 4031 | . . . . . . . . . . . 12
⊢ ((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ⊆ ∪ 𝑔 ∈ {(𝑡𝐵((2nd ‘𝑥) + 1))}𝑔 | 
| 146 |  | vex 3483 | . . . . . . . . . . . . 13
⊢ 𝑔 ∈ V | 
| 147 | 13, 14, 146 | heiborlem1 37819 | . . . . . . . . . . . 12
⊢ (({(𝑡𝐵((2nd ‘𝑥) + 1))} ∈ Fin ∧ ((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ⊆ ∪ 𝑔 ∈ {(𝑡𝐵((2nd ‘𝑥) + 1))}𝑔 ∧ ((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾) → ∃𝑔 ∈ {(𝑡𝐵((2nd ‘𝑥) + 1))}𝑔 ∈ 𝐾) | 
| 148 | 139, 145,
147 | mp3an12 1452 | . . . . . . . . . . 11
⊢ (((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾 → ∃𝑔 ∈ {(𝑡𝐵((2nd ‘𝑥) + 1))}𝑔 ∈ 𝐾) | 
| 149 |  | eleq1 2828 | . . . . . . . . . . . 12
⊢ (𝑔 = (𝑡𝐵((2nd ‘𝑥) + 1)) → (𝑔 ∈ 𝐾 ↔ (𝑡𝐵((2nd ‘𝑥) + 1)) ∈ 𝐾)) | 
| 150 | 141, 149 | rexsn 4681 | . . . . . . . . . . 11
⊢
(∃𝑔 ∈
{(𝑡𝐵((2nd ‘𝑥) + 1))}𝑔 ∈ 𝐾 ↔ (𝑡𝐵((2nd ‘𝑥) + 1)) ∈ 𝐾) | 
| 151 | 148, 150 | sylib 218 | . . . . . . . . . 10
⊢ (((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾 → (𝑡𝐵((2nd ‘𝑥) + 1)) ∈ 𝐾) | 
| 152 |  | ovex 7465 | . . . . . . . . . . . 12
⊢
((2nd ‘𝑥) + 1) ∈ V | 
| 153 | 13, 14, 6, 42, 152 | heiborlem2 37820 | . . . . . . . . . . 11
⊢ (𝑡𝐺((2nd ‘𝑥) + 1) ↔ (((2nd ‘𝑥) + 1) ∈
ℕ0 ∧ 𝑡
∈ (𝐹‘((2nd ‘𝑥) + 1)) ∧ (𝑡𝐵((2nd ‘𝑥) + 1)) ∈ 𝐾)) | 
| 154 | 153 | biimpri 228 | . . . . . . . . . 10
⊢
((((2nd ‘𝑥) + 1) ∈ ℕ0 ∧ 𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1)) ∧ (𝑡𝐵((2nd ‘𝑥) + 1)) ∈ 𝐾) → 𝑡𝐺((2nd ‘𝑥) + 1)) | 
| 155 | 137, 138,
151, 154 | syl3an 1160 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐺) ∧ 𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1)) ∧ ((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾) → 𝑡𝐺((2nd ‘𝑥) + 1)) | 
| 156 | 155 | 3expb 1120 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐺) ∧ (𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1)) ∧ ((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾)) → 𝑡𝐺((2nd ‘𝑥) + 1)) | 
| 157 |  | simprr 772 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐺) ∧ (𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1)) ∧ ((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾)) → ((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾) | 
| 158 | 136, 156,
157 | jca32 515 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐺) ∧ (𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1)) ∧ ((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾)) → (𝑡 ∈ ∪ 𝐽 ∧ (𝑡𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾))) | 
| 159 | 158 | ex 412 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → ((𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1)) ∧ ((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾) → (𝑡 ∈ ∪ 𝐽 ∧ (𝑡𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾)))) | 
| 160 | 159 | reximdv2 3163 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (∃𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾 → ∃𝑡 ∈ ∪ 𝐽(𝑡𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾))) | 
| 161 | 128, 160 | mpd 15 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → ∃𝑡 ∈ ∪ 𝐽(𝑡𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾)) | 
| 162 | 161 | ralrimiva 3145 | . . 3
⊢ (𝜑 → ∀𝑥 ∈ 𝐺 ∃𝑡 ∈ ∪ 𝐽(𝑡𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾)) | 
| 163 | 13 | fvexi 6919 | . . . . 5
⊢ 𝐽 ∈ V | 
| 164 | 163 | uniex 7762 | . . . 4
⊢ ∪ 𝐽
∈ V | 
| 165 |  | breq1 5145 | . . . . 5
⊢ (𝑡 = (𝑔‘𝑥) → (𝑡𝐺((2nd ‘𝑥) + 1) ↔ (𝑔‘𝑥)𝐺((2nd ‘𝑥) + 1))) | 
| 166 |  | oveq1 7439 | . . . . . . 7
⊢ (𝑡 = (𝑔‘𝑥) → (𝑡𝐵((2nd ‘𝑥) + 1)) = ((𝑔‘𝑥)𝐵((2nd ‘𝑥) + 1))) | 
| 167 | 166 | ineq2d 4219 | . . . . . 6
⊢ (𝑡 = (𝑔‘𝑥) → ((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) = ((𝐵‘𝑥) ∩ ((𝑔‘𝑥)𝐵((2nd ‘𝑥) + 1)))) | 
| 168 | 167 | eleq1d 2825 | . . . . 5
⊢ (𝑡 = (𝑔‘𝑥) → (((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾 ↔ ((𝐵‘𝑥) ∩ ((𝑔‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾)) | 
| 169 | 165, 168 | anbi12d 632 | . . . 4
⊢ (𝑡 = (𝑔‘𝑥) → ((𝑡𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾) ↔ ((𝑔‘𝑥)𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ ((𝑔‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾))) | 
| 170 | 164, 169 | axcc4dom 10482 | . . 3
⊢ ((𝐺 ≼ ω ∧
∀𝑥 ∈ 𝐺 ∃𝑡 ∈ ∪ 𝐽(𝑡𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾)) → ∃𝑔(𝑔:𝐺⟶∪ 𝐽 ∧ ∀𝑥 ∈ 𝐺 ((𝑔‘𝑥)𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ ((𝑔‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾))) | 
| 171 | 58, 162, 170 | syl2anc 584 | . 2
⊢ (𝜑 → ∃𝑔(𝑔:𝐺⟶∪ 𝐽 ∧ ∀𝑥 ∈ 𝐺 ((𝑔‘𝑥)𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ ((𝑔‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾))) | 
| 172 |  | exsimpr 1868 | . 2
⊢
(∃𝑔(𝑔:𝐺⟶∪ 𝐽 ∧ ∀𝑥 ∈ 𝐺 ((𝑔‘𝑥)𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ ((𝑔‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾)) → ∃𝑔∀𝑥 ∈ 𝐺 ((𝑔‘𝑥)𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ ((𝑔‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾)) | 
| 173 | 171, 172 | syl 17 | 1
⊢ (𝜑 → ∃𝑔∀𝑥 ∈ 𝐺 ((𝑔‘𝑥)𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ ((𝑔‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾)) |