Step | Hyp | Ref
| Expression |
1 | | f1stres 7950 |
. . . 4
β’
(1st βΎ (βͺ π Γ βͺ π)):(βͺ
π Γ βͺ π)βΆβͺ π |
2 | | 1stmbfm.1 |
. . . . . 6
β’ (π β π β βͺ ran
sigAlgebra) |
3 | | 1stmbfm.2 |
. . . . . 6
β’ (π β π β βͺ ran
sigAlgebra) |
4 | | sxuni 32832 |
. . . . . 6
β’ ((π β βͺ ran sigAlgebra β§ π β βͺ ran
sigAlgebra) β (βͺ π Γ βͺ π) = βͺ
(π Γs
π)) |
5 | 2, 3, 4 | syl2anc 585 |
. . . . 5
β’ (π β (βͺ π
Γ βͺ π) = βͺ (π Γs π)) |
6 | 5 | feq2d 6659 |
. . . 4
β’ (π β ((1st βΎ
(βͺ π Γ βͺ π)):(βͺ
π Γ βͺ π)βΆβͺ π β (1st βΎ
(βͺ π Γ βͺ π)):βͺ
(π Γs
π)βΆβͺ π)) |
7 | 1, 6 | mpbii 232 |
. . 3
β’ (π β (1st βΎ
(βͺ π Γ βͺ π)):βͺ
(π Γs
π)βΆβͺ π) |
8 | | unielsiga 32767 |
. . . . 5
β’ (π β βͺ ran sigAlgebra β βͺ π β π) |
9 | 2, 8 | syl 17 |
. . . 4
β’ (π β βͺ π
β π) |
10 | | sxsiga 32830 |
. . . . . 6
β’ ((π β βͺ ran sigAlgebra β§ π β βͺ ran
sigAlgebra) β (π
Γs π)
β βͺ ran sigAlgebra) |
11 | 2, 3, 10 | syl2anc 585 |
. . . . 5
β’ (π β (π Γs π) β βͺ ran
sigAlgebra) |
12 | | unielsiga 32767 |
. . . . 5
β’ ((π Γs π) β βͺ ran sigAlgebra β βͺ
(π Γs
π) β (π Γs π)) |
13 | 11, 12 | syl 17 |
. . . 4
β’ (π β βͺ (π
Γs π)
β (π
Γs π)) |
14 | 9, 13 | elmapd 8786 |
. . 3
β’ (π β ((1st βΎ
(βͺ π Γ βͺ π)) β (βͺ π
βm βͺ (π Γs π)) β (1st βΎ (βͺ π
Γ βͺ π)):βͺ (π Γs π)βΆβͺ π)) |
15 | 7, 14 | mpbird 257 |
. 2
β’ (π β (1st βΎ
(βͺ π Γ βͺ π)) β (βͺ π
βm βͺ (π Γs π))) |
16 | | ffn 6673 |
. . . . . . . 8
β’
((1st βΎ (βͺ π Γ βͺ π)):(βͺ
π Γ βͺ π)βΆβͺ π β (1st βΎ
(βͺ π Γ βͺ π)) Fn (βͺ π
Γ βͺ π)) |
17 | | elpreima 7013 |
. . . . . . . 8
β’
((1st βΎ (βͺ π Γ βͺ π)) Fn (βͺ π
Γ βͺ π) β (π§ β (β‘(1st βΎ (βͺ π
Γ βͺ π)) β π) β (π§ β (βͺ π Γ βͺ π)
β§ ((1st βΎ (βͺ π Γ βͺ π))βπ§) β π))) |
18 | 1, 16, 17 | mp2b 10 |
. . . . . . 7
β’ (π§ β (β‘(1st βΎ (βͺ π
Γ βͺ π)) β π) β (π§ β (βͺ π Γ βͺ π)
β§ ((1st βΎ (βͺ π Γ βͺ π))βπ§) β π)) |
19 | | fvres 6866 |
. . . . . . . . . 10
β’ (π§ β (βͺ π
Γ βͺ π) β ((1st βΎ (βͺ π
Γ βͺ π))βπ§) = (1st βπ§)) |
20 | 19 | eleq1d 2823 |
. . . . . . . . 9
β’ (π§ β (βͺ π
Γ βͺ π) β (((1st βΎ (βͺ π
Γ βͺ π))βπ§) β π β (1st βπ§) β π)) |
21 | | 1st2nd2 7965 |
. . . . . . . . . 10
β’ (π§ β (βͺ π
Γ βͺ π) β π§ = β¨(1st βπ§), (2nd βπ§)β©) |
22 | | xp2nd 7959 |
. . . . . . . . . 10
β’ (π§ β (βͺ π
Γ βͺ π) β (2nd βπ§) β βͺ π) |
23 | | elxp6 7960 |
. . . . . . . . . . . 12
β’ (π§ β (π Γ βͺ π) β (π§ = β¨(1st βπ§), (2nd βπ§)β© β§ ((1st
βπ§) β π β§ (2nd
βπ§) β βͺ π))) |
24 | | anass 470 |
. . . . . . . . . . . 12
β’ (((π§ = β¨(1st
βπ§), (2nd
βπ§)β© β§
(1st βπ§)
β π) β§
(2nd βπ§)
β βͺ π) β (π§ = β¨(1st βπ§), (2nd βπ§)β© β§ ((1st
βπ§) β π β§ (2nd
βπ§) β βͺ π))) |
25 | | an32 645 |
. . . . . . . . . . . 12
β’ (((π§ = β¨(1st
βπ§), (2nd
βπ§)β© β§
(1st βπ§)
β π) β§
(2nd βπ§)
β βͺ π) β ((π§ = β¨(1st βπ§), (2nd βπ§)β© β§ (2nd
βπ§) β βͺ π)
β§ (1st βπ§) β π)) |
26 | 23, 24, 25 | 3bitr2i 299 |
. . . . . . . . . . 11
β’ (π§ β (π Γ βͺ π) β ((π§ = β¨(1st βπ§), (2nd βπ§)β© β§ (2nd
βπ§) β βͺ π)
β§ (1st βπ§) β π)) |
27 | 26 | baib 537 |
. . . . . . . . . 10
β’ ((π§ = β¨(1st
βπ§), (2nd
βπ§)β© β§
(2nd βπ§)
β βͺ π) β (π§ β (π Γ βͺ π) β (1st
βπ§) β π)) |
28 | 21, 22, 27 | syl2anc 585 |
. . . . . . . . 9
β’ (π§ β (βͺ π
Γ βͺ π) β (π§ β (π Γ βͺ π) β (1st
βπ§) β π)) |
29 | 20, 28 | bitr4d 282 |
. . . . . . . 8
β’ (π§ β (βͺ π
Γ βͺ π) β (((1st βΎ (βͺ π
Γ βͺ π))βπ§) β π β π§ β (π Γ βͺ π))) |
30 | 29 | pm5.32i 576 |
. . . . . . 7
β’ ((π§ β (βͺ π
Γ βͺ π) β§ ((1st βΎ (βͺ π
Γ βͺ π))βπ§) β π) β (π§ β (βͺ π Γ βͺ π)
β§ π§ β (π Γ βͺ π))) |
31 | 18, 30 | bitri 275 |
. . . . . 6
β’ (π§ β (β‘(1st βΎ (βͺ π
Γ βͺ π)) β π) β (π§ β (βͺ π Γ βͺ π)
β§ π§ β (π Γ βͺ π))) |
32 | | sgon 32763 |
. . . . . . . . . . 11
β’ (π β βͺ ran sigAlgebra β π β (sigAlgebraββͺ π)) |
33 | | sigasspw 32755 |
. . . . . . . . . . 11
β’ (π β (sigAlgebraββͺ π)
β π β π«
βͺ π) |
34 | | pwssb 5066 |
. . . . . . . . . . . 12
β’ (π β π« βͺ π
β βπ β
π π β βͺ π) |
35 | 34 | biimpi 215 |
. . . . . . . . . . 11
β’ (π β π« βͺ π
β βπ β
π π β βͺ π) |
36 | 2, 32, 33, 35 | 4syl 19 |
. . . . . . . . . 10
β’ (π β βπ β π π β βͺ π) |
37 | 36 | r19.21bi 3237 |
. . . . . . . . 9
β’ ((π β§ π β π) β π β βͺ π) |
38 | | xpss1 5657 |
. . . . . . . . 9
β’ (π β βͺ π
β (π Γ βͺ π)
β (βͺ π Γ βͺ π)) |
39 | 37, 38 | syl 17 |
. . . . . . . 8
β’ ((π β§ π β π) β (π Γ βͺ π) β (βͺ π
Γ βͺ π)) |
40 | 39 | sseld 3948 |
. . . . . . 7
β’ ((π β§ π β π) β (π§ β (π Γ βͺ π) β π§ β (βͺ π Γ βͺ π))) |
41 | 40 | pm4.71rd 564 |
. . . . . 6
β’ ((π β§ π β π) β (π§ β (π Γ βͺ π) β (π§ β (βͺ π Γ βͺ π)
β§ π§ β (π Γ βͺ π)))) |
42 | 31, 41 | bitr4id 290 |
. . . . 5
β’ ((π β§ π β π) β (π§ β (β‘(1st βΎ (βͺ π
Γ βͺ π)) β π) β π§ β (π Γ βͺ π))) |
43 | 42 | eqrdv 2735 |
. . . 4
β’ ((π β§ π β π) β (β‘(1st βΎ (βͺ π
Γ βͺ π)) β π) = (π Γ βͺ π)) |
44 | 2 | adantr 482 |
. . . . 5
β’ ((π β§ π β π) β π β βͺ ran
sigAlgebra) |
45 | 3 | adantr 482 |
. . . . 5
β’ ((π β§ π β π) β π β βͺ ran
sigAlgebra) |
46 | | simpr 486 |
. . . . 5
β’ ((π β§ π β π) β π β π) |
47 | | eqid 2737 |
. . . . . . . 8
β’ βͺ π =
βͺ π |
48 | | issgon 32762 |
. . . . . . . 8
β’ (π β (sigAlgebraββͺ π)
β (π β βͺ ran sigAlgebra β§ βͺ π = βͺ
π)) |
49 | 3, 47, 48 | sylanblrc 591 |
. . . . . . 7
β’ (π β π β (sigAlgebraββͺ π)) |
50 | | baselsiga 32754 |
. . . . . . 7
β’ (π β (sigAlgebraββͺ π)
β βͺ π β π) |
51 | 49, 50 | syl 17 |
. . . . . 6
β’ (π β βͺ π
β π) |
52 | 51 | adantr 482 |
. . . . 5
β’ ((π β§ π β π) β βͺ π β π) |
53 | | elsx 32833 |
. . . . 5
β’ (((π β βͺ ran sigAlgebra β§ π β βͺ ran
sigAlgebra) β§ (π β
π β§ βͺ π
β π)) β (π Γ βͺ π)
β (π
Γs π)) |
54 | 44, 45, 46, 52, 53 | syl22anc 838 |
. . . 4
β’ ((π β§ π β π) β (π Γ βͺ π) β (π Γs π)) |
55 | 43, 54 | eqeltrd 2838 |
. . 3
β’ ((π β§ π β π) β (β‘(1st βΎ (βͺ π
Γ βͺ π)) β π) β (π Γs π)) |
56 | 55 | ralrimiva 3144 |
. 2
β’ (π β βπ β π (β‘(1st βΎ (βͺ π
Γ βͺ π)) β π) β (π Γs π)) |
57 | 11, 2 | ismbfm 32890 |
. 2
β’ (π β ((1st βΎ
(βͺ π Γ βͺ π)) β ((π Γs π)MblFnMπ) β ((1st βΎ (βͺ π
Γ βͺ π)) β (βͺ
π βm βͺ (π
Γs π))
β§ βπ β
π (β‘(1st βΎ (βͺ π
Γ βͺ π)) β π) β (π Γs π)))) |
58 | 15, 56, 57 | mpbir2and 712 |
1
β’ (π β (1st βΎ
(βͺ π Γ βͺ π)) β ((π Γs π)MblFnMπ)) |