| Step | Hyp | Ref
| Expression |
| 1 | | om1val.o |
. 2
⊢ 𝑂 = (𝐽 Ω1 𝑌) |
| 2 | | df-om1 25039 |
. . . 4
⊢
Ω1 = (𝑗
∈ Top, 𝑦 ∈ ∪ 𝑗
↦ {〈(Base‘ndx), {𝑓 ∈ (II Cn 𝑗) ∣ ((𝑓‘0) = 𝑦 ∧ (𝑓‘1) = 𝑦)}〉, 〈(+g‘ndx),
(*𝑝‘𝑗)〉, 〈(TopSet‘ndx), (𝑗 ↑ko
II)〉}) |
| 3 | 2 | a1i 11 |
. . 3
⊢ (𝜑 → Ω1 =
(𝑗 ∈ Top, 𝑦 ∈ ∪ 𝑗
↦ {〈(Base‘ndx), {𝑓 ∈ (II Cn 𝑗) ∣ ((𝑓‘0) = 𝑦 ∧ (𝑓‘1) = 𝑦)}〉, 〈(+g‘ndx),
(*𝑝‘𝑗)〉, 〈(TopSet‘ndx), (𝑗 ↑ko
II)〉})) |
| 4 | | simprl 771 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑗 = 𝐽 ∧ 𝑦 = 𝑌)) → 𝑗 = 𝐽) |
| 5 | 4 | oveq2d 7447 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑗 = 𝐽 ∧ 𝑦 = 𝑌)) → (II Cn 𝑗) = (II Cn 𝐽)) |
| 6 | | simprr 773 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑗 = 𝐽 ∧ 𝑦 = 𝑌)) → 𝑦 = 𝑌) |
| 7 | 6 | eqeq2d 2748 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑗 = 𝐽 ∧ 𝑦 = 𝑌)) → ((𝑓‘0) = 𝑦 ↔ (𝑓‘0) = 𝑌)) |
| 8 | 6 | eqeq2d 2748 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑗 = 𝐽 ∧ 𝑦 = 𝑌)) → ((𝑓‘1) = 𝑦 ↔ (𝑓‘1) = 𝑌)) |
| 9 | 7, 8 | anbi12d 632 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑗 = 𝐽 ∧ 𝑦 = 𝑌)) → (((𝑓‘0) = 𝑦 ∧ (𝑓‘1) = 𝑦) ↔ ((𝑓‘0) = 𝑌 ∧ (𝑓‘1) = 𝑌))) |
| 10 | 5, 9 | rabeqbidv 3455 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑗 = 𝐽 ∧ 𝑦 = 𝑌)) → {𝑓 ∈ (II Cn 𝑗) ∣ ((𝑓‘0) = 𝑦 ∧ (𝑓‘1) = 𝑦)} = {𝑓 ∈ (II Cn 𝐽) ∣ ((𝑓‘0) = 𝑌 ∧ (𝑓‘1) = 𝑌)}) |
| 11 | | om1val.b |
. . . . . . 7
⊢ (𝜑 → 𝐵 = {𝑓 ∈ (II Cn 𝐽) ∣ ((𝑓‘0) = 𝑌 ∧ (𝑓‘1) = 𝑌)}) |
| 12 | 11 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑗 = 𝐽 ∧ 𝑦 = 𝑌)) → 𝐵 = {𝑓 ∈ (II Cn 𝐽) ∣ ((𝑓‘0) = 𝑌 ∧ (𝑓‘1) = 𝑌)}) |
| 13 | 10, 12 | eqtr4d 2780 |
. . . . 5
⊢ ((𝜑 ∧ (𝑗 = 𝐽 ∧ 𝑦 = 𝑌)) → {𝑓 ∈ (II Cn 𝑗) ∣ ((𝑓‘0) = 𝑦 ∧ (𝑓‘1) = 𝑦)} = 𝐵) |
| 14 | 13 | opeq2d 4880 |
. . . 4
⊢ ((𝜑 ∧ (𝑗 = 𝐽 ∧ 𝑦 = 𝑌)) → 〈(Base‘ndx), {𝑓 ∈ (II Cn 𝑗) ∣ ((𝑓‘0) = 𝑦 ∧ (𝑓‘1) = 𝑦)}〉 = 〈(Base‘ndx), 𝐵〉) |
| 15 | 4 | fveq2d 6910 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑗 = 𝐽 ∧ 𝑦 = 𝑌)) → (*𝑝‘𝑗) =
(*𝑝‘𝐽)) |
| 16 | | om1val.p |
. . . . . . 7
⊢ (𝜑 → + =
(*𝑝‘𝐽)) |
| 17 | 16 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑗 = 𝐽 ∧ 𝑦 = 𝑌)) → + =
(*𝑝‘𝐽)) |
| 18 | 15, 17 | eqtr4d 2780 |
. . . . 5
⊢ ((𝜑 ∧ (𝑗 = 𝐽 ∧ 𝑦 = 𝑌)) → (*𝑝‘𝑗) = + ) |
| 19 | 18 | opeq2d 4880 |
. . . 4
⊢ ((𝜑 ∧ (𝑗 = 𝐽 ∧ 𝑦 = 𝑌)) → 〈(+g‘ndx),
(*𝑝‘𝑗)〉 = 〈(+g‘ndx),
+
〉) |
| 20 | 4 | oveq1d 7446 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑗 = 𝐽 ∧ 𝑦 = 𝑌)) → (𝑗 ↑ko II) = (𝐽 ↑ko II)) |
| 21 | | om1val.k |
. . . . . . 7
⊢ (𝜑 → 𝐾 = (𝐽 ↑ko II)) |
| 22 | 21 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑗 = 𝐽 ∧ 𝑦 = 𝑌)) → 𝐾 = (𝐽 ↑ko II)) |
| 23 | 20, 22 | eqtr4d 2780 |
. . . . 5
⊢ ((𝜑 ∧ (𝑗 = 𝐽 ∧ 𝑦 = 𝑌)) → (𝑗 ↑ko II) = 𝐾) |
| 24 | 23 | opeq2d 4880 |
. . . 4
⊢ ((𝜑 ∧ (𝑗 = 𝐽 ∧ 𝑦 = 𝑌)) → 〈(TopSet‘ndx), (𝑗 ↑ko II)〉 =
〈(TopSet‘ndx), 𝐾〉) |
| 25 | 14, 19, 24 | tpeq123d 4748 |
. . 3
⊢ ((𝜑 ∧ (𝑗 = 𝐽 ∧ 𝑦 = 𝑌)) → {〈(Base‘ndx), {𝑓 ∈ (II Cn 𝑗) ∣ ((𝑓‘0) = 𝑦 ∧ (𝑓‘1) = 𝑦)}〉, 〈(+g‘ndx),
(*𝑝‘𝑗)〉, 〈(TopSet‘ndx), (𝑗 ↑ko II)〉}
= {〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx),
+ 〉,
〈(TopSet‘ndx), 𝐾〉}) |
| 26 | | unieq 4918 |
. . . . 5
⊢ (𝑗 = 𝐽 → ∪ 𝑗 = ∪
𝐽) |
| 27 | 26 | adantl 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 = 𝐽) → ∪ 𝑗 = ∪
𝐽) |
| 28 | | om1val.j |
. . . . . 6
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) |
| 29 | | toponuni 22920 |
. . . . . 6
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = ∪ 𝐽) |
| 30 | 28, 29 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑋 = ∪ 𝐽) |
| 31 | 30 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 = 𝐽) → 𝑋 = ∪ 𝐽) |
| 32 | 27, 31 | eqtr4d 2780 |
. . 3
⊢ ((𝜑 ∧ 𝑗 = 𝐽) → ∪ 𝑗 = 𝑋) |
| 33 | | topontop 22919 |
. . . 4
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top) |
| 34 | 28, 33 | syl 17 |
. . 3
⊢ (𝜑 → 𝐽 ∈ Top) |
| 35 | | om1val.y |
. . 3
⊢ (𝜑 → 𝑌 ∈ 𝑋) |
| 36 | | tpex 7766 |
. . . 4
⊢
{〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx),
+ 〉,
〈(TopSet‘ndx), 𝐾〉} ∈ V |
| 37 | 36 | a1i 11 |
. . 3
⊢ (𝜑 → {〈(Base‘ndx),
𝐵〉,
〈(+g‘ndx), + 〉,
〈(TopSet‘ndx), 𝐾〉} ∈ V) |
| 38 | 3, 25, 32, 34, 35, 37 | ovmpodx 7584 |
. 2
⊢ (𝜑 → (𝐽 Ω1 𝑌) = {〈(Base‘ndx), 𝐵〉,
〈(+g‘ndx), + 〉,
〈(TopSet‘ndx), 𝐾〉}) |
| 39 | 1, 38 | eqtrid 2789 |
1
⊢ (𝜑 → 𝑂 = {〈(Base‘ndx), 𝐵〉,
〈(+g‘ndx), + 〉,
〈(TopSet‘ndx), 𝐾〉}) |