Step | Hyp | Ref
| Expression |
1 | | fconstmpt 5625 |
. . . . 5
⊢ ({𝐴} × {𝑥}) = (𝑘 ∈ {𝐴} ↦ 𝑥) |
2 | | pt1hmeo.a |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
3 | 2 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑉) |
4 | | sneq 4565 |
. . . . . . . . 9
⊢ (𝑘 = 𝐴 → {𝑘} = {𝐴}) |
5 | 4 | xpeq1d 5594 |
. . . . . . . 8
⊢ (𝑘 = 𝐴 → ({𝑘} × {𝑥}) = ({𝐴} × {𝑥})) |
6 | | opeq1 4798 |
. . . . . . . . 9
⊢ (𝑘 = 𝐴 → 〈𝑘, 𝑥〉 = 〈𝐴, 𝑥〉) |
7 | 6 | sneqd 4567 |
. . . . . . . 8
⊢ (𝑘 = 𝐴 → {〈𝑘, 𝑥〉} = {〈𝐴, 𝑥〉}) |
8 | 5, 7 | eqeq12d 2754 |
. . . . . . 7
⊢ (𝑘 = 𝐴 → (({𝑘} × {𝑥}) = {〈𝑘, 𝑥〉} ↔ ({𝐴} × {𝑥}) = {〈𝐴, 𝑥〉})) |
9 | | vex 3424 |
. . . . . . . 8
⊢ 𝑘 ∈ V |
10 | | vex 3424 |
. . . . . . . 8
⊢ 𝑥 ∈ V |
11 | 9, 10 | xpsn 6974 |
. . . . . . 7
⊢ ({𝑘} × {𝑥}) = {〈𝑘, 𝑥〉} |
12 | 8, 11 | vtoclg 3493 |
. . . . . 6
⊢ (𝐴 ∈ 𝑉 → ({𝐴} × {𝑥}) = {〈𝐴, 𝑥〉}) |
13 | 3, 12 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ({𝐴} × {𝑥}) = {〈𝐴, 𝑥〉}) |
14 | 1, 13 | eqtr3id 2793 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑘 ∈ {𝐴} ↦ 𝑥) = {〈𝐴, 𝑥〉}) |
15 | 14 | mpteq2dva 5164 |
. . 3
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝑘 ∈ {𝐴} ↦ 𝑥)) = (𝑥 ∈ 𝑋 ↦ {〈𝐴, 𝑥〉})) |
16 | | pt1hmeo.j |
. . . 4
⊢ 𝐾 =
(∏t‘{〈𝐴, 𝐽〉}) |
17 | | pt1hmeo.r |
. . . 4
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) |
18 | | snex 5338 |
. . . . 5
⊢ {𝐴} ∈ V |
19 | 18 | a1i 11 |
. . . 4
⊢ (𝜑 → {𝐴} ∈ V) |
20 | | topontop 21834 |
. . . . . 6
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top) |
21 | 17, 20 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐽 ∈ Top) |
22 | 2, 21 | fsnd 6721 |
. . . 4
⊢ (𝜑 → {〈𝐴, 𝐽〉}:{𝐴}⟶Top) |
23 | 17 | cnmptid 22582 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝑥) ∈ (𝐽 Cn 𝐽)) |
24 | 23 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ {𝐴}) → (𝑥 ∈ 𝑋 ↦ 𝑥) ∈ (𝐽 Cn 𝐽)) |
25 | | elsni 4572 |
. . . . . . . 8
⊢ (𝑘 ∈ {𝐴} → 𝑘 = 𝐴) |
26 | 25 | fveq2d 6739 |
. . . . . . 7
⊢ (𝑘 ∈ {𝐴} → ({〈𝐴, 𝐽〉}‘𝑘) = ({〈𝐴, 𝐽〉}‘𝐴)) |
27 | | fvsng 7013 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐽 ∈ (TopOn‘𝑋)) → ({〈𝐴, 𝐽〉}‘𝐴) = 𝐽) |
28 | 2, 17, 27 | syl2anc 587 |
. . . . . . 7
⊢ (𝜑 → ({〈𝐴, 𝐽〉}‘𝐴) = 𝐽) |
29 | 26, 28 | sylan9eqr 2801 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ {𝐴}) → ({〈𝐴, 𝐽〉}‘𝑘) = 𝐽) |
30 | 29 | oveq2d 7247 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ {𝐴}) → (𝐽 Cn ({〈𝐴, 𝐽〉}‘𝑘)) = (𝐽 Cn 𝐽)) |
31 | 24, 30 | eleqtrrd 2842 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ {𝐴}) → (𝑥 ∈ 𝑋 ↦ 𝑥) ∈ (𝐽 Cn ({〈𝐴, 𝐽〉}‘𝑘))) |
32 | 16, 17, 19, 22, 31 | ptcn 22548 |
. . 3
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝑘 ∈ {𝐴} ↦ 𝑥)) ∈ (𝐽 Cn 𝐾)) |
33 | 15, 32 | eqeltrrd 2840 |
. 2
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ {〈𝐴, 𝑥〉}) ∈ (𝐽 Cn 𝐾)) |
34 | | simprr 773 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 = {〈𝐴, 𝑥〉})) → 𝑦 = {〈𝐴, 𝑥〉}) |
35 | 14 | adantrr 717 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 = {〈𝐴, 𝑥〉})) → (𝑘 ∈ {𝐴} ↦ 𝑥) = {〈𝐴, 𝑥〉}) |
36 | 34, 35 | eqtr4d 2781 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 = {〈𝐴, 𝑥〉})) → 𝑦 = (𝑘 ∈ {𝐴} ↦ 𝑥)) |
37 | | simprl 771 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 = {〈𝐴, 𝑥〉})) → 𝑥 ∈ 𝑋) |
38 | 37 | adantr 484 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 = {〈𝐴, 𝑥〉})) ∧ 𝑘 ∈ {𝐴}) → 𝑥 ∈ 𝑋) |
39 | 38 | fmpttd 6950 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 = {〈𝐴, 𝑥〉})) → (𝑘 ∈ {𝐴} ↦ 𝑥):{𝐴}⟶𝑋) |
40 | | toponmax 21847 |
. . . . . . . . . . . 12
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 ∈ 𝐽) |
41 | 17, 40 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑋 ∈ 𝐽) |
42 | 41 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 = {〈𝐴, 𝑥〉})) → 𝑋 ∈ 𝐽) |
43 | | elmapg 8541 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ 𝐽 ∧ {𝐴} ∈ V) → ((𝑘 ∈ {𝐴} ↦ 𝑥) ∈ (𝑋 ↑m {𝐴}) ↔ (𝑘 ∈ {𝐴} ↦ 𝑥):{𝐴}⟶𝑋)) |
44 | 42, 18, 43 | sylancl 589 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 = {〈𝐴, 𝑥〉})) → ((𝑘 ∈ {𝐴} ↦ 𝑥) ∈ (𝑋 ↑m {𝐴}) ↔ (𝑘 ∈ {𝐴} ↦ 𝑥):{𝐴}⟶𝑋)) |
45 | 39, 44 | mpbird 260 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 = {〈𝐴, 𝑥〉})) → (𝑘 ∈ {𝐴} ↦ 𝑥) ∈ (𝑋 ↑m {𝐴})) |
46 | 36, 45 | eqeltrd 2839 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 = {〈𝐴, 𝑥〉})) → 𝑦 ∈ (𝑋 ↑m {𝐴})) |
47 | 34 | fveq1d 6737 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 = {〈𝐴, 𝑥〉})) → (𝑦‘𝐴) = ({〈𝐴, 𝑥〉}‘𝐴)) |
48 | 2 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 = {〈𝐴, 𝑥〉})) → 𝐴 ∈ 𝑉) |
49 | | fvsng 7013 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ 𝑋) → ({〈𝐴, 𝑥〉}‘𝐴) = 𝑥) |
50 | 48, 37, 49 | syl2anc 587 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 = {〈𝐴, 𝑥〉})) → ({〈𝐴, 𝑥〉}‘𝐴) = 𝑥) |
51 | 47, 50 | eqtr2d 2779 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 = {〈𝐴, 𝑥〉})) → 𝑥 = (𝑦‘𝐴)) |
52 | 46, 51 | jca 515 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 = {〈𝐴, 𝑥〉})) → (𝑦 ∈ (𝑋 ↑m {𝐴}) ∧ 𝑥 = (𝑦‘𝐴))) |
53 | | simprr 773 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ (𝑋 ↑m {𝐴}) ∧ 𝑥 = (𝑦‘𝐴))) → 𝑥 = (𝑦‘𝐴)) |
54 | | simprl 771 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ∈ (𝑋 ↑m {𝐴}) ∧ 𝑥 = (𝑦‘𝐴))) → 𝑦 ∈ (𝑋 ↑m {𝐴})) |
55 | 41 | adantr 484 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 ∈ (𝑋 ↑m {𝐴}) ∧ 𝑥 = (𝑦‘𝐴))) → 𝑋 ∈ 𝐽) |
56 | | elmapg 8541 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ 𝐽 ∧ {𝐴} ∈ V) → (𝑦 ∈ (𝑋 ↑m {𝐴}) ↔ 𝑦:{𝐴}⟶𝑋)) |
57 | 55, 18, 56 | sylancl 589 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ∈ (𝑋 ↑m {𝐴}) ∧ 𝑥 = (𝑦‘𝐴))) → (𝑦 ∈ (𝑋 ↑m {𝐴}) ↔ 𝑦:{𝐴}⟶𝑋)) |
58 | 54, 57 | mpbid 235 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ (𝑋 ↑m {𝐴}) ∧ 𝑥 = (𝑦‘𝐴))) → 𝑦:{𝐴}⟶𝑋) |
59 | | snidg 4589 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ {𝐴}) |
60 | 2, 59 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈ {𝐴}) |
61 | 60 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ (𝑋 ↑m {𝐴}) ∧ 𝑥 = (𝑦‘𝐴))) → 𝐴 ∈ {𝐴}) |
62 | 58, 61 | ffvelrnd 6923 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ (𝑋 ↑m {𝐴}) ∧ 𝑥 = (𝑦‘𝐴))) → (𝑦‘𝐴) ∈ 𝑋) |
63 | 53, 62 | eqeltrd 2839 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ (𝑋 ↑m {𝐴}) ∧ 𝑥 = (𝑦‘𝐴))) → 𝑥 ∈ 𝑋) |
64 | 2 | adantr 484 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 ∈ (𝑋 ↑m {𝐴}) ∧ 𝑥 = (𝑦‘𝐴))) → 𝐴 ∈ 𝑉) |
65 | | fsn2g 6971 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ 𝑉 → (𝑦:{𝐴}⟶𝑋 ↔ ((𝑦‘𝐴) ∈ 𝑋 ∧ 𝑦 = {〈𝐴, (𝑦‘𝐴)〉}))) |
66 | 64, 65 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ∈ (𝑋 ↑m {𝐴}) ∧ 𝑥 = (𝑦‘𝐴))) → (𝑦:{𝐴}⟶𝑋 ↔ ((𝑦‘𝐴) ∈ 𝑋 ∧ 𝑦 = {〈𝐴, (𝑦‘𝐴)〉}))) |
67 | 58, 66 | mpbid 235 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ (𝑋 ↑m {𝐴}) ∧ 𝑥 = (𝑦‘𝐴))) → ((𝑦‘𝐴) ∈ 𝑋 ∧ 𝑦 = {〈𝐴, (𝑦‘𝐴)〉})) |
68 | 67 | simprd 499 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ (𝑋 ↑m {𝐴}) ∧ 𝑥 = (𝑦‘𝐴))) → 𝑦 = {〈𝐴, (𝑦‘𝐴)〉}) |
69 | 53 | opeq2d 4805 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ (𝑋 ↑m {𝐴}) ∧ 𝑥 = (𝑦‘𝐴))) → 〈𝐴, 𝑥〉 = 〈𝐴, (𝑦‘𝐴)〉) |
70 | 69 | sneqd 4567 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ (𝑋 ↑m {𝐴}) ∧ 𝑥 = (𝑦‘𝐴))) → {〈𝐴, 𝑥〉} = {〈𝐴, (𝑦‘𝐴)〉}) |
71 | 68, 70 | eqtr4d 2781 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ (𝑋 ↑m {𝐴}) ∧ 𝑥 = (𝑦‘𝐴))) → 𝑦 = {〈𝐴, 𝑥〉}) |
72 | 63, 71 | jca 515 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ (𝑋 ↑m {𝐴}) ∧ 𝑥 = (𝑦‘𝐴))) → (𝑥 ∈ 𝑋 ∧ 𝑦 = {〈𝐴, 𝑥〉})) |
73 | 52, 72 | impbida 801 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ 𝑋 ∧ 𝑦 = {〈𝐴, 𝑥〉}) ↔ (𝑦 ∈ (𝑋 ↑m {𝐴}) ∧ 𝑥 = (𝑦‘𝐴)))) |
74 | 73 | mptcnv 6017 |
. . . 4
⊢ (𝜑 → ◡(𝑥 ∈ 𝑋 ↦ {〈𝐴, 𝑥〉}) = (𝑦 ∈ (𝑋 ↑m {𝐴}) ↦ (𝑦‘𝐴))) |
75 | | xpsng 6972 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐽 ∈ (TopOn‘𝑋)) → ({𝐴} × {𝐽}) = {〈𝐴, 𝐽〉}) |
76 | 2, 17, 75 | syl2anc 587 |
. . . . . . . . . 10
⊢ (𝜑 → ({𝐴} × {𝐽}) = {〈𝐴, 𝐽〉}) |
77 | 76 | eqcomd 2744 |
. . . . . . . . 9
⊢ (𝜑 → {〈𝐴, 𝐽〉} = ({𝐴} × {𝐽})) |
78 | 77 | fveq2d 6739 |
. . . . . . . 8
⊢ (𝜑 →
(∏t‘{〈𝐴, 𝐽〉}) = (∏t‘({𝐴} × {𝐽}))) |
79 | 16, 78 | syl5eq 2791 |
. . . . . . 7
⊢ (𝜑 → 𝐾 = (∏t‘({𝐴} × {𝐽}))) |
80 | | eqid 2738 |
. . . . . . . . 9
⊢
(∏t‘({𝐴} × {𝐽})) = (∏t‘({𝐴} × {𝐽})) |
81 | 80 | pttoponconst 22518 |
. . . . . . . 8
⊢ (({𝐴} ∈ V ∧ 𝐽 ∈ (TopOn‘𝑋)) →
(∏t‘({𝐴} × {𝐽})) ∈ (TopOn‘(𝑋 ↑m {𝐴}))) |
82 | 19, 17, 81 | syl2anc 587 |
. . . . . . 7
⊢ (𝜑 →
(∏t‘({𝐴} × {𝐽})) ∈ (TopOn‘(𝑋 ↑m {𝐴}))) |
83 | 79, 82 | eqeltrd 2839 |
. . . . . 6
⊢ (𝜑 → 𝐾 ∈ (TopOn‘(𝑋 ↑m {𝐴}))) |
84 | | toponuni 21835 |
. . . . . 6
⊢ (𝐾 ∈ (TopOn‘(𝑋 ↑m {𝐴})) → (𝑋 ↑m {𝐴}) = ∪ 𝐾) |
85 | 83, 84 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝑋 ↑m {𝐴}) = ∪ 𝐾) |
86 | 85 | mpteq1d 5158 |
. . . 4
⊢ (𝜑 → (𝑦 ∈ (𝑋 ↑m {𝐴}) ↦ (𝑦‘𝐴)) = (𝑦 ∈ ∪ 𝐾 ↦ (𝑦‘𝐴))) |
87 | 74, 86 | eqtrd 2778 |
. . 3
⊢ (𝜑 → ◡(𝑥 ∈ 𝑋 ↦ {〈𝐴, 𝑥〉}) = (𝑦 ∈ ∪ 𝐾 ↦ (𝑦‘𝐴))) |
88 | | eqid 2738 |
. . . . . 6
⊢ ∪ 𝐾 =
∪ 𝐾 |
89 | 88, 16 | ptpjcn 22532 |
. . . . 5
⊢ (({𝐴} ∈ V ∧ {〈𝐴, 𝐽〉}:{𝐴}⟶Top ∧ 𝐴 ∈ {𝐴}) → (𝑦 ∈ ∪ 𝐾 ↦ (𝑦‘𝐴)) ∈ (𝐾 Cn ({〈𝐴, 𝐽〉}‘𝐴))) |
90 | 18, 22, 60, 89 | mp3an2i 1468 |
. . . 4
⊢ (𝜑 → (𝑦 ∈ ∪ 𝐾 ↦ (𝑦‘𝐴)) ∈ (𝐾 Cn ({〈𝐴, 𝐽〉}‘𝐴))) |
91 | 28 | oveq2d 7247 |
. . . 4
⊢ (𝜑 → (𝐾 Cn ({〈𝐴, 𝐽〉}‘𝐴)) = (𝐾 Cn 𝐽)) |
92 | 90, 91 | eleqtrd 2841 |
. . 3
⊢ (𝜑 → (𝑦 ∈ ∪ 𝐾 ↦ (𝑦‘𝐴)) ∈ (𝐾 Cn 𝐽)) |
93 | 87, 92 | eqeltrd 2839 |
. 2
⊢ (𝜑 → ◡(𝑥 ∈ 𝑋 ↦ {〈𝐴, 𝑥〉}) ∈ (𝐾 Cn 𝐽)) |
94 | | ishmeo 22680 |
. 2
⊢ ((𝑥 ∈ 𝑋 ↦ {〈𝐴, 𝑥〉}) ∈ (𝐽Homeo𝐾) ↔ ((𝑥 ∈ 𝑋 ↦ {〈𝐴, 𝑥〉}) ∈ (𝐽 Cn 𝐾) ∧ ◡(𝑥 ∈ 𝑋 ↦ {〈𝐴, 𝑥〉}) ∈ (𝐾 Cn 𝐽))) |
95 | 33, 93, 94 | sylanbrc 586 |
1
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ {〈𝐴, 𝑥〉}) ∈ (𝐽Homeo𝐾)) |