Step | Hyp | Ref
| Expression |
1 | | funcestrcsetc.e |
. . . . 5
β’ πΈ = (ExtStrCatβπ) |
2 | | funcestrcsetc.s |
. . . . 5
β’ π = (SetCatβπ) |
3 | | funcestrcsetc.b |
. . . . 5
β’ π΅ = (BaseβπΈ) |
4 | | funcestrcsetc.c |
. . . . 5
β’ πΆ = (Baseβπ) |
5 | | funcestrcsetc.u |
. . . . 5
β’ (π β π β WUni) |
6 | | funcestrcsetc.f |
. . . . 5
β’ (π β πΉ = (π₯ β π΅ β¦ (Baseβπ₯))) |
7 | | funcestrcsetc.g |
. . . . 5
β’ (π β πΊ = (π₯ β π΅, π¦ β π΅ β¦ ( I βΎ ((Baseβπ¦) βm
(Baseβπ₯))))) |
8 | | eqid 2733 |
. . . . 5
β’
(Baseβπ) =
(Baseβπ) |
9 | 1, 2, 3, 4, 5, 6, 7, 8, 8 | funcestrcsetclem5 18037 |
. . . 4
β’ ((π β§ (π β π΅ β§ π β π΅)) β (ππΊπ) = ( I βΎ ((Baseβπ) βm
(Baseβπ)))) |
10 | 9 | anabsan2 673 |
. . 3
β’ ((π β§ π β π΅) β (ππΊπ) = ( I βΎ ((Baseβπ) βm
(Baseβπ)))) |
11 | | eqid 2733 |
. . . 4
β’
(IdβπΈ) =
(IdβπΈ) |
12 | 5 | adantr 482 |
. . . 4
β’ ((π β§ π β π΅) β π β WUni) |
13 | 1, 5 | estrcbas 18017 |
. . . . . . 7
β’ (π β π = (BaseβπΈ)) |
14 | 3, 13 | eqtr4id 2792 |
. . . . . 6
β’ (π β π΅ = π) |
15 | 14 | eleq2d 2820 |
. . . . 5
β’ (π β (π β π΅ β π β π)) |
16 | 15 | biimpa 478 |
. . . 4
β’ ((π β§ π β π΅) β π β π) |
17 | 1, 11, 12, 16 | estrcid 18026 |
. . 3
β’ ((π β§ π β π΅) β ((IdβπΈ)βπ) = ( I βΎ (Baseβπ))) |
18 | 10, 17 | fveq12d 6850 |
. 2
β’ ((π β§ π β π΅) β ((ππΊπ)β((IdβπΈ)βπ)) = (( I βΎ ((Baseβπ) βm
(Baseβπ)))β( I
βΎ (Baseβπ)))) |
19 | | fvex 6856 |
. . . . 5
β’
(Baseβπ)
β V |
20 | 19, 19 | pm3.2i 472 |
. . . 4
β’
((Baseβπ)
β V β§ (Baseβπ) β V) |
21 | 20 | a1i 11 |
. . 3
β’ ((π β§ π β π΅) β ((Baseβπ) β V β§ (Baseβπ) β V)) |
22 | | f1oi 6823 |
. . . . 5
β’ ( I
βΎ (Baseβπ)):(Baseβπ)β1-1-ontoβ(Baseβπ) |
23 | | f1of 6785 |
. . . . 5
β’ (( I
βΎ (Baseβπ)):(Baseβπ)β1-1-ontoβ(Baseβπ) β ( I βΎ (Baseβπ)):(Baseβπ)βΆ(Baseβπ)) |
24 | 22, 23 | ax-mp 5 |
. . . 4
β’ ( I
βΎ (Baseβπ)):(Baseβπ)βΆ(Baseβπ) |
25 | | elmapg 8781 |
. . . 4
β’
(((Baseβπ)
β V β§ (Baseβπ) β V) β (( I βΎ
(Baseβπ)) β
((Baseβπ)
βm (Baseβπ)) β ( I βΎ (Baseβπ)):(Baseβπ)βΆ(Baseβπ))) |
26 | 24, 25 | mpbiri 258 |
. . 3
β’
(((Baseβπ)
β V β§ (Baseβπ) β V) β ( I βΎ
(Baseβπ)) β
((Baseβπ)
βm (Baseβπ))) |
27 | | fvresi 7120 |
. . 3
β’ (( I
βΎ (Baseβπ))
β ((Baseβπ)
βm (Baseβπ)) β (( I βΎ ((Baseβπ) βm
(Baseβπ)))β( I
βΎ (Baseβπ))) =
( I βΎ (Baseβπ))) |
28 | 21, 26, 27 | 3syl 18 |
. 2
β’ ((π β§ π β π΅) β (( I βΎ ((Baseβπ) βm
(Baseβπ)))β( I
βΎ (Baseβπ))) =
( I βΎ (Baseβπ))) |
29 | 1, 2, 3, 4, 5, 6 | funcestrcsetclem1 18033 |
. . . 4
β’ ((π β§ π β π΅) β (πΉβπ) = (Baseβπ)) |
30 | 29 | fveq2d 6847 |
. . 3
β’ ((π β§ π β π΅) β ((Idβπ)β(πΉβπ)) = ((Idβπ)β(Baseβπ))) |
31 | | eqid 2733 |
. . . 4
β’
(Idβπ) =
(Idβπ) |
32 | 1, 3, 5 | estrcbasbas 18023 |
. . . 4
β’ ((π β§ π β π΅) β (Baseβπ) β π) |
33 | 2, 31, 12, 32 | setcid 17977 |
. . 3
β’ ((π β§ π β π΅) β ((Idβπ)β(Baseβπ)) = ( I βΎ (Baseβπ))) |
34 | 30, 33 | eqtr2d 2774 |
. 2
β’ ((π β§ π β π΅) β ( I βΎ (Baseβπ)) = ((Idβπ)β(πΉβπ))) |
35 | 18, 28, 34 | 3eqtrd 2777 |
1
β’ ((π β§ π β π΅) β ((ππΊπ)β((IdβπΈ)βπ)) = ((Idβπ)β(πΉβπ))) |