Step | Hyp | Ref
| Expression |
1 | | funcestrcsetc.e |
. . 3
β’ πΈ = (ExtStrCatβπ) |
2 | | funcestrcsetc.s |
. . 3
β’ π = (SetCatβπ) |
3 | | funcestrcsetc.b |
. . 3
β’ π΅ = (BaseβπΈ) |
4 | | funcestrcsetc.c |
. . 3
β’ πΆ = (Baseβπ) |
5 | | funcestrcsetc.u |
. . 3
β’ (π β π β WUni) |
6 | | funcestrcsetc.f |
. . 3
β’ (π β πΉ = (π₯ β π΅ β¦ (Baseβπ₯))) |
7 | | funcestrcsetc.g |
. . 3
β’ (π β πΊ = (π₯ β π΅, π¦ β π΅ β¦ ( I βΎ ((Baseβπ¦) βm
(Baseβπ₯))))) |
8 | 1, 2, 3, 4, 5, 6, 7 | fthestrcsetc 18043 |
. 2
β’ (π β πΉ(πΈ Faith π)πΊ) |
9 | 1, 2, 3, 4, 5, 6, 7 | fullestrcsetc 18044 |
. 2
β’ (π β πΉ(πΈ Full π)πΊ) |
10 | 2, 5 | setcbas 17969 |
. . . . . . . . 9
β’ (π β π = (Baseβπ)) |
11 | 4, 10 | eqtr4id 2792 |
. . . . . . . 8
β’ (π β πΆ = π) |
12 | 11 | eleq2d 2820 |
. . . . . . 7
β’ (π β (π β πΆ β π β π)) |
13 | | eqid 2733 |
. . . . . . . . 9
β’
{β¨(Baseβndx), πβ©} = {β¨(Baseβndx), πβ©} |
14 | | equivestrcsetc.i |
. . . . . . . . 9
β’ (π β (Baseβndx) β
π) |
15 | 13, 5, 14 | 1strwunbndx 17107 |
. . . . . . . 8
β’ ((π β§ π β π) β {β¨(Baseβndx), πβ©} β π) |
16 | 15 | ex 414 |
. . . . . . 7
β’ (π β (π β π β {β¨(Baseβndx), πβ©} β π)) |
17 | 12, 16 | sylbid 239 |
. . . . . 6
β’ (π β (π β πΆ β {β¨(Baseβndx), πβ©} β π)) |
18 | 17 | imp 408 |
. . . . 5
β’ ((π β§ π β πΆ) β {β¨(Baseβndx), πβ©} β π) |
19 | 1, 5 | estrcbas 18017 |
. . . . . . 7
β’ (π β π = (BaseβπΈ)) |
20 | 19 | adantr 482 |
. . . . . 6
β’ ((π β§ π β πΆ) β π = (BaseβπΈ)) |
21 | 3, 20 | eqtr4id 2792 |
. . . . 5
β’ ((π β§ π β πΆ) β π΅ = π) |
22 | 18, 21 | eleqtrrd 2837 |
. . . 4
β’ ((π β§ π β πΆ) β {β¨(Baseβndx), πβ©} β π΅) |
23 | | fveq2 6843 |
. . . . . . 7
β’ (π = {β¨(Baseβndx),
πβ©} β (πΉβπ) = (πΉβ{β¨(Baseβndx), πβ©})) |
24 | 23 | f1oeq3d 6782 |
. . . . . 6
β’ (π = {β¨(Baseβndx),
πβ©} β (π:πβ1-1-ontoβ(πΉβπ) β π:πβ1-1-ontoβ(πΉβ{β¨(Baseβndx), πβ©}))) |
25 | 24 | exbidv 1925 |
. . . . 5
β’ (π = {β¨(Baseβndx),
πβ©} β
(βπ π:πβ1-1-ontoβ(πΉβπ) β βπ π:πβ1-1-ontoβ(πΉβ{β¨(Baseβndx), πβ©}))) |
26 | 25 | adantl 483 |
. . . 4
β’ (((π β§ π β πΆ) β§ π = {β¨(Baseβndx), πβ©}) β (βπ π:πβ1-1-ontoβ(πΉβπ) β βπ π:πβ1-1-ontoβ(πΉβ{β¨(Baseβndx), πβ©}))) |
27 | | f1oi 6823 |
. . . . . 6
β’ ( I
βΎ π):πβ1-1-ontoβπ |
28 | 1, 2, 3, 4, 5, 6 | funcestrcsetclem1 18033 |
. . . . . . . . 9
β’ ((π β§ {β¨(Baseβndx),
πβ©} β π΅) β (πΉβ{β¨(Baseβndx), πβ©}) =
(Baseβ{β¨(Baseβndx), πβ©})) |
29 | 22, 28 | syldan 592 |
. . . . . . . 8
β’ ((π β§ π β πΆ) β (πΉβ{β¨(Baseβndx), πβ©}) =
(Baseβ{β¨(Baseβndx), πβ©})) |
30 | 13 | 1strbas 17105 |
. . . . . . . . 9
β’ (π β πΆ β π = (Baseβ{β¨(Baseβndx), πβ©})) |
31 | 30 | adantl 483 |
. . . . . . . 8
β’ ((π β§ π β πΆ) β π = (Baseβ{β¨(Baseβndx), πβ©})) |
32 | 29, 31 | eqtr4d 2776 |
. . . . . . 7
β’ ((π β§ π β πΆ) β (πΉβ{β¨(Baseβndx), πβ©}) = π) |
33 | 32 | f1oeq3d 6782 |
. . . . . 6
β’ ((π β§ π β πΆ) β (( I βΎ π):πβ1-1-ontoβ(πΉβ{β¨(Baseβndx), πβ©}) β ( I βΎ
π):πβ1-1-ontoβπ)) |
34 | 27, 33 | mpbiri 258 |
. . . . 5
β’ ((π β§ π β πΆ) β ( I βΎ π):πβ1-1-ontoβ(πΉβ{β¨(Baseβndx), πβ©})) |
35 | | resiexg 7852 |
. . . . . . 7
β’ (π β V β ( I βΎ
π) β
V) |
36 | 35 | elv 3450 |
. . . . . 6
β’ ( I
βΎ π) β
V |
37 | | f1oeq1 6773 |
. . . . . 6
β’ (π = ( I βΎ π) β (π:πβ1-1-ontoβ(πΉβ{β¨(Baseβndx), πβ©}) β ( I βΎ
π):πβ1-1-ontoβ(πΉβ{β¨(Baseβndx), πβ©}))) |
38 | 36, 37 | spcev 3564 |
. . . . 5
β’ (( I
βΎ π):πβ1-1-ontoβ(πΉβ{β¨(Baseβndx), πβ©}) β βπ π:πβ1-1-ontoβ(πΉβ{β¨(Baseβndx), πβ©})) |
39 | 34, 38 | syl 17 |
. . . 4
β’ ((π β§ π β πΆ) β βπ π:πβ1-1-ontoβ(πΉβ{β¨(Baseβndx), πβ©})) |
40 | 22, 26, 39 | rspcedvd 3582 |
. . 3
β’ ((π β§ π β πΆ) β βπ β π΅ βπ π:πβ1-1-ontoβ(πΉβπ)) |
41 | 40 | ralrimiva 3140 |
. 2
β’ (π β βπ β πΆ βπ β π΅ βπ π:πβ1-1-ontoβ(πΉβπ)) |
42 | 8, 9, 41 | 3jca 1129 |
1
β’ (π β (πΉ(πΈ Faith π)πΊ β§ πΉ(πΈ Full π)πΊ β§ βπ β πΆ βπ β π΅ βπ π:πβ1-1-ontoβ(πΉβπ))) |