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