Step | Hyp | Ref
| Expression |
1 | | f1stres 7081 |
. . . 4
⊢
(1st ↾ (∪ 𝑆 × ∪ 𝑇)):(∪
𝑆 × ∪ 𝑇)⟶∪ 𝑆 |
2 | | 1stmbfm.1 |
. . . . . 6
⊢ (𝜑 → 𝑆 ∈ ∪ ran
sigAlgebra) |
3 | | 1stmbfm.2 |
. . . . . 6
⊢ (𝜑 → 𝑇 ∈ ∪ ran
sigAlgebra) |
4 | | sxuni 29583 |
. . . . . 6
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑇 ∈ ∪ ran
sigAlgebra) → (∪ 𝑆 × ∪ 𝑇) = ∪
(𝑆 ×s
𝑇)) |
5 | 2, 3, 4 | syl2anc 691 |
. . . . 5
⊢ (𝜑 → (∪ 𝑆
× ∪ 𝑇) = ∪ (𝑆 ×s 𝑇)) |
6 | 5 | feq2d 5944 |
. . . 4
⊢ (𝜑 → ((1st ↾
(∪ 𝑆 × ∪ 𝑇)):(∪
𝑆 × ∪ 𝑇)⟶∪ 𝑆 ↔ (1st ↾
(∪ 𝑆 × ∪ 𝑇)):∪
(𝑆 ×s
𝑇)⟶∪ 𝑆)) |
7 | 1, 6 | mpbii 222 |
. . 3
⊢ (𝜑 → (1st ↾
(∪ 𝑆 × ∪ 𝑇)):∪
(𝑆 ×s
𝑇)⟶∪ 𝑆) |
8 | | unielsiga 29518 |
. . . . 5
⊢ (𝑆 ∈ ∪ ran sigAlgebra → ∪ 𝑆 ∈ 𝑆) |
9 | 2, 8 | syl 17 |
. . . 4
⊢ (𝜑 → ∪ 𝑆
∈ 𝑆) |
10 | | sxsiga 29581 |
. . . . . 6
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑇 ∈ ∪ ran
sigAlgebra) → (𝑆
×s 𝑇)
∈ ∪ ran sigAlgebra) |
11 | 2, 3, 10 | syl2anc 691 |
. . . . 5
⊢ (𝜑 → (𝑆 ×s 𝑇) ∈ ∪ ran
sigAlgebra) |
12 | | unielsiga 29518 |
. . . . 5
⊢ ((𝑆 ×s 𝑇) ∈ ∪ ran sigAlgebra → ∪
(𝑆 ×s
𝑇) ∈ (𝑆 ×s 𝑇)) |
13 | 11, 12 | syl 17 |
. . . 4
⊢ (𝜑 → ∪ (𝑆
×s 𝑇)
∈ (𝑆
×s 𝑇)) |
14 | 9, 13 | elmapd 7758 |
. . 3
⊢ (𝜑 → ((1st ↾
(∪ 𝑆 × ∪ 𝑇)) ∈ (∪ 𝑆
↑𝑚 ∪ (𝑆 ×s 𝑇)) ↔ (1st ↾ (∪ 𝑆
× ∪ 𝑇)):∪ (𝑆 ×s 𝑇)⟶∪ 𝑆)) |
15 | 7, 14 | mpbird 246 |
. 2
⊢ (𝜑 → (1st ↾
(∪ 𝑆 × ∪ 𝑇)) ∈ (∪ 𝑆
↑𝑚 ∪ (𝑆 ×s 𝑇))) |
16 | | sgon 29514 |
. . . . . . . . . . 11
⊢ (𝑆 ∈ ∪ ran sigAlgebra → 𝑆 ∈ (sigAlgebra‘∪ 𝑆)) |
17 | | sigasspw 29506 |
. . . . . . . . . . 11
⊢ (𝑆 ∈ (sigAlgebra‘∪ 𝑆)
→ 𝑆 ⊆ 𝒫
∪ 𝑆) |
18 | | pwssb 4548 |
. . . . . . . . . . . 12
⊢ (𝑆 ⊆ 𝒫 ∪ 𝑆
↔ ∀𝑎 ∈
𝑆 𝑎 ⊆ ∪ 𝑆) |
19 | 18 | biimpi 205 |
. . . . . . . . . . 11
⊢ (𝑆 ⊆ 𝒫 ∪ 𝑆
→ ∀𝑎 ∈
𝑆 𝑎 ⊆ ∪ 𝑆) |
20 | 2, 16, 17, 19 | 4syl 19 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑎 ∈ 𝑆 𝑎 ⊆ ∪ 𝑆) |
21 | 20 | r19.21bi 2916 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑎 ⊆ ∪ 𝑆) |
22 | | xpss1 5151 |
. . . . . . . . 9
⊢ (𝑎 ⊆ ∪ 𝑆
→ (𝑎 × ∪ 𝑇)
⊆ (∪ 𝑆 × ∪ 𝑇)) |
23 | 21, 22 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑎 × ∪ 𝑇) ⊆ (∪ 𝑆
× ∪ 𝑇)) |
24 | 23 | sseld 3567 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑧 ∈ (𝑎 × ∪ 𝑇) → 𝑧 ∈ (∪ 𝑆 × ∪ 𝑇))) |
25 | 24 | pm4.71rd 665 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑧 ∈ (𝑎 × ∪ 𝑇) ↔ (𝑧 ∈ (∪ 𝑆 × ∪ 𝑇)
∧ 𝑧 ∈ (𝑎 × ∪ 𝑇)))) |
26 | | ffn 5958 |
. . . . . . . 8
⊢
((1st ↾ (∪ 𝑆 × ∪ 𝑇)):(∪
𝑆 × ∪ 𝑇)⟶∪ 𝑆 → (1st ↾
(∪ 𝑆 × ∪ 𝑇)) Fn (∪ 𝑆
× ∪ 𝑇)) |
27 | | elpreima 6245 |
. . . . . . . 8
⊢
((1st ↾ (∪ 𝑆 × ∪ 𝑇)) Fn (∪ 𝑆
× ∪ 𝑇) → (𝑧 ∈ (◡(1st ↾ (∪ 𝑆
× ∪ 𝑇)) “ 𝑎) ↔ (𝑧 ∈ (∪ 𝑆 × ∪ 𝑇)
∧ ((1st ↾ (∪ 𝑆 × ∪ 𝑇))‘𝑧) ∈ 𝑎))) |
28 | 1, 26, 27 | mp2b 10 |
. . . . . . 7
⊢ (𝑧 ∈ (◡(1st ↾ (∪ 𝑆
× ∪ 𝑇)) “ 𝑎) ↔ (𝑧 ∈ (∪ 𝑆 × ∪ 𝑇)
∧ ((1st ↾ (∪ 𝑆 × ∪ 𝑇))‘𝑧) ∈ 𝑎)) |
29 | | fvres 6117 |
. . . . . . . . . 10
⊢ (𝑧 ∈ (∪ 𝑆
× ∪ 𝑇) → ((1st ↾ (∪ 𝑆
× ∪ 𝑇))‘𝑧) = (1st ‘𝑧)) |
30 | 29 | eleq1d 2672 |
. . . . . . . . 9
⊢ (𝑧 ∈ (∪ 𝑆
× ∪ 𝑇) → (((1st ↾ (∪ 𝑆
× ∪ 𝑇))‘𝑧) ∈ 𝑎 ↔ (1st ‘𝑧) ∈ 𝑎)) |
31 | | 1st2nd2 7096 |
. . . . . . . . . 10
⊢ (𝑧 ∈ (∪ 𝑆
× ∪ 𝑇) → 𝑧 = 〈(1st ‘𝑧), (2nd ‘𝑧)〉) |
32 | | xp2nd 7090 |
. . . . . . . . . 10
⊢ (𝑧 ∈ (∪ 𝑆
× ∪ 𝑇) → (2nd ‘𝑧) ∈ ∪ 𝑇) |
33 | | elxp6 7091 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ (𝑎 × ∪ 𝑇) ↔ (𝑧 = 〈(1st ‘𝑧), (2nd ‘𝑧)〉 ∧ ((1st
‘𝑧) ∈ 𝑎 ∧ (2nd
‘𝑧) ∈ ∪ 𝑇))) |
34 | | anass 679 |
. . . . . . . . . . . 12
⊢ (((𝑧 = 〈(1st
‘𝑧), (2nd
‘𝑧)〉 ∧
(1st ‘𝑧)
∈ 𝑎) ∧
(2nd ‘𝑧)
∈ ∪ 𝑇) ↔ (𝑧 = 〈(1st ‘𝑧), (2nd ‘𝑧)〉 ∧ ((1st
‘𝑧) ∈ 𝑎 ∧ (2nd
‘𝑧) ∈ ∪ 𝑇))) |
35 | | an32 835 |
. . . . . . . . . . . 12
⊢ (((𝑧 = 〈(1st
‘𝑧), (2nd
‘𝑧)〉 ∧
(1st ‘𝑧)
∈ 𝑎) ∧
(2nd ‘𝑧)
∈ ∪ 𝑇) ↔ ((𝑧 = 〈(1st ‘𝑧), (2nd ‘𝑧)〉 ∧ (2nd
‘𝑧) ∈ ∪ 𝑇)
∧ (1st ‘𝑧) ∈ 𝑎)) |
36 | 33, 34, 35 | 3bitr2i 287 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ (𝑎 × ∪ 𝑇) ↔ ((𝑧 = 〈(1st ‘𝑧), (2nd ‘𝑧)〉 ∧ (2nd
‘𝑧) ∈ ∪ 𝑇)
∧ (1st ‘𝑧) ∈ 𝑎)) |
37 | 36 | baib 942 |
. . . . . . . . . 10
⊢ ((𝑧 = 〈(1st
‘𝑧), (2nd
‘𝑧)〉 ∧
(2nd ‘𝑧)
∈ ∪ 𝑇) → (𝑧 ∈ (𝑎 × ∪ 𝑇) ↔ (1st
‘𝑧) ∈ 𝑎)) |
38 | 31, 32, 37 | syl2anc 691 |
. . . . . . . . 9
⊢ (𝑧 ∈ (∪ 𝑆
× ∪ 𝑇) → (𝑧 ∈ (𝑎 × ∪ 𝑇) ↔ (1st
‘𝑧) ∈ 𝑎)) |
39 | 30, 38 | bitr4d 270 |
. . . . . . . 8
⊢ (𝑧 ∈ (∪ 𝑆
× ∪ 𝑇) → (((1st ↾ (∪ 𝑆
× ∪ 𝑇))‘𝑧) ∈ 𝑎 ↔ 𝑧 ∈ (𝑎 × ∪ 𝑇))) |
40 | 39 | pm5.32i 667 |
. . . . . . 7
⊢ ((𝑧 ∈ (∪ 𝑆
× ∪ 𝑇) ∧ ((1st ↾ (∪ 𝑆
× ∪ 𝑇))‘𝑧) ∈ 𝑎) ↔ (𝑧 ∈ (∪ 𝑆 × ∪ 𝑇)
∧ 𝑧 ∈ (𝑎 × ∪ 𝑇))) |
41 | 28, 40 | bitri 263 |
. . . . . 6
⊢ (𝑧 ∈ (◡(1st ↾ (∪ 𝑆
× ∪ 𝑇)) “ 𝑎) ↔ (𝑧 ∈ (∪ 𝑆 × ∪ 𝑇)
∧ 𝑧 ∈ (𝑎 × ∪ 𝑇))) |
42 | 25, 41 | syl6rbbr 278 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑧 ∈ (◡(1st ↾ (∪ 𝑆
× ∪ 𝑇)) “ 𝑎) ↔ 𝑧 ∈ (𝑎 × ∪ 𝑇))) |
43 | 42 | eqrdv 2608 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (◡(1st ↾ (∪ 𝑆
× ∪ 𝑇)) “ 𝑎) = (𝑎 × ∪ 𝑇)) |
44 | 2 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑆 ∈ ∪ ran
sigAlgebra) |
45 | 3 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑇 ∈ ∪ ran
sigAlgebra) |
46 | | simpr 476 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑎 ∈ 𝑆) |
47 | | eqid 2610 |
. . . . . . . 8
⊢ ∪ 𝑇 =
∪ 𝑇 |
48 | | issgon 29513 |
. . . . . . . . 9
⊢ (𝑇 ∈ (sigAlgebra‘∪ 𝑇)
↔ (𝑇 ∈ ∪ ran sigAlgebra ∧ ∪ 𝑇 = ∪
𝑇)) |
49 | 48 | biimpri 217 |
. . . . . . . 8
⊢ ((𝑇 ∈ ∪ ran sigAlgebra ∧ ∪ 𝑇 = ∪
𝑇) → 𝑇 ∈ (sigAlgebra‘∪ 𝑇)) |
50 | 3, 47, 49 | sylancl 693 |
. . . . . . 7
⊢ (𝜑 → 𝑇 ∈ (sigAlgebra‘∪ 𝑇)) |
51 | | baselsiga 29505 |
. . . . . . 7
⊢ (𝑇 ∈ (sigAlgebra‘∪ 𝑇)
→ ∪ 𝑇 ∈ 𝑇) |
52 | 50, 51 | syl 17 |
. . . . . 6
⊢ (𝜑 → ∪ 𝑇
∈ 𝑇) |
53 | 52 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → ∪ 𝑇 ∈ 𝑇) |
54 | | elsx 29584 |
. . . . 5
⊢ (((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑇 ∈ ∪ ran
sigAlgebra) ∧ (𝑎 ∈
𝑆 ∧ ∪ 𝑇
∈ 𝑇)) → (𝑎 × ∪ 𝑇)
∈ (𝑆
×s 𝑇)) |
55 | 44, 45, 46, 53, 54 | syl22anc 1319 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑎 × ∪ 𝑇) ∈ (𝑆 ×s 𝑇)) |
56 | 43, 55 | eqeltrd 2688 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (◡(1st ↾ (∪ 𝑆
× ∪ 𝑇)) “ 𝑎) ∈ (𝑆 ×s 𝑇)) |
57 | 56 | ralrimiva 2949 |
. 2
⊢ (𝜑 → ∀𝑎 ∈ 𝑆 (◡(1st ↾ (∪ 𝑆
× ∪ 𝑇)) “ 𝑎) ∈ (𝑆 ×s 𝑇)) |
58 | 11, 2 | ismbfm 29641 |
. 2
⊢ (𝜑 → ((1st ↾
(∪ 𝑆 × ∪ 𝑇)) ∈ ((𝑆 ×s 𝑇)MblFnM𝑆) ↔ ((1st ↾ (∪ 𝑆
× ∪ 𝑇)) ∈ (∪
𝑆
↑𝑚 ∪ (𝑆 ×s 𝑇)) ∧ ∀𝑎 ∈ 𝑆 (◡(1st ↾ (∪ 𝑆
× ∪ 𝑇)) “ 𝑎) ∈ (𝑆 ×s 𝑇)))) |
59 | 15, 57, 58 | mpbir2and 959 |
1
⊢ (𝜑 → (1st ↾
(∪ 𝑆 × ∪ 𝑇)) ∈ ((𝑆 ×s 𝑇)MblFnM𝑆)) |