Step | Hyp | Ref
| Expression |
1 | | pi1addval.3 |
. . 3
⊢ (𝜑 → 𝑀 ∈ ∪ 𝐵) |
2 | | pi1addval.4 |
. . 3
⊢ (𝜑 → 𝑁 ∈ ∪ 𝐵) |
3 | | eqidd 2611 |
. . . . . 6
⊢ (𝜑 → ((𝐽 Ω1 𝑌) /s (
≃ph‘𝐽)) = ((𝐽 Ω1 𝑌) /s (
≃ph‘𝐽))) |
4 | | eqidd 2611 |
. . . . . 6
⊢ (𝜑 → (Base‘(𝐽 Ω1 𝑌)) = (Base‘(𝐽 Ω1 𝑌))) |
5 | | fvex 6113 |
. . . . . . 7
⊢ (
≃ph‘𝐽) ∈ V |
6 | 5 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (
≃ph‘𝐽) ∈ V) |
7 | | ovex 6577 |
. . . . . . 7
⊢ (𝐽 Ω1 𝑌) ∈ V |
8 | 7 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (𝐽 Ω1 𝑌) ∈ V) |
9 | | elpi1.g |
. . . . . . . 8
⊢ 𝐺 = (𝐽 π1 𝑌) |
10 | | elpi1.1 |
. . . . . . . 8
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) |
11 | | elpi1.2 |
. . . . . . . 8
⊢ (𝜑 → 𝑌 ∈ 𝑋) |
12 | | eqid 2610 |
. . . . . . . 8
⊢ (𝐽 Ω1 𝑌) = (𝐽 Ω1 𝑌) |
13 | | elpi1.b |
. . . . . . . . 9
⊢ 𝐵 = (Base‘𝐺) |
14 | 13 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 = (Base‘𝐺)) |
15 | 9, 10, 11, 12, 14, 4 | pi1blem 22647 |
. . . . . . 7
⊢ (𝜑 → (((
≃ph‘𝐽) “ (Base‘(𝐽 Ω1 𝑌))) ⊆ (Base‘(𝐽 Ω1 𝑌)) ∧ (Base‘(𝐽 Ω1 𝑌)) ⊆ (II Cn 𝐽))) |
16 | 15 | simpld 474 |
. . . . . 6
⊢ (𝜑 → ((
≃ph‘𝐽) “ (Base‘(𝐽 Ω1 𝑌))) ⊆ (Base‘(𝐽 Ω1 𝑌))) |
17 | 3, 4, 6, 8, 16 | qusin 16027 |
. . . . 5
⊢ (𝜑 → ((𝐽 Ω1 𝑌) /s (
≃ph‘𝐽)) = ((𝐽 Ω1 𝑌) /s ((
≃ph‘𝐽) ∩ ((Base‘(𝐽 Ω1 𝑌)) × (Base‘(𝐽 Ω1 𝑌)))))) |
18 | 9, 10, 11, 12 | pi1val 22645 |
. . . . 5
⊢ (𝜑 → 𝐺 = ((𝐽 Ω1 𝑌) /s (
≃ph‘𝐽))) |
19 | 9, 10, 11, 12, 14, 4 | pi1buni 22648 |
. . . . . . . 8
⊢ (𝜑 → ∪ 𝐵 =
(Base‘(𝐽
Ω1 𝑌))) |
20 | 19 | sqxpeqd 5065 |
. . . . . . 7
⊢ (𝜑 → (∪ 𝐵
× ∪ 𝐵) = ((Base‘(𝐽 Ω1 𝑌)) × (Base‘(𝐽 Ω1 𝑌)))) |
21 | 20 | ineq2d 3776 |
. . . . . 6
⊢ (𝜑 → ((
≃ph‘𝐽) ∩ (∪ 𝐵 × ∪ 𝐵))
= (( ≃ph‘𝐽) ∩ ((Base‘(𝐽 Ω1 𝑌)) × (Base‘(𝐽 Ω1 𝑌))))) |
22 | 21 | oveq2d 6565 |
. . . . 5
⊢ (𝜑 → ((𝐽 Ω1 𝑌) /s ((
≃ph‘𝐽) ∩ (∪ 𝐵 × ∪ 𝐵)))
= ((𝐽 Ω1
𝑌) /s ((
≃ph‘𝐽) ∩ ((Base‘(𝐽 Ω1 𝑌)) × (Base‘(𝐽 Ω1 𝑌)))))) |
23 | 17, 18, 22 | 3eqtr4d 2654 |
. . . 4
⊢ (𝜑 → 𝐺 = ((𝐽 Ω1 𝑌) /s ((
≃ph‘𝐽) ∩ (∪ 𝐵 × ∪ 𝐵)))) |
24 | | phtpcer 22602 |
. . . . . 6
⊢ (
≃ph‘𝐽) Er (II Cn 𝐽) |
25 | 24 | a1i 11 |
. . . . 5
⊢ (𝜑 → (
≃ph‘𝐽) Er (II Cn 𝐽)) |
26 | 15 | simprd 478 |
. . . . . 6
⊢ (𝜑 → (Base‘(𝐽 Ω1 𝑌)) ⊆ (II Cn 𝐽)) |
27 | 19, 26 | eqsstrd 3602 |
. . . . 5
⊢ (𝜑 → ∪ 𝐵
⊆ (II Cn 𝐽)) |
28 | 25, 27 | erinxp 7708 |
. . . 4
⊢ (𝜑 → ((
≃ph‘𝐽) ∩ (∪ 𝐵 × ∪ 𝐵))
Er ∪ 𝐵) |
29 | | eqid 2610 |
. . . . 5
⊢ ((
≃ph‘𝐽) ∩ (∪ 𝐵 × ∪ 𝐵))
= (( ≃ph‘𝐽) ∩ (∪ 𝐵 × ∪ 𝐵)) |
30 | | eqid 2610 |
. . . . 5
⊢
(+g‘(𝐽 Ω1 𝑌)) = (+g‘(𝐽 Ω1 𝑌)) |
31 | 9, 10, 11, 14, 29, 12, 30 | pi1cpbl 22652 |
. . . 4
⊢ (𝜑 → ((𝑎(( ≃ph‘𝐽) ∩ (∪ 𝐵
× ∪ 𝐵))𝑐 ∧ 𝑏(( ≃ph‘𝐽) ∩ (∪ 𝐵
× ∪ 𝐵))𝑑) → (𝑎(+g‘(𝐽 Ω1 𝑌))𝑏)(( ≃ph‘𝐽) ∩ (∪ 𝐵
× ∪ 𝐵))(𝑐(+g‘(𝐽 Ω1 𝑌))𝑑))) |
32 | 12, 10, 11 | om1plusg 22642 |
. . . . . . 7
⊢ (𝜑 →
(*𝑝‘𝐽) = (+g‘(𝐽 Ω1 𝑌))) |
33 | 32 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑐 ∈ ∪ 𝐵 ∧ 𝑑 ∈ ∪ 𝐵)) →
(*𝑝‘𝐽) = (+g‘(𝐽 Ω1 𝑌))) |
34 | 33 | oveqd 6566 |
. . . . 5
⊢ ((𝜑 ∧ (𝑐 ∈ ∪ 𝐵 ∧ 𝑑 ∈ ∪ 𝐵)) → (𝑐(*𝑝‘𝐽)𝑑) = (𝑐(+g‘(𝐽 Ω1 𝑌))𝑑)) |
35 | 10 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑐 ∈ ∪ 𝐵 ∧ 𝑑 ∈ ∪ 𝐵)) → 𝐽 ∈ (TopOn‘𝑋)) |
36 | 11 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑐 ∈ ∪ 𝐵 ∧ 𝑑 ∈ ∪ 𝐵)) → 𝑌 ∈ 𝑋) |
37 | 19 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑐 ∈ ∪ 𝐵 ∧ 𝑑 ∈ ∪ 𝐵)) → ∪ 𝐵 =
(Base‘(𝐽
Ω1 𝑌))) |
38 | | simprl 790 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑐 ∈ ∪ 𝐵 ∧ 𝑑 ∈ ∪ 𝐵)) → 𝑐 ∈ ∪ 𝐵) |
39 | | simprr 792 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑐 ∈ ∪ 𝐵 ∧ 𝑑 ∈ ∪ 𝐵)) → 𝑑 ∈ ∪ 𝐵) |
40 | 12, 35, 36, 37, 38, 39 | om1addcl 22641 |
. . . . 5
⊢ ((𝜑 ∧ (𝑐 ∈ ∪ 𝐵 ∧ 𝑑 ∈ ∪ 𝐵)) → (𝑐(*𝑝‘𝐽)𝑑) ∈ ∪ 𝐵) |
41 | 34, 40 | eqeltrrd 2689 |
. . . 4
⊢ ((𝜑 ∧ (𝑐 ∈ ∪ 𝐵 ∧ 𝑑 ∈ ∪ 𝐵)) → (𝑐(+g‘(𝐽 Ω1 𝑌))𝑑) ∈ ∪ 𝐵) |
42 | | pi1addf.p |
. . . 4
⊢ + =
(+g‘𝐺) |
43 | 23, 19, 28, 8, 31, 41, 30, 42 | qusaddval 16036 |
. . 3
⊢ ((𝜑 ∧ 𝑀 ∈ ∪ 𝐵 ∧ 𝑁 ∈ ∪ 𝐵) → ([𝑀](( ≃ph‘𝐽) ∩ (∪ 𝐵
× ∪ 𝐵)) + [𝑁](( ≃ph‘𝐽) ∩ (∪ 𝐵
× ∪ 𝐵))) = [(𝑀(+g‘(𝐽 Ω1 𝑌))𝑁)](( ≃ph‘𝐽) ∩ (∪ 𝐵
× ∪ 𝐵))) |
44 | 1, 2, 43 | mpd3an23 1418 |
. 2
⊢ (𝜑 → ([𝑀](( ≃ph‘𝐽) ∩ (∪ 𝐵
× ∪ 𝐵)) + [𝑁](( ≃ph‘𝐽) ∩ (∪ 𝐵
× ∪ 𝐵))) = [(𝑀(+g‘(𝐽 Ω1 𝑌))𝑁)](( ≃ph‘𝐽) ∩ (∪ 𝐵
× ∪ 𝐵))) |
45 | 19 | imaeq2d 5385 |
. . . . 5
⊢ (𝜑 → ((
≃ph‘𝐽) “ ∪ 𝐵) = ((
≃ph‘𝐽) “ (Base‘(𝐽 Ω1 𝑌)))) |
46 | 16, 45, 19 | 3sstr4d 3611 |
. . . 4
⊢ (𝜑 → ((
≃ph‘𝐽) “ ∪ 𝐵) ⊆ ∪ 𝐵) |
47 | | ecinxp 7709 |
. . . 4
⊢ ((((
≃ph‘𝐽) “ ∪ 𝐵) ⊆ ∪ 𝐵
∧ 𝑀 ∈ ∪ 𝐵)
→ [𝑀](
≃ph‘𝐽) = [𝑀](( ≃ph‘𝐽) ∩ (∪ 𝐵
× ∪ 𝐵))) |
48 | 46, 1, 47 | syl2anc 691 |
. . 3
⊢ (𝜑 → [𝑀]( ≃ph‘𝐽) = [𝑀](( ≃ph‘𝐽) ∩ (∪ 𝐵
× ∪ 𝐵))) |
49 | | ecinxp 7709 |
. . . 4
⊢ ((((
≃ph‘𝐽) “ ∪ 𝐵) ⊆ ∪ 𝐵
∧ 𝑁 ∈ ∪ 𝐵)
→ [𝑁](
≃ph‘𝐽) = [𝑁](( ≃ph‘𝐽) ∩ (∪ 𝐵
× ∪ 𝐵))) |
50 | 46, 2, 49 | syl2anc 691 |
. . 3
⊢ (𝜑 → [𝑁]( ≃ph‘𝐽) = [𝑁](( ≃ph‘𝐽) ∩ (∪ 𝐵
× ∪ 𝐵))) |
51 | 48, 50 | oveq12d 6567 |
. 2
⊢ (𝜑 → ([𝑀]( ≃ph‘𝐽) + [𝑁]( ≃ph‘𝐽)) = ([𝑀](( ≃ph‘𝐽) ∩ (∪ 𝐵
× ∪ 𝐵)) + [𝑁](( ≃ph‘𝐽) ∩ (∪ 𝐵
× ∪ 𝐵)))) |
52 | 12, 10, 11, 19, 1, 2 | om1addcl 22641 |
. . . 4
⊢ (𝜑 → (𝑀(*𝑝‘𝐽)𝑁) ∈ ∪ 𝐵) |
53 | | ecinxp 7709 |
. . . 4
⊢ ((((
≃ph‘𝐽) “ ∪ 𝐵) ⊆ ∪ 𝐵
∧ (𝑀(*𝑝‘𝐽)𝑁) ∈ ∪ 𝐵) → [(𝑀(*𝑝‘𝐽)𝑁)]( ≃ph‘𝐽) = [(𝑀(*𝑝‘𝐽)𝑁)](( ≃ph‘𝐽) ∩ (∪ 𝐵
× ∪ 𝐵))) |
54 | 46, 52, 53 | syl2anc 691 |
. . 3
⊢ (𝜑 → [(𝑀(*𝑝‘𝐽)𝑁)]( ≃ph‘𝐽) = [(𝑀(*𝑝‘𝐽)𝑁)](( ≃ph‘𝐽) ∩ (∪ 𝐵
× ∪ 𝐵))) |
55 | 32 | oveqd 6566 |
. . . 4
⊢ (𝜑 → (𝑀(*𝑝‘𝐽)𝑁) = (𝑀(+g‘(𝐽 Ω1 𝑌))𝑁)) |
56 | 55 | eceq1d 7670 |
. . 3
⊢ (𝜑 → [(𝑀(*𝑝‘𝐽)𝑁)](( ≃ph‘𝐽) ∩ (∪ 𝐵
× ∪ 𝐵)) = [(𝑀(+g‘(𝐽 Ω1 𝑌))𝑁)](( ≃ph‘𝐽) ∩ (∪ 𝐵
× ∪ 𝐵))) |
57 | 54, 56 | eqtrd 2644 |
. 2
⊢ (𝜑 → [(𝑀(*𝑝‘𝐽)𝑁)]( ≃ph‘𝐽) = [(𝑀(+g‘(𝐽 Ω1 𝑌))𝑁)](( ≃ph‘𝐽) ∩ (∪ 𝐵
× ∪ 𝐵))) |
58 | 44, 51, 57 | 3eqtr4d 2654 |
1
⊢ (𝜑 → ([𝑀]( ≃ph‘𝐽) + [𝑁]( ≃ph‘𝐽)) = [(𝑀(*𝑝‘𝐽)𝑁)]( ≃ph‘𝐽)) |