Step |
Hyp |
Ref |
Expression |
1 |
|
hauseqlcld.k |
⊢ ( 𝜑 → 𝐾 ∈ Haus ) |
2 |
|
hauseqlcld.f |
⊢ ( 𝜑 → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) |
3 |
|
hauseqlcld.g |
⊢ ( 𝜑 → 𝐺 ∈ ( 𝐽 Cn 𝐾 ) ) |
4 |
|
eqid |
⊢ ∪ 𝐽 = ∪ 𝐽 |
5 |
|
eqid |
⊢ ∪ 𝐾 = ∪ 𝐾 |
6 |
4 5
|
cnf |
⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐹 : ∪ 𝐽 ⟶ ∪ 𝐾 ) |
7 |
2 6
|
syl |
⊢ ( 𝜑 → 𝐹 : ∪ 𝐽 ⟶ ∪ 𝐾 ) |
8 |
7
|
ffvelrnda |
⊢ ( ( 𝜑 ∧ 𝑏 ∈ ∪ 𝐽 ) → ( 𝐹 ‘ 𝑏 ) ∈ ∪ 𝐾 ) |
9 |
8
|
biantrurd |
⊢ ( ( 𝜑 ∧ 𝑏 ∈ ∪ 𝐽 ) → ( 〈 ( 𝐹 ‘ 𝑏 ) , ( 𝐺 ‘ 𝑏 ) 〉 ∈ I ↔ ( ( 𝐹 ‘ 𝑏 ) ∈ ∪ 𝐾 ∧ 〈 ( 𝐹 ‘ 𝑏 ) , ( 𝐺 ‘ 𝑏 ) 〉 ∈ I ) ) ) |
10 |
|
fvex |
⊢ ( 𝐺 ‘ 𝑏 ) ∈ V |
11 |
10
|
ideq |
⊢ ( ( 𝐹 ‘ 𝑏 ) I ( 𝐺 ‘ 𝑏 ) ↔ ( 𝐹 ‘ 𝑏 ) = ( 𝐺 ‘ 𝑏 ) ) |
12 |
|
df-br |
⊢ ( ( 𝐹 ‘ 𝑏 ) I ( 𝐺 ‘ 𝑏 ) ↔ 〈 ( 𝐹 ‘ 𝑏 ) , ( 𝐺 ‘ 𝑏 ) 〉 ∈ I ) |
13 |
11 12
|
bitr3i |
⊢ ( ( 𝐹 ‘ 𝑏 ) = ( 𝐺 ‘ 𝑏 ) ↔ 〈 ( 𝐹 ‘ 𝑏 ) , ( 𝐺 ‘ 𝑏 ) 〉 ∈ I ) |
14 |
10
|
opelresi |
⊢ ( 〈 ( 𝐹 ‘ 𝑏 ) , ( 𝐺 ‘ 𝑏 ) 〉 ∈ ( I ↾ ∪ 𝐾 ) ↔ ( ( 𝐹 ‘ 𝑏 ) ∈ ∪ 𝐾 ∧ 〈 ( 𝐹 ‘ 𝑏 ) , ( 𝐺 ‘ 𝑏 ) 〉 ∈ I ) ) |
15 |
9 13 14
|
3bitr4g |
⊢ ( ( 𝜑 ∧ 𝑏 ∈ ∪ 𝐽 ) → ( ( 𝐹 ‘ 𝑏 ) = ( 𝐺 ‘ 𝑏 ) ↔ 〈 ( 𝐹 ‘ 𝑏 ) , ( 𝐺 ‘ 𝑏 ) 〉 ∈ ( I ↾ ∪ 𝐾 ) ) ) |
16 |
|
fveq2 |
⊢ ( 𝑎 = 𝑏 → ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) ) |
17 |
|
fveq2 |
⊢ ( 𝑎 = 𝑏 → ( 𝐺 ‘ 𝑎 ) = ( 𝐺 ‘ 𝑏 ) ) |
18 |
16 17
|
opeq12d |
⊢ ( 𝑎 = 𝑏 → 〈 ( 𝐹 ‘ 𝑎 ) , ( 𝐺 ‘ 𝑎 ) 〉 = 〈 ( 𝐹 ‘ 𝑏 ) , ( 𝐺 ‘ 𝑏 ) 〉 ) |
19 |
|
eqid |
⊢ ( 𝑎 ∈ ∪ 𝐽 ↦ 〈 ( 𝐹 ‘ 𝑎 ) , ( 𝐺 ‘ 𝑎 ) 〉 ) = ( 𝑎 ∈ ∪ 𝐽 ↦ 〈 ( 𝐹 ‘ 𝑎 ) , ( 𝐺 ‘ 𝑎 ) 〉 ) |
20 |
|
opex |
⊢ 〈 ( 𝐹 ‘ 𝑏 ) , ( 𝐺 ‘ 𝑏 ) 〉 ∈ V |
21 |
18 19 20
|
fvmpt |
⊢ ( 𝑏 ∈ ∪ 𝐽 → ( ( 𝑎 ∈ ∪ 𝐽 ↦ 〈 ( 𝐹 ‘ 𝑎 ) , ( 𝐺 ‘ 𝑎 ) 〉 ) ‘ 𝑏 ) = 〈 ( 𝐹 ‘ 𝑏 ) , ( 𝐺 ‘ 𝑏 ) 〉 ) |
22 |
21
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑏 ∈ ∪ 𝐽 ) → ( ( 𝑎 ∈ ∪ 𝐽 ↦ 〈 ( 𝐹 ‘ 𝑎 ) , ( 𝐺 ‘ 𝑎 ) 〉 ) ‘ 𝑏 ) = 〈 ( 𝐹 ‘ 𝑏 ) , ( 𝐺 ‘ 𝑏 ) 〉 ) |
23 |
22
|
eleq1d |
⊢ ( ( 𝜑 ∧ 𝑏 ∈ ∪ 𝐽 ) → ( ( ( 𝑎 ∈ ∪ 𝐽 ↦ 〈 ( 𝐹 ‘ 𝑎 ) , ( 𝐺 ‘ 𝑎 ) 〉 ) ‘ 𝑏 ) ∈ ( I ↾ ∪ 𝐾 ) ↔ 〈 ( 𝐹 ‘ 𝑏 ) , ( 𝐺 ‘ 𝑏 ) 〉 ∈ ( I ↾ ∪ 𝐾 ) ) ) |
24 |
15 23
|
bitr4d |
⊢ ( ( 𝜑 ∧ 𝑏 ∈ ∪ 𝐽 ) → ( ( 𝐹 ‘ 𝑏 ) = ( 𝐺 ‘ 𝑏 ) ↔ ( ( 𝑎 ∈ ∪ 𝐽 ↦ 〈 ( 𝐹 ‘ 𝑎 ) , ( 𝐺 ‘ 𝑎 ) 〉 ) ‘ 𝑏 ) ∈ ( I ↾ ∪ 𝐾 ) ) ) |
25 |
24
|
pm5.32da |
⊢ ( 𝜑 → ( ( 𝑏 ∈ ∪ 𝐽 ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐺 ‘ 𝑏 ) ) ↔ ( 𝑏 ∈ ∪ 𝐽 ∧ ( ( 𝑎 ∈ ∪ 𝐽 ↦ 〈 ( 𝐹 ‘ 𝑎 ) , ( 𝐺 ‘ 𝑎 ) 〉 ) ‘ 𝑏 ) ∈ ( I ↾ ∪ 𝐾 ) ) ) ) |
26 |
7
|
ffnd |
⊢ ( 𝜑 → 𝐹 Fn ∪ 𝐽 ) |
27 |
4 5
|
cnf |
⊢ ( 𝐺 ∈ ( 𝐽 Cn 𝐾 ) → 𝐺 : ∪ 𝐽 ⟶ ∪ 𝐾 ) |
28 |
3 27
|
syl |
⊢ ( 𝜑 → 𝐺 : ∪ 𝐽 ⟶ ∪ 𝐾 ) |
29 |
28
|
ffnd |
⊢ ( 𝜑 → 𝐺 Fn ∪ 𝐽 ) |
30 |
|
fndmin |
⊢ ( ( 𝐹 Fn ∪ 𝐽 ∧ 𝐺 Fn ∪ 𝐽 ) → dom ( 𝐹 ∩ 𝐺 ) = { 𝑏 ∈ ∪ 𝐽 ∣ ( 𝐹 ‘ 𝑏 ) = ( 𝐺 ‘ 𝑏 ) } ) |
31 |
26 29 30
|
syl2anc |
⊢ ( 𝜑 → dom ( 𝐹 ∩ 𝐺 ) = { 𝑏 ∈ ∪ 𝐽 ∣ ( 𝐹 ‘ 𝑏 ) = ( 𝐺 ‘ 𝑏 ) } ) |
32 |
31
|
eleq2d |
⊢ ( 𝜑 → ( 𝑏 ∈ dom ( 𝐹 ∩ 𝐺 ) ↔ 𝑏 ∈ { 𝑏 ∈ ∪ 𝐽 ∣ ( 𝐹 ‘ 𝑏 ) = ( 𝐺 ‘ 𝑏 ) } ) ) |
33 |
|
rabid |
⊢ ( 𝑏 ∈ { 𝑏 ∈ ∪ 𝐽 ∣ ( 𝐹 ‘ 𝑏 ) = ( 𝐺 ‘ 𝑏 ) } ↔ ( 𝑏 ∈ ∪ 𝐽 ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐺 ‘ 𝑏 ) ) ) |
34 |
32 33
|
bitrdi |
⊢ ( 𝜑 → ( 𝑏 ∈ dom ( 𝐹 ∩ 𝐺 ) ↔ ( 𝑏 ∈ ∪ 𝐽 ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐺 ‘ 𝑏 ) ) ) ) |
35 |
|
opex |
⊢ 〈 ( 𝐹 ‘ 𝑎 ) , ( 𝐺 ‘ 𝑎 ) 〉 ∈ V |
36 |
35 19
|
fnmpti |
⊢ ( 𝑎 ∈ ∪ 𝐽 ↦ 〈 ( 𝐹 ‘ 𝑎 ) , ( 𝐺 ‘ 𝑎 ) 〉 ) Fn ∪ 𝐽 |
37 |
|
elpreima |
⊢ ( ( 𝑎 ∈ ∪ 𝐽 ↦ 〈 ( 𝐹 ‘ 𝑎 ) , ( 𝐺 ‘ 𝑎 ) 〉 ) Fn ∪ 𝐽 → ( 𝑏 ∈ ( ◡ ( 𝑎 ∈ ∪ 𝐽 ↦ 〈 ( 𝐹 ‘ 𝑎 ) , ( 𝐺 ‘ 𝑎 ) 〉 ) “ ( I ↾ ∪ 𝐾 ) ) ↔ ( 𝑏 ∈ ∪ 𝐽 ∧ ( ( 𝑎 ∈ ∪ 𝐽 ↦ 〈 ( 𝐹 ‘ 𝑎 ) , ( 𝐺 ‘ 𝑎 ) 〉 ) ‘ 𝑏 ) ∈ ( I ↾ ∪ 𝐾 ) ) ) ) |
38 |
36 37
|
mp1i |
⊢ ( 𝜑 → ( 𝑏 ∈ ( ◡ ( 𝑎 ∈ ∪ 𝐽 ↦ 〈 ( 𝐹 ‘ 𝑎 ) , ( 𝐺 ‘ 𝑎 ) 〉 ) “ ( I ↾ ∪ 𝐾 ) ) ↔ ( 𝑏 ∈ ∪ 𝐽 ∧ ( ( 𝑎 ∈ ∪ 𝐽 ↦ 〈 ( 𝐹 ‘ 𝑎 ) , ( 𝐺 ‘ 𝑎 ) 〉 ) ‘ 𝑏 ) ∈ ( I ↾ ∪ 𝐾 ) ) ) ) |
39 |
25 34 38
|
3bitr4d |
⊢ ( 𝜑 → ( 𝑏 ∈ dom ( 𝐹 ∩ 𝐺 ) ↔ 𝑏 ∈ ( ◡ ( 𝑎 ∈ ∪ 𝐽 ↦ 〈 ( 𝐹 ‘ 𝑎 ) , ( 𝐺 ‘ 𝑎 ) 〉 ) “ ( I ↾ ∪ 𝐾 ) ) ) ) |
40 |
39
|
eqrdv |
⊢ ( 𝜑 → dom ( 𝐹 ∩ 𝐺 ) = ( ◡ ( 𝑎 ∈ ∪ 𝐽 ↦ 〈 ( 𝐹 ‘ 𝑎 ) , ( 𝐺 ‘ 𝑎 ) 〉 ) “ ( I ↾ ∪ 𝐾 ) ) ) |
41 |
4 19
|
txcnmpt |
⊢ ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝐺 ∈ ( 𝐽 Cn 𝐾 ) ) → ( 𝑎 ∈ ∪ 𝐽 ↦ 〈 ( 𝐹 ‘ 𝑎 ) , ( 𝐺 ‘ 𝑎 ) 〉 ) ∈ ( 𝐽 Cn ( 𝐾 ×t 𝐾 ) ) ) |
42 |
2 3 41
|
syl2anc |
⊢ ( 𝜑 → ( 𝑎 ∈ ∪ 𝐽 ↦ 〈 ( 𝐹 ‘ 𝑎 ) , ( 𝐺 ‘ 𝑎 ) 〉 ) ∈ ( 𝐽 Cn ( 𝐾 ×t 𝐾 ) ) ) |
43 |
5
|
hausdiag |
⊢ ( 𝐾 ∈ Haus ↔ ( 𝐾 ∈ Top ∧ ( I ↾ ∪ 𝐾 ) ∈ ( Clsd ‘ ( 𝐾 ×t 𝐾 ) ) ) ) |
44 |
43
|
simprbi |
⊢ ( 𝐾 ∈ Haus → ( I ↾ ∪ 𝐾 ) ∈ ( Clsd ‘ ( 𝐾 ×t 𝐾 ) ) ) |
45 |
1 44
|
syl |
⊢ ( 𝜑 → ( I ↾ ∪ 𝐾 ) ∈ ( Clsd ‘ ( 𝐾 ×t 𝐾 ) ) ) |
46 |
|
cnclima |
⊢ ( ( ( 𝑎 ∈ ∪ 𝐽 ↦ 〈 ( 𝐹 ‘ 𝑎 ) , ( 𝐺 ‘ 𝑎 ) 〉 ) ∈ ( 𝐽 Cn ( 𝐾 ×t 𝐾 ) ) ∧ ( I ↾ ∪ 𝐾 ) ∈ ( Clsd ‘ ( 𝐾 ×t 𝐾 ) ) ) → ( ◡ ( 𝑎 ∈ ∪ 𝐽 ↦ 〈 ( 𝐹 ‘ 𝑎 ) , ( 𝐺 ‘ 𝑎 ) 〉 ) “ ( I ↾ ∪ 𝐾 ) ) ∈ ( Clsd ‘ 𝐽 ) ) |
47 |
42 45 46
|
syl2anc |
⊢ ( 𝜑 → ( ◡ ( 𝑎 ∈ ∪ 𝐽 ↦ 〈 ( 𝐹 ‘ 𝑎 ) , ( 𝐺 ‘ 𝑎 ) 〉 ) “ ( I ↾ ∪ 𝐾 ) ) ∈ ( Clsd ‘ 𝐽 ) ) |
48 |
40 47
|
eqeltrd |
⊢ ( 𝜑 → dom ( 𝐹 ∩ 𝐺 ) ∈ ( Clsd ‘ 𝐽 ) ) |