Step | Hyp | Ref
| Expression |
1 | | f2ndres 7950 |
. . . 4
β’
(2nd βΎ (βͺ π Γ βͺ π)):(βͺ
π Γ βͺ π)βΆβͺ π |
2 | | 1stmbfm.1 |
. . . . . 6
β’ (π β π β βͺ ran
sigAlgebra) |
3 | | 1stmbfm.2 |
. . . . . 6
β’ (π β π β βͺ ran
sigAlgebra) |
4 | | sxuni 32856 |
. . . . . 6
β’ ((π β βͺ ran sigAlgebra β§ π β βͺ ran
sigAlgebra) β (βͺ π Γ βͺ π) = βͺ
(π Γs
π)) |
5 | 2, 3, 4 | syl2anc 585 |
. . . . 5
β’ (π β (βͺ π
Γ βͺ π) = βͺ (π Γs π)) |
6 | 5 | feq2d 6658 |
. . . 4
β’ (π β ((2nd βΎ
(βͺ π Γ βͺ π)):(βͺ
π Γ βͺ π)βΆβͺ π β (2nd βΎ
(βͺ π Γ βͺ π)):βͺ
(π Γs
π)βΆβͺ π)) |
7 | 1, 6 | mpbii 232 |
. . 3
β’ (π β (2nd βΎ
(βͺ π Γ βͺ π)):βͺ
(π Γs
π)βΆβͺ π) |
8 | | unielsiga 32791 |
. . . . 5
β’ (π β βͺ ran sigAlgebra β βͺ π β π) |
9 | 3, 8 | syl 17 |
. . . 4
β’ (π β βͺ π
β π) |
10 | | sxsiga 32854 |
. . . . . 6
β’ ((π β βͺ ran sigAlgebra β§ π β βͺ ran
sigAlgebra) β (π
Γs π)
β βͺ ran sigAlgebra) |
11 | 2, 3, 10 | syl2anc 585 |
. . . . 5
β’ (π β (π Γs π) β βͺ ran
sigAlgebra) |
12 | | unielsiga 32791 |
. . . . 5
β’ ((π Γs π) β βͺ ran sigAlgebra β βͺ
(π Γs
π) β (π Γs π)) |
13 | 11, 12 | syl 17 |
. . . 4
β’ (π β βͺ (π
Γs π)
β (π
Γs π)) |
14 | 9, 13 | elmapd 8785 |
. . 3
β’ (π β ((2nd βΎ
(βͺ π Γ βͺ π)) β (βͺ π
βm βͺ (π Γs π)) β (2nd βΎ (βͺ π
Γ βͺ π)):βͺ (π Γs π)βΆβͺ π)) |
15 | 7, 14 | mpbird 257 |
. 2
β’ (π β (2nd βΎ
(βͺ π Γ βͺ π)) β (βͺ π
βm βͺ (π Γs π))) |
16 | | ffn 6672 |
. . . . . . . 8
β’
((2nd βΎ (βͺ π Γ βͺ π)):(βͺ
π Γ βͺ π)βΆβͺ π β (2nd βΎ
(βͺ π Γ βͺ π)) Fn (βͺ π
Γ βͺ π)) |
17 | | elpreima 7012 |
. . . . . . . 8
β’
((2nd βΎ (βͺ π Γ βͺ π)) Fn (βͺ π
Γ βͺ π) β (π§ β (β‘(2nd βΎ (βͺ π
Γ βͺ π)) β π) β (π§ β (βͺ π Γ βͺ π)
β§ ((2nd βΎ (βͺ π Γ βͺ π))βπ§) β π))) |
18 | 1, 16, 17 | mp2b 10 |
. . . . . . 7
β’ (π§ β (β‘(2nd βΎ (βͺ π
Γ βͺ π)) β π) β (π§ β (βͺ π Γ βͺ π)
β§ ((2nd βΎ (βͺ π Γ βͺ π))βπ§) β π)) |
19 | | fvres 6865 |
. . . . . . . . . 10
β’ (π§ β (βͺ π
Γ βͺ π) β ((2nd βΎ (βͺ π
Γ βͺ π))βπ§) = (2nd βπ§)) |
20 | 19 | eleq1d 2819 |
. . . . . . . . 9
β’ (π§ β (βͺ π
Γ βͺ π) β (((2nd βΎ (βͺ π
Γ βͺ π))βπ§) β π β (2nd βπ§) β π)) |
21 | | 1st2nd2 7964 |
. . . . . . . . . 10
β’ (π§ β (βͺ π
Γ βͺ π) β π§ = β¨(1st βπ§), (2nd βπ§)β©) |
22 | | xp1st 7957 |
. . . . . . . . . 10
β’ (π§ β (βͺ π
Γ βͺ π) β (1st βπ§) β βͺ π) |
23 | | elxp6 7959 |
. . . . . . . . . . . 12
β’ (π§ β (βͺ π
Γ π) β (π§ = β¨(1st
βπ§), (2nd
βπ§)β© β§
((1st βπ§)
β βͺ π β§ (2nd βπ§) β π))) |
24 | | anass 470 |
. . . . . . . . . . . 12
β’ (((π§ = β¨(1st
βπ§), (2nd
βπ§)β© β§
(1st βπ§)
β βͺ π) β§ (2nd βπ§) β π) β (π§ = β¨(1st βπ§), (2nd βπ§)β© β§ ((1st
βπ§) β βͺ π
β§ (2nd βπ§) β π))) |
25 | 23, 24 | bitr4i 278 |
. . . . . . . . . . 11
β’ (π§ β (βͺ π
Γ π) β ((π§ = β¨(1st
βπ§), (2nd
βπ§)β© β§
(1st βπ§)
β βͺ π) β§ (2nd βπ§) β π)) |
26 | 25 | baib 537 |
. . . . . . . . . 10
β’ ((π§ = β¨(1st
βπ§), (2nd
βπ§)β© β§
(1st βπ§)
β βͺ π) β (π§ β (βͺ π Γ π) β (2nd βπ§) β π)) |
27 | 21, 22, 26 | syl2anc 585 |
. . . . . . . . 9
β’ (π§ β (βͺ π
Γ βͺ π) β (π§ β (βͺ π Γ π) β (2nd βπ§) β π)) |
28 | 20, 27 | bitr4d 282 |
. . . . . . . 8
β’ (π§ β (βͺ π
Γ βͺ π) β (((2nd βΎ (βͺ π
Γ βͺ π))βπ§) β π β π§ β (βͺ π Γ π))) |
29 | 28 | pm5.32i 576 |
. . . . . . 7
β’ ((π§ β (βͺ π
Γ βͺ π) β§ ((2nd βΎ (βͺ π
Γ βͺ π))βπ§) β π) β (π§ β (βͺ π Γ βͺ π)
β§ π§ β (βͺ π
Γ π))) |
30 | 18, 29 | bitri 275 |
. . . . . 6
β’ (π§ β (β‘(2nd βΎ (βͺ π
Γ βͺ π)) β π) β (π§ β (βͺ π Γ βͺ π)
β§ π§ β (βͺ π
Γ π))) |
31 | | sgon 32787 |
. . . . . . . . . . 11
β’ (π β βͺ ran sigAlgebra β π β (sigAlgebraββͺ π)) |
32 | | sigasspw 32779 |
. . . . . . . . . . 11
β’ (π β (sigAlgebraββͺ π)
β π β π«
βͺ π) |
33 | | pwssb 5065 |
. . . . . . . . . . . 12
β’ (π β π« βͺ π
β βπ β
π π β βͺ π) |
34 | 33 | biimpi 215 |
. . . . . . . . . . 11
β’ (π β π« βͺ π
β βπ β
π π β βͺ π) |
35 | 3, 31, 32, 34 | 4syl 19 |
. . . . . . . . . 10
β’ (π β βπ β π π β βͺ π) |
36 | 35 | r19.21bi 3233 |
. . . . . . . . 9
β’ ((π β§ π β π) β π β βͺ π) |
37 | | xpss2 5657 |
. . . . . . . . 9
β’ (π β βͺ π
β (βͺ π Γ π) β (βͺ π Γ βͺ π)) |
38 | 36, 37 | syl 17 |
. . . . . . . 8
β’ ((π β§ π β π) β (βͺ π Γ π) β (βͺ π Γ βͺ π)) |
39 | 38 | sseld 3947 |
. . . . . . 7
β’ ((π β§ π β π) β (π§ β (βͺ π Γ π) β π§ β (βͺ π Γ βͺ π))) |
40 | 39 | pm4.71rd 564 |
. . . . . 6
β’ ((π β§ π β π) β (π§ β (βͺ π Γ π) β (π§ β (βͺ π Γ βͺ π)
β§ π§ β (βͺ π
Γ π)))) |
41 | 30, 40 | bitr4id 290 |
. . . . 5
β’ ((π β§ π β π) β (π§ β (β‘(2nd βΎ (βͺ π
Γ βͺ π)) β π) β π§ β (βͺ π Γ π))) |
42 | 41 | eqrdv 2731 |
. . . 4
β’ ((π β§ π β π) β (β‘(2nd βΎ (βͺ π
Γ βͺ π)) β π) = (βͺ π Γ π)) |
43 | 2 | adantr 482 |
. . . . 5
β’ ((π β§ π β π) β π β βͺ ran
sigAlgebra) |
44 | 3 | adantr 482 |
. . . . 5
β’ ((π β§ π β π) β π β βͺ ran
sigAlgebra) |
45 | | eqid 2733 |
. . . . . . . 8
β’ βͺ π =
βͺ π |
46 | | issgon 32786 |
. . . . . . . 8
β’ (π β (sigAlgebraββͺ π)
β (π β βͺ ran sigAlgebra β§ βͺ π = βͺ
π)) |
47 | 2, 45, 46 | sylanblrc 591 |
. . . . . . 7
β’ (π β π β (sigAlgebraββͺ π)) |
48 | | baselsiga 32778 |
. . . . . . 7
β’ (π β (sigAlgebraββͺ π)
β βͺ π β π) |
49 | 47, 48 | syl 17 |
. . . . . 6
β’ (π β βͺ π
β π) |
50 | 49 | adantr 482 |
. . . . 5
β’ ((π β§ π β π) β βͺ π β π) |
51 | | simpr 486 |
. . . . 5
β’ ((π β§ π β π) β π β π) |
52 | | elsx 32857 |
. . . . 5
β’ (((π β βͺ ran sigAlgebra β§ π β βͺ ran
sigAlgebra) β§ (βͺ π β π β§ π β π)) β (βͺ
π Γ π) β (π Γs π)) |
53 | 43, 44, 50, 51, 52 | syl22anc 838 |
. . . 4
β’ ((π β§ π β π) β (βͺ π Γ π) β (π Γs π)) |
54 | 42, 53 | eqeltrd 2834 |
. . 3
β’ ((π β§ π β π) β (β‘(2nd βΎ (βͺ π
Γ βͺ π)) β π) β (π Γs π)) |
55 | 54 | ralrimiva 3140 |
. 2
β’ (π β βπ β π (β‘(2nd βΎ (βͺ π
Γ βͺ π)) β π) β (π Γs π)) |
56 | 11, 3 | ismbfm 32914 |
. 2
β’ (π β ((2nd βΎ
(βͺ π Γ βͺ π)) β ((π Γs π)MblFnMπ) β ((2nd βΎ (βͺ π
Γ βͺ π)) β (βͺ
π βm βͺ (π
Γs π))
β§ βπ β
π (β‘(2nd βΎ (βͺ π
Γ βͺ π)) β π) β (π Γs π)))) |
57 | 15, 55, 56 | mpbir2and 712 |
1
β’ (π β (2nd βΎ
(βͺ π Γ βͺ π)) β ((π Γs π)MblFnMπ)) |