Step | Hyp | Ref
| Expression |
1 | | f1stres 7457 |
. . . 4
⊢
(1st ↾ (∪ 𝑆 × ∪ 𝑇)):(∪
𝑆 × ∪ 𝑇)⟶∪ 𝑆 |
2 | | 1stmbfm.1 |
. . . . . 6
⊢ (𝜑 → 𝑆 ∈ ∪ ran
sigAlgebra) |
3 | | 1stmbfm.2 |
. . . . . 6
⊢ (𝜑 → 𝑇 ∈ ∪ ran
sigAlgebra) |
4 | | sxuni 30797 |
. . . . . 6
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑇 ∈ ∪ ran
sigAlgebra) → (∪ 𝑆 × ∪ 𝑇) = ∪
(𝑆 ×s
𝑇)) |
5 | 2, 3, 4 | syl2anc 579 |
. . . . 5
⊢ (𝜑 → (∪ 𝑆
× ∪ 𝑇) = ∪ (𝑆 ×s 𝑇)) |
6 | 5 | feq2d 6268 |
. . . 4
⊢ (𝜑 → ((1st ↾
(∪ 𝑆 × ∪ 𝑇)):(∪
𝑆 × ∪ 𝑇)⟶∪ 𝑆 ↔ (1st ↾
(∪ 𝑆 × ∪ 𝑇)):∪
(𝑆 ×s
𝑇)⟶∪ 𝑆)) |
7 | 1, 6 | mpbii 225 |
. . 3
⊢ (𝜑 → (1st ↾
(∪ 𝑆 × ∪ 𝑇)):∪
(𝑆 ×s
𝑇)⟶∪ 𝑆) |
8 | | unielsiga 30732 |
. . . . 5
⊢ (𝑆 ∈ ∪ ran sigAlgebra → ∪ 𝑆 ∈ 𝑆) |
9 | 2, 8 | syl 17 |
. . . 4
⊢ (𝜑 → ∪ 𝑆
∈ 𝑆) |
10 | | sxsiga 30795 |
. . . . . 6
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑇 ∈ ∪ ran
sigAlgebra) → (𝑆
×s 𝑇)
∈ ∪ ran sigAlgebra) |
11 | 2, 3, 10 | syl2anc 579 |
. . . . 5
⊢ (𝜑 → (𝑆 ×s 𝑇) ∈ ∪ ran
sigAlgebra) |
12 | | unielsiga 30732 |
. . . . 5
⊢ ((𝑆 ×s 𝑇) ∈ ∪ ran sigAlgebra → ∪
(𝑆 ×s
𝑇) ∈ (𝑆 ×s 𝑇)) |
13 | 11, 12 | syl 17 |
. . . 4
⊢ (𝜑 → ∪ (𝑆
×s 𝑇)
∈ (𝑆
×s 𝑇)) |
14 | 9, 13 | elmapd 8141 |
. . 3
⊢ (𝜑 → ((1st ↾
(∪ 𝑆 × ∪ 𝑇)) ∈ (∪ 𝑆
↑𝑚 ∪ (𝑆 ×s 𝑇)) ↔ (1st ↾ (∪ 𝑆
× ∪ 𝑇)):∪ (𝑆 ×s 𝑇)⟶∪ 𝑆)) |
15 | 7, 14 | mpbird 249 |
. 2
⊢ (𝜑 → (1st ↾
(∪ 𝑆 × ∪ 𝑇)) ∈ (∪ 𝑆
↑𝑚 ∪ (𝑆 ×s 𝑇))) |
16 | | sgon 30728 |
. . . . . . . . . . 11
⊢ (𝑆 ∈ ∪ ran sigAlgebra → 𝑆 ∈ (sigAlgebra‘∪ 𝑆)) |
17 | | sigasspw 30720 |
. . . . . . . . . . 11
⊢ (𝑆 ∈ (sigAlgebra‘∪ 𝑆)
→ 𝑆 ⊆ 𝒫
∪ 𝑆) |
18 | | pwssb 4835 |
. . . . . . . . . . . 12
⊢ (𝑆 ⊆ 𝒫 ∪ 𝑆
↔ ∀𝑎 ∈
𝑆 𝑎 ⊆ ∪ 𝑆) |
19 | 18 | biimpi 208 |
. . . . . . . . . . 11
⊢ (𝑆 ⊆ 𝒫 ∪ 𝑆
→ ∀𝑎 ∈
𝑆 𝑎 ⊆ ∪ 𝑆) |
20 | 2, 16, 17, 19 | 4syl 19 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑎 ∈ 𝑆 𝑎 ⊆ ∪ 𝑆) |
21 | 20 | r19.21bi 3141 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑎 ⊆ ∪ 𝑆) |
22 | | xpss1 5365 |
. . . . . . . . 9
⊢ (𝑎 ⊆ ∪ 𝑆
→ (𝑎 × ∪ 𝑇)
⊆ (∪ 𝑆 × ∪ 𝑇)) |
23 | 21, 22 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑎 × ∪ 𝑇) ⊆ (∪ 𝑆
× ∪ 𝑇)) |
24 | 23 | sseld 3826 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑧 ∈ (𝑎 × ∪ 𝑇) → 𝑧 ∈ (∪ 𝑆 × ∪ 𝑇))) |
25 | 24 | pm4.71rd 558 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑧 ∈ (𝑎 × ∪ 𝑇) ↔ (𝑧 ∈ (∪ 𝑆 × ∪ 𝑇)
∧ 𝑧 ∈ (𝑎 × ∪ 𝑇)))) |
26 | | ffn 6282 |
. . . . . . . 8
⊢
((1st ↾ (∪ 𝑆 × ∪ 𝑇)):(∪
𝑆 × ∪ 𝑇)⟶∪ 𝑆 → (1st ↾
(∪ 𝑆 × ∪ 𝑇)) Fn (∪ 𝑆
× ∪ 𝑇)) |
27 | | elpreima 6591 |
. . . . . . . 8
⊢
((1st ↾ (∪ 𝑆 × ∪ 𝑇)) Fn (∪ 𝑆
× ∪ 𝑇) → (𝑧 ∈ (◡(1st ↾ (∪ 𝑆
× ∪ 𝑇)) “ 𝑎) ↔ (𝑧 ∈ (∪ 𝑆 × ∪ 𝑇)
∧ ((1st ↾ (∪ 𝑆 × ∪ 𝑇))‘𝑧) ∈ 𝑎))) |
28 | 1, 26, 27 | mp2b 10 |
. . . . . . 7
⊢ (𝑧 ∈ (◡(1st ↾ (∪ 𝑆
× ∪ 𝑇)) “ 𝑎) ↔ (𝑧 ∈ (∪ 𝑆 × ∪ 𝑇)
∧ ((1st ↾ (∪ 𝑆 × ∪ 𝑇))‘𝑧) ∈ 𝑎)) |
29 | | fvres 6456 |
. . . . . . . . . 10
⊢ (𝑧 ∈ (∪ 𝑆
× ∪ 𝑇) → ((1st ↾ (∪ 𝑆
× ∪ 𝑇))‘𝑧) = (1st ‘𝑧)) |
30 | 29 | eleq1d 2891 |
. . . . . . . . 9
⊢ (𝑧 ∈ (∪ 𝑆
× ∪ 𝑇) → (((1st ↾ (∪ 𝑆
× ∪ 𝑇))‘𝑧) ∈ 𝑎 ↔ (1st ‘𝑧) ∈ 𝑎)) |
31 | | 1st2nd2 7472 |
. . . . . . . . . 10
⊢ (𝑧 ∈ (∪ 𝑆
× ∪ 𝑇) → 𝑧 = 〈(1st ‘𝑧), (2nd ‘𝑧)〉) |
32 | | xp2nd 7466 |
. . . . . . . . . 10
⊢ (𝑧 ∈ (∪ 𝑆
× ∪ 𝑇) → (2nd ‘𝑧) ∈ ∪ 𝑇) |
33 | | elxp6 7467 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ (𝑎 × ∪ 𝑇) ↔ (𝑧 = 〈(1st ‘𝑧), (2nd ‘𝑧)〉 ∧ ((1st
‘𝑧) ∈ 𝑎 ∧ (2nd
‘𝑧) ∈ ∪ 𝑇))) |
34 | | anass 462 |
. . . . . . . . . . . 12
⊢ (((𝑧 = 〈(1st
‘𝑧), (2nd
‘𝑧)〉 ∧
(1st ‘𝑧)
∈ 𝑎) ∧
(2nd ‘𝑧)
∈ ∪ 𝑇) ↔ (𝑧 = 〈(1st ‘𝑧), (2nd ‘𝑧)〉 ∧ ((1st
‘𝑧) ∈ 𝑎 ∧ (2nd
‘𝑧) ∈ ∪ 𝑇))) |
35 | | an32 636 |
. . . . . . . . . . . 12
⊢ (((𝑧 = 〈(1st
‘𝑧), (2nd
‘𝑧)〉 ∧
(1st ‘𝑧)
∈ 𝑎) ∧
(2nd ‘𝑧)
∈ ∪ 𝑇) ↔ ((𝑧 = 〈(1st ‘𝑧), (2nd ‘𝑧)〉 ∧ (2nd
‘𝑧) ∈ ∪ 𝑇)
∧ (1st ‘𝑧) ∈ 𝑎)) |
36 | 33, 34, 35 | 3bitr2i 291 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ (𝑎 × ∪ 𝑇) ↔ ((𝑧 = 〈(1st ‘𝑧), (2nd ‘𝑧)〉 ∧ (2nd
‘𝑧) ∈ ∪ 𝑇)
∧ (1st ‘𝑧) ∈ 𝑎)) |
37 | 36 | baib 531 |
. . . . . . . . . 10
⊢ ((𝑧 = 〈(1st
‘𝑧), (2nd
‘𝑧)〉 ∧
(2nd ‘𝑧)
∈ ∪ 𝑇) → (𝑧 ∈ (𝑎 × ∪ 𝑇) ↔ (1st
‘𝑧) ∈ 𝑎)) |
38 | 31, 32, 37 | syl2anc 579 |
. . . . . . . . 9
⊢ (𝑧 ∈ (∪ 𝑆
× ∪ 𝑇) → (𝑧 ∈ (𝑎 × ∪ 𝑇) ↔ (1st
‘𝑧) ∈ 𝑎)) |
39 | 30, 38 | bitr4d 274 |
. . . . . . . 8
⊢ (𝑧 ∈ (∪ 𝑆
× ∪ 𝑇) → (((1st ↾ (∪ 𝑆
× ∪ 𝑇))‘𝑧) ∈ 𝑎 ↔ 𝑧 ∈ (𝑎 × ∪ 𝑇))) |
40 | 39 | pm5.32i 570 |
. . . . . . 7
⊢ ((𝑧 ∈ (∪ 𝑆
× ∪ 𝑇) ∧ ((1st ↾ (∪ 𝑆
× ∪ 𝑇))‘𝑧) ∈ 𝑎) ↔ (𝑧 ∈ (∪ 𝑆 × ∪ 𝑇)
∧ 𝑧 ∈ (𝑎 × ∪ 𝑇))) |
41 | 28, 40 | bitri 267 |
. . . . . 6
⊢ (𝑧 ∈ (◡(1st ↾ (∪ 𝑆
× ∪ 𝑇)) “ 𝑎) ↔ (𝑧 ∈ (∪ 𝑆 × ∪ 𝑇)
∧ 𝑧 ∈ (𝑎 × ∪ 𝑇))) |
42 | 25, 41 | syl6rbbr 282 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑧 ∈ (◡(1st ↾ (∪ 𝑆
× ∪ 𝑇)) “ 𝑎) ↔ 𝑧 ∈ (𝑎 × ∪ 𝑇))) |
43 | 42 | eqrdv 2823 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (◡(1st ↾ (∪ 𝑆
× ∪ 𝑇)) “ 𝑎) = (𝑎 × ∪ 𝑇)) |
44 | 2 | adantr 474 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑆 ∈ ∪ ran
sigAlgebra) |
45 | 3 | adantr 474 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑇 ∈ ∪ ran
sigAlgebra) |
46 | | simpr 479 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑎 ∈ 𝑆) |
47 | | eqid 2825 |
. . . . . . . 8
⊢ ∪ 𝑇 =
∪ 𝑇 |
48 | | issgon 30727 |
. . . . . . . 8
⊢ (𝑇 ∈ (sigAlgebra‘∪ 𝑇)
↔ (𝑇 ∈ ∪ ran sigAlgebra ∧ ∪ 𝑇 = ∪
𝑇)) |
49 | 3, 47, 48 | sylanblrc 584 |
. . . . . . 7
⊢ (𝜑 → 𝑇 ∈ (sigAlgebra‘∪ 𝑇)) |
50 | | baselsiga 30719 |
. . . . . . 7
⊢ (𝑇 ∈ (sigAlgebra‘∪ 𝑇)
→ ∪ 𝑇 ∈ 𝑇) |
51 | 49, 50 | syl 17 |
. . . . . 6
⊢ (𝜑 → ∪ 𝑇
∈ 𝑇) |
52 | 51 | adantr 474 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → ∪ 𝑇 ∈ 𝑇) |
53 | | elsx 30798 |
. . . . 5
⊢ (((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑇 ∈ ∪ ran
sigAlgebra) ∧ (𝑎 ∈
𝑆 ∧ ∪ 𝑇
∈ 𝑇)) → (𝑎 × ∪ 𝑇)
∈ (𝑆
×s 𝑇)) |
54 | 44, 45, 46, 52, 53 | syl22anc 872 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑎 × ∪ 𝑇) ∈ (𝑆 ×s 𝑇)) |
55 | 43, 54 | eqeltrd 2906 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (◡(1st ↾ (∪ 𝑆
× ∪ 𝑇)) “ 𝑎) ∈ (𝑆 ×s 𝑇)) |
56 | 55 | ralrimiva 3175 |
. 2
⊢ (𝜑 → ∀𝑎 ∈ 𝑆 (◡(1st ↾ (∪ 𝑆
× ∪ 𝑇)) “ 𝑎) ∈ (𝑆 ×s 𝑇)) |
57 | 11, 2 | ismbfm 30855 |
. 2
⊢ (𝜑 → ((1st ↾
(∪ 𝑆 × ∪ 𝑇)) ∈ ((𝑆 ×s 𝑇)MblFnM𝑆) ↔ ((1st ↾ (∪ 𝑆
× ∪ 𝑇)) ∈ (∪
𝑆
↑𝑚 ∪ (𝑆 ×s 𝑇)) ∧ ∀𝑎 ∈ 𝑆 (◡(1st ↾ (∪ 𝑆
× ∪ 𝑇)) “ 𝑎) ∈ (𝑆 ×s 𝑇)))) |
58 | 15, 56, 57 | mpbir2and 704 |
1
⊢ (𝜑 → (1st ↾
(∪ 𝑆 × ∪ 𝑇)) ∈ ((𝑆 ×s 𝑇)MblFnM𝑆)) |