Step | Hyp | Ref
| Expression |
1 | | f1stres 7740 |
. . . 4
⊢
(1st ↾ (∪ 𝑆 × ∪ 𝑇)):(∪
𝑆 × ∪ 𝑇)⟶∪ 𝑆 |
2 | | 1stmbfm.1 |
. . . . . 6
⊢ (𝜑 → 𝑆 ∈ ∪ ran
sigAlgebra) |
3 | | 1stmbfm.2 |
. . . . . 6
⊢ (𝜑 → 𝑇 ∈ ∪ ran
sigAlgebra) |
4 | | sxuni 31733 |
. . . . . 6
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑇 ∈ ∪ ran
sigAlgebra) → (∪ 𝑆 × ∪ 𝑇) = ∪
(𝑆 ×s
𝑇)) |
5 | 2, 3, 4 | syl2anc 587 |
. . . . 5
⊢ (𝜑 → (∪ 𝑆
× ∪ 𝑇) = ∪ (𝑆 ×s 𝑇)) |
6 | 5 | feq2d 6490 |
. . . 4
⊢ (𝜑 → ((1st ↾
(∪ 𝑆 × ∪ 𝑇)):(∪
𝑆 × ∪ 𝑇)⟶∪ 𝑆 ↔ (1st ↾
(∪ 𝑆 × ∪ 𝑇)):∪
(𝑆 ×s
𝑇)⟶∪ 𝑆)) |
7 | 1, 6 | mpbii 236 |
. . 3
⊢ (𝜑 → (1st ↾
(∪ 𝑆 × ∪ 𝑇)):∪
(𝑆 ×s
𝑇)⟶∪ 𝑆) |
8 | | unielsiga 31668 |
. . . . 5
⊢ (𝑆 ∈ ∪ ran sigAlgebra → ∪ 𝑆 ∈ 𝑆) |
9 | 2, 8 | syl 17 |
. . . 4
⊢ (𝜑 → ∪ 𝑆
∈ 𝑆) |
10 | | sxsiga 31731 |
. . . . . 6
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑇 ∈ ∪ ran
sigAlgebra) → (𝑆
×s 𝑇)
∈ ∪ ran sigAlgebra) |
11 | 2, 3, 10 | syl2anc 587 |
. . . . 5
⊢ (𝜑 → (𝑆 ×s 𝑇) ∈ ∪ ran
sigAlgebra) |
12 | | unielsiga 31668 |
. . . . 5
⊢ ((𝑆 ×s 𝑇) ∈ ∪ ran sigAlgebra → ∪
(𝑆 ×s
𝑇) ∈ (𝑆 ×s 𝑇)) |
13 | 11, 12 | syl 17 |
. . . 4
⊢ (𝜑 → ∪ (𝑆
×s 𝑇)
∈ (𝑆
×s 𝑇)) |
14 | 9, 13 | elmapd 8453 |
. . 3
⊢ (𝜑 → ((1st ↾
(∪ 𝑆 × ∪ 𝑇)) ∈ (∪ 𝑆
↑m ∪ (𝑆 ×s 𝑇)) ↔ (1st ↾ (∪ 𝑆
× ∪ 𝑇)):∪ (𝑆 ×s 𝑇)⟶∪ 𝑆)) |
15 | 7, 14 | mpbird 260 |
. 2
⊢ (𝜑 → (1st ↾
(∪ 𝑆 × ∪ 𝑇)) ∈ (∪ 𝑆
↑m ∪ (𝑆 ×s 𝑇))) |
16 | | ffn 6504 |
. . . . . . . 8
⊢
((1st ↾ (∪ 𝑆 × ∪ 𝑇)):(∪
𝑆 × ∪ 𝑇)⟶∪ 𝑆 → (1st ↾
(∪ 𝑆 × ∪ 𝑇)) Fn (∪ 𝑆
× ∪ 𝑇)) |
17 | | elpreima 6837 |
. . . . . . . 8
⊢
((1st ↾ (∪ 𝑆 × ∪ 𝑇)) Fn (∪ 𝑆
× ∪ 𝑇) → (𝑧 ∈ (◡(1st ↾ (∪ 𝑆
× ∪ 𝑇)) “ 𝑎) ↔ (𝑧 ∈ (∪ 𝑆 × ∪ 𝑇)
∧ ((1st ↾ (∪ 𝑆 × ∪ 𝑇))‘𝑧) ∈ 𝑎))) |
18 | 1, 16, 17 | mp2b 10 |
. . . . . . 7
⊢ (𝑧 ∈ (◡(1st ↾ (∪ 𝑆
× ∪ 𝑇)) “ 𝑎) ↔ (𝑧 ∈ (∪ 𝑆 × ∪ 𝑇)
∧ ((1st ↾ (∪ 𝑆 × ∪ 𝑇))‘𝑧) ∈ 𝑎)) |
19 | | fvres 6695 |
. . . . . . . . . 10
⊢ (𝑧 ∈ (∪ 𝑆
× ∪ 𝑇) → ((1st ↾ (∪ 𝑆
× ∪ 𝑇))‘𝑧) = (1st ‘𝑧)) |
20 | 19 | eleq1d 2817 |
. . . . . . . . 9
⊢ (𝑧 ∈ (∪ 𝑆
× ∪ 𝑇) → (((1st ↾ (∪ 𝑆
× ∪ 𝑇))‘𝑧) ∈ 𝑎 ↔ (1st ‘𝑧) ∈ 𝑎)) |
21 | | 1st2nd2 7755 |
. . . . . . . . . 10
⊢ (𝑧 ∈ (∪ 𝑆
× ∪ 𝑇) → 𝑧 = 〈(1st ‘𝑧), (2nd ‘𝑧)〉) |
22 | | xp2nd 7749 |
. . . . . . . . . 10
⊢ (𝑧 ∈ (∪ 𝑆
× ∪ 𝑇) → (2nd ‘𝑧) ∈ ∪ 𝑇) |
23 | | elxp6 7750 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ (𝑎 × ∪ 𝑇) ↔ (𝑧 = 〈(1st ‘𝑧), (2nd ‘𝑧)〉 ∧ ((1st
‘𝑧) ∈ 𝑎 ∧ (2nd
‘𝑧) ∈ ∪ 𝑇))) |
24 | | anass 472 |
. . . . . . . . . . . 12
⊢ (((𝑧 = 〈(1st
‘𝑧), (2nd
‘𝑧)〉 ∧
(1st ‘𝑧)
∈ 𝑎) ∧
(2nd ‘𝑧)
∈ ∪ 𝑇) ↔ (𝑧 = 〈(1st ‘𝑧), (2nd ‘𝑧)〉 ∧ ((1st
‘𝑧) ∈ 𝑎 ∧ (2nd
‘𝑧) ∈ ∪ 𝑇))) |
25 | | an32 646 |
. . . . . . . . . . . 12
⊢ (((𝑧 = 〈(1st
‘𝑧), (2nd
‘𝑧)〉 ∧
(1st ‘𝑧)
∈ 𝑎) ∧
(2nd ‘𝑧)
∈ ∪ 𝑇) ↔ ((𝑧 = 〈(1st ‘𝑧), (2nd ‘𝑧)〉 ∧ (2nd
‘𝑧) ∈ ∪ 𝑇)
∧ (1st ‘𝑧) ∈ 𝑎)) |
26 | 23, 24, 25 | 3bitr2i 302 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ (𝑎 × ∪ 𝑇) ↔ ((𝑧 = 〈(1st ‘𝑧), (2nd ‘𝑧)〉 ∧ (2nd
‘𝑧) ∈ ∪ 𝑇)
∧ (1st ‘𝑧) ∈ 𝑎)) |
27 | 26 | baib 539 |
. . . . . . . . . 10
⊢ ((𝑧 = 〈(1st
‘𝑧), (2nd
‘𝑧)〉 ∧
(2nd ‘𝑧)
∈ ∪ 𝑇) → (𝑧 ∈ (𝑎 × ∪ 𝑇) ↔ (1st
‘𝑧) ∈ 𝑎)) |
28 | 21, 22, 27 | syl2anc 587 |
. . . . . . . . 9
⊢ (𝑧 ∈ (∪ 𝑆
× ∪ 𝑇) → (𝑧 ∈ (𝑎 × ∪ 𝑇) ↔ (1st
‘𝑧) ∈ 𝑎)) |
29 | 20, 28 | bitr4d 285 |
. . . . . . . 8
⊢ (𝑧 ∈ (∪ 𝑆
× ∪ 𝑇) → (((1st ↾ (∪ 𝑆
× ∪ 𝑇))‘𝑧) ∈ 𝑎 ↔ 𝑧 ∈ (𝑎 × ∪ 𝑇))) |
30 | 29 | pm5.32i 578 |
. . . . . . 7
⊢ ((𝑧 ∈ (∪ 𝑆
× ∪ 𝑇) ∧ ((1st ↾ (∪ 𝑆
× ∪ 𝑇))‘𝑧) ∈ 𝑎) ↔ (𝑧 ∈ (∪ 𝑆 × ∪ 𝑇)
∧ 𝑧 ∈ (𝑎 × ∪ 𝑇))) |
31 | 18, 30 | bitri 278 |
. . . . . 6
⊢ (𝑧 ∈ (◡(1st ↾ (∪ 𝑆
× ∪ 𝑇)) “ 𝑎) ↔ (𝑧 ∈ (∪ 𝑆 × ∪ 𝑇)
∧ 𝑧 ∈ (𝑎 × ∪ 𝑇))) |
32 | | sgon 31664 |
. . . . . . . . . . 11
⊢ (𝑆 ∈ ∪ ran sigAlgebra → 𝑆 ∈ (sigAlgebra‘∪ 𝑆)) |
33 | | sigasspw 31656 |
. . . . . . . . . . 11
⊢ (𝑆 ∈ (sigAlgebra‘∪ 𝑆)
→ 𝑆 ⊆ 𝒫
∪ 𝑆) |
34 | | pwssb 4986 |
. . . . . . . . . . . 12
⊢ (𝑆 ⊆ 𝒫 ∪ 𝑆
↔ ∀𝑎 ∈
𝑆 𝑎 ⊆ ∪ 𝑆) |
35 | 34 | biimpi 219 |
. . . . . . . . . . 11
⊢ (𝑆 ⊆ 𝒫 ∪ 𝑆
→ ∀𝑎 ∈
𝑆 𝑎 ⊆ ∪ 𝑆) |
36 | 2, 32, 33, 35 | 4syl 19 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑎 ∈ 𝑆 𝑎 ⊆ ∪ 𝑆) |
37 | 36 | r19.21bi 3121 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑎 ⊆ ∪ 𝑆) |
38 | | xpss1 5544 |
. . . . . . . . 9
⊢ (𝑎 ⊆ ∪ 𝑆
→ (𝑎 × ∪ 𝑇)
⊆ (∪ 𝑆 × ∪ 𝑇)) |
39 | 37, 38 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑎 × ∪ 𝑇) ⊆ (∪ 𝑆
× ∪ 𝑇)) |
40 | 39 | sseld 3876 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑧 ∈ (𝑎 × ∪ 𝑇) → 𝑧 ∈ (∪ 𝑆 × ∪ 𝑇))) |
41 | 40 | pm4.71rd 566 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑧 ∈ (𝑎 × ∪ 𝑇) ↔ (𝑧 ∈ (∪ 𝑆 × ∪ 𝑇)
∧ 𝑧 ∈ (𝑎 × ∪ 𝑇)))) |
42 | 31, 41 | bitr4id 293 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑧 ∈ (◡(1st ↾ (∪ 𝑆
× ∪ 𝑇)) “ 𝑎) ↔ 𝑧 ∈ (𝑎 × ∪ 𝑇))) |
43 | 42 | eqrdv 2736 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (◡(1st ↾ (∪ 𝑆
× ∪ 𝑇)) “ 𝑎) = (𝑎 × ∪ 𝑇)) |
44 | 2 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑆 ∈ ∪ ran
sigAlgebra) |
45 | 3 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑇 ∈ ∪ ran
sigAlgebra) |
46 | | simpr 488 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑎 ∈ 𝑆) |
47 | | eqid 2738 |
. . . . . . . 8
⊢ ∪ 𝑇 =
∪ 𝑇 |
48 | | issgon 31663 |
. . . . . . . 8
⊢ (𝑇 ∈ (sigAlgebra‘∪ 𝑇)
↔ (𝑇 ∈ ∪ ran sigAlgebra ∧ ∪ 𝑇 = ∪
𝑇)) |
49 | 3, 47, 48 | sylanblrc 593 |
. . . . . . 7
⊢ (𝜑 → 𝑇 ∈ (sigAlgebra‘∪ 𝑇)) |
50 | | baselsiga 31655 |
. . . . . . 7
⊢ (𝑇 ∈ (sigAlgebra‘∪ 𝑇)
→ ∪ 𝑇 ∈ 𝑇) |
51 | 49, 50 | syl 17 |
. . . . . 6
⊢ (𝜑 → ∪ 𝑇
∈ 𝑇) |
52 | 51 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → ∪ 𝑇 ∈ 𝑇) |
53 | | elsx 31734 |
. . . . 5
⊢ (((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑇 ∈ ∪ ran
sigAlgebra) ∧ (𝑎 ∈
𝑆 ∧ ∪ 𝑇
∈ 𝑇)) → (𝑎 × ∪ 𝑇)
∈ (𝑆
×s 𝑇)) |
54 | 44, 45, 46, 52, 53 | syl22anc 838 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑎 × ∪ 𝑇) ∈ (𝑆 ×s 𝑇)) |
55 | 43, 54 | eqeltrd 2833 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (◡(1st ↾ (∪ 𝑆
× ∪ 𝑇)) “ 𝑎) ∈ (𝑆 ×s 𝑇)) |
56 | 55 | ralrimiva 3096 |
. 2
⊢ (𝜑 → ∀𝑎 ∈ 𝑆 (◡(1st ↾ (∪ 𝑆
× ∪ 𝑇)) “ 𝑎) ∈ (𝑆 ×s 𝑇)) |
57 | 11, 2 | ismbfm 31791 |
. 2
⊢ (𝜑 → ((1st ↾
(∪ 𝑆 × ∪ 𝑇)) ∈ ((𝑆 ×s 𝑇)MblFnM𝑆) ↔ ((1st ↾ (∪ 𝑆
× ∪ 𝑇)) ∈ (∪
𝑆 ↑m ∪ (𝑆
×s 𝑇))
∧ ∀𝑎 ∈
𝑆 (◡(1st ↾ (∪ 𝑆
× ∪ 𝑇)) “ 𝑎) ∈ (𝑆 ×s 𝑇)))) |
58 | 15, 56, 57 | mpbir2and 713 |
1
⊢ (𝜑 → (1st ↾
(∪ 𝑆 × ∪ 𝑇)) ∈ ((𝑆 ×s 𝑇)MblFnM𝑆)) |