Step | Hyp | Ref
| Expression |
1 | | f2ndres 7999 |
. . . 4
β’
(2nd βΎ (βͺ π Γ βͺ π)):(βͺ
π Γ βͺ π)βΆβͺ π |
2 | | 1stmbfm.1 |
. . . . . 6
β’ (π β π β βͺ ran
sigAlgebra) |
3 | | 1stmbfm.2 |
. . . . . 6
β’ (π β π β βͺ ran
sigAlgebra) |
4 | | sxuni 33186 |
. . . . . 6
β’ ((π β βͺ ran sigAlgebra β§ π β βͺ ran
sigAlgebra) β (βͺ π Γ βͺ π) = βͺ
(π Γs
π)) |
5 | 2, 3, 4 | syl2anc 584 |
. . . . 5
β’ (π β (βͺ π
Γ βͺ π) = βͺ (π Γs π)) |
6 | 5 | feq2d 6703 |
. . . 4
β’ (π β ((2nd βΎ
(βͺ π Γ βͺ π)):(βͺ
π Γ βͺ π)βΆβͺ π β (2nd βΎ
(βͺ π Γ βͺ π)):βͺ
(π Γs
π)βΆβͺ π)) |
7 | 1, 6 | mpbii 232 |
. . 3
β’ (π β (2nd βΎ
(βͺ π Γ βͺ π)):βͺ
(π Γs
π)βΆβͺ π) |
8 | | unielsiga 33121 |
. . . . 5
β’ (π β βͺ ran sigAlgebra β βͺ π β π) |
9 | 3, 8 | syl 17 |
. . . 4
β’ (π β βͺ π
β π) |
10 | | sxsiga 33184 |
. . . . . 6
β’ ((π β βͺ ran sigAlgebra β§ π β βͺ ran
sigAlgebra) β (π
Γs π)
β βͺ ran sigAlgebra) |
11 | 2, 3, 10 | syl2anc 584 |
. . . . 5
β’ (π β (π Γs π) β βͺ ran
sigAlgebra) |
12 | | unielsiga 33121 |
. . . . 5
β’ ((π Γs π) β βͺ ran sigAlgebra β βͺ
(π Γs
π) β (π Γs π)) |
13 | 11, 12 | syl 17 |
. . . 4
β’ (π β βͺ (π
Γs π)
β (π
Γs π)) |
14 | 9, 13 | elmapd 8833 |
. . 3
β’ (π β ((2nd βΎ
(βͺ π Γ βͺ π)) β (βͺ π
βm βͺ (π Γs π)) β (2nd βΎ (βͺ π
Γ βͺ π)):βͺ (π Γs π)βΆβͺ π)) |
15 | 7, 14 | mpbird 256 |
. 2
β’ (π β (2nd βΎ
(βͺ π Γ βͺ π)) β (βͺ π
βm βͺ (π Γs π))) |
16 | | ffn 6717 |
. . . . . . . 8
β’
((2nd βΎ (βͺ π Γ βͺ π)):(βͺ
π Γ βͺ π)βΆβͺ π β (2nd βΎ
(βͺ π Γ βͺ π)) Fn (βͺ π
Γ βͺ π)) |
17 | | elpreima 7059 |
. . . . . . . 8
β’
((2nd βΎ (βͺ π Γ βͺ π)) Fn (βͺ π
Γ βͺ π) β (π§ β (β‘(2nd βΎ (βͺ π
Γ βͺ π)) β π) β (π§ β (βͺ π Γ βͺ π)
β§ ((2nd βΎ (βͺ π Γ βͺ π))βπ§) β π))) |
18 | 1, 16, 17 | mp2b 10 |
. . . . . . 7
β’ (π§ β (β‘(2nd βΎ (βͺ π
Γ βͺ π)) β π) β (π§ β (βͺ π Γ βͺ π)
β§ ((2nd βΎ (βͺ π Γ βͺ π))βπ§) β π)) |
19 | | fvres 6910 |
. . . . . . . . . 10
β’ (π§ β (βͺ π
Γ βͺ π) β ((2nd βΎ (βͺ π
Γ βͺ π))βπ§) = (2nd βπ§)) |
20 | 19 | eleq1d 2818 |
. . . . . . . . 9
β’ (π§ β (βͺ π
Γ βͺ π) β (((2nd βΎ (βͺ π
Γ βͺ π))βπ§) β π β (2nd βπ§) β π)) |
21 | | 1st2nd2 8013 |
. . . . . . . . . 10
β’ (π§ β (βͺ π
Γ βͺ π) β π§ = β¨(1st βπ§), (2nd βπ§)β©) |
22 | | xp1st 8006 |
. . . . . . . . . 10
β’ (π§ β (βͺ π
Γ βͺ π) β (1st βπ§) β βͺ π) |
23 | | elxp6 8008 |
. . . . . . . . . . . 12
β’ (π§ β (βͺ π
Γ π) β (π§ = β¨(1st
βπ§), (2nd
βπ§)β© β§
((1st βπ§)
β βͺ π β§ (2nd βπ§) β π))) |
24 | | anass 469 |
. . . . . . . . . . . 12
β’ (((π§ = β¨(1st
βπ§), (2nd
βπ§)β© β§
(1st βπ§)
β βͺ π) β§ (2nd βπ§) β π) β (π§ = β¨(1st βπ§), (2nd βπ§)β© β§ ((1st
βπ§) β βͺ π
β§ (2nd βπ§) β π))) |
25 | 23, 24 | bitr4i 277 |
. . . . . . . . . . 11
β’ (π§ β (βͺ π
Γ π) β ((π§ = β¨(1st
βπ§), (2nd
βπ§)β© β§
(1st βπ§)
β βͺ π) β§ (2nd βπ§) β π)) |
26 | 25 | baib 536 |
. . . . . . . . . 10
β’ ((π§ = β¨(1st
βπ§), (2nd
βπ§)β© β§
(1st βπ§)
β βͺ π) β (π§ β (βͺ π Γ π) β (2nd βπ§) β π)) |
27 | 21, 22, 26 | syl2anc 584 |
. . . . . . . . 9
β’ (π§ β (βͺ π
Γ βͺ π) β (π§ β (βͺ π Γ π) β (2nd βπ§) β π)) |
28 | 20, 27 | bitr4d 281 |
. . . . . . . 8
β’ (π§ β (βͺ π
Γ βͺ π) β (((2nd βΎ (βͺ π
Γ βͺ π))βπ§) β π β π§ β (βͺ π Γ π))) |
29 | 28 | pm5.32i 575 |
. . . . . . 7
β’ ((π§ β (βͺ π
Γ βͺ π) β§ ((2nd βΎ (βͺ π
Γ βͺ π))βπ§) β π) β (π§ β (βͺ π Γ βͺ π)
β§ π§ β (βͺ π
Γ π))) |
30 | 18, 29 | bitri 274 |
. . . . . 6
β’ (π§ β (β‘(2nd βΎ (βͺ π
Γ βͺ π)) β π) β (π§ β (βͺ π Γ βͺ π)
β§ π§ β (βͺ π
Γ π))) |
31 | | sgon 33117 |
. . . . . . . . . . 11
β’ (π β βͺ ran sigAlgebra β π β (sigAlgebraββͺ π)) |
32 | | sigasspw 33109 |
. . . . . . . . . . 11
β’ (π β (sigAlgebraββͺ π)
β π β π«
βͺ π) |
33 | | pwssb 5104 |
. . . . . . . . . . . 12
β’ (π β π« βͺ π
β βπ β
π π β βͺ π) |
34 | 33 | biimpi 215 |
. . . . . . . . . . 11
β’ (π β π« βͺ π
β βπ β
π π β βͺ π) |
35 | 3, 31, 32, 34 | 4syl 19 |
. . . . . . . . . 10
β’ (π β βπ β π π β βͺ π) |
36 | 35 | r19.21bi 3248 |
. . . . . . . . 9
β’ ((π β§ π β π) β π β βͺ π) |
37 | | xpss2 5696 |
. . . . . . . . 9
β’ (π β βͺ π
β (βͺ π Γ π) β (βͺ π Γ βͺ π)) |
38 | 36, 37 | syl 17 |
. . . . . . . 8
β’ ((π β§ π β π) β (βͺ π Γ π) β (βͺ π Γ βͺ π)) |
39 | 38 | sseld 3981 |
. . . . . . 7
β’ ((π β§ π β π) β (π§ β (βͺ π Γ π) β π§ β (βͺ π Γ βͺ π))) |
40 | 39 | pm4.71rd 563 |
. . . . . 6
β’ ((π β§ π β π) β (π§ β (βͺ π Γ π) β (π§ β (βͺ π Γ βͺ π)
β§ π§ β (βͺ π
Γ π)))) |
41 | 30, 40 | bitr4id 289 |
. . . . 5
β’ ((π β§ π β π) β (π§ β (β‘(2nd βΎ (βͺ π
Γ βͺ π)) β π) β π§ β (βͺ π Γ π))) |
42 | 41 | eqrdv 2730 |
. . . 4
β’ ((π β§ π β π) β (β‘(2nd βΎ (βͺ π
Γ βͺ π)) β π) = (βͺ π Γ π)) |
43 | 2 | adantr 481 |
. . . . 5
β’ ((π β§ π β π) β π β βͺ ran
sigAlgebra) |
44 | 3 | adantr 481 |
. . . . 5
β’ ((π β§ π β π) β π β βͺ ran
sigAlgebra) |
45 | | eqid 2732 |
. . . . . . . 8
β’ βͺ π =
βͺ π |
46 | | issgon 33116 |
. . . . . . . 8
β’ (π β (sigAlgebraββͺ π)
β (π β βͺ ran sigAlgebra β§ βͺ π = βͺ
π)) |
47 | 2, 45, 46 | sylanblrc 590 |
. . . . . . 7
β’ (π β π β (sigAlgebraββͺ π)) |
48 | | baselsiga 33108 |
. . . . . . 7
β’ (π β (sigAlgebraββͺ π)
β βͺ π β π) |
49 | 47, 48 | syl 17 |
. . . . . 6
β’ (π β βͺ π
β π) |
50 | 49 | adantr 481 |
. . . . 5
β’ ((π β§ π β π) β βͺ π β π) |
51 | | simpr 485 |
. . . . 5
β’ ((π β§ π β π) β π β π) |
52 | | elsx 33187 |
. . . . 5
β’ (((π β βͺ ran sigAlgebra β§ π β βͺ ran
sigAlgebra) β§ (βͺ π β π β§ π β π)) β (βͺ
π Γ π) β (π Γs π)) |
53 | 43, 44, 50, 51, 52 | syl22anc 837 |
. . . 4
β’ ((π β§ π β π) β (βͺ π Γ π) β (π Γs π)) |
54 | 42, 53 | eqeltrd 2833 |
. . 3
β’ ((π β§ π β π) β (β‘(2nd βΎ (βͺ π
Γ βͺ π)) β π) β (π Γs π)) |
55 | 54 | ralrimiva 3146 |
. 2
β’ (π β βπ β π (β‘(2nd βΎ (βͺ π
Γ βͺ π)) β π) β (π Γs π)) |
56 | 11, 3 | ismbfm 33244 |
. 2
β’ (π β ((2nd βΎ
(βͺ π Γ βͺ π)) β ((π Γs π)MblFnMπ) β ((2nd βΎ (βͺ π
Γ βͺ π)) β (βͺ
π βm βͺ (π
Γs π))
β§ βπ β
π (β‘(2nd βΎ (βͺ π
Γ βͺ π)) β π) β (π Γs π)))) |
57 | 15, 55, 56 | mpbir2and 711 |
1
β’ (π β (2nd βΎ
(βͺ π Γ βͺ π)) β ((π Γs π)MblFnMπ)) |