Step | Hyp | Ref
| Expression |
1 | | f1f1orn 6796 |
. . . . . . . 8
β’ (πΉ:π΄β1-1βπ΅ β πΉ:π΄β1-1-ontoβran
πΉ) |
2 | 1 | 3ad2ant1 1134 |
. . . . . . 7
β’ ((πΉ:π΄β1-1βπ΅ β§ π΄ β π β§ π΅ β π) β πΉ:π΄β1-1-ontoβran
πΉ) |
3 | | simp2 1138 |
. . . . . . . . . 10
β’ ((πΉ:π΄β1-1βπ΅ β§ π΄ β π β§ π΅ β π) β π΄ β π) |
4 | | rnexg 7842 |
. . . . . . . . . 10
β’ (π΄ β π β ran π΄ β V) |
5 | 3, 4 | syl 17 |
. . . . . . . . 9
β’ ((πΉ:π΄β1-1βπ΅ β§ π΄ β π β§ π΅ β π) β ran π΄ β V) |
6 | | uniexg 7678 |
. . . . . . . . 9
β’ (ran
π΄ β V β βͺ ran π΄ β V) |
7 | | pwexg 5334 |
. . . . . . . . 9
β’ (βͺ ran π΄ β V β π« βͺ ran π΄ β V) |
8 | 5, 6, 7 | 3syl 18 |
. . . . . . . 8
β’ ((πΉ:π΄β1-1βπ΅ β§ π΄ β π β§ π΅ β π) β π« βͺ ran π΄ β V) |
9 | | 1stconst 8033 |
. . . . . . . 8
β’
(π« βͺ ran π΄ β V β (1st βΎ
((π΅ β ran πΉ) Γ {π« βͺ ran π΄})):((π΅ β ran πΉ) Γ {π« βͺ ran π΄})β1-1-ontoβ(π΅ β ran πΉ)) |
10 | 8, 9 | syl 17 |
. . . . . . 7
β’ ((πΉ:π΄β1-1βπ΅ β§ π΄ β π β§ π΅ β π) β (1st βΎ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄})):((π΅ β ran πΉ) Γ {π« βͺ ran π΄})β1-1-ontoβ(π΅ β ran πΉ)) |
11 | | difexg 5285 |
. . . . . . . . . 10
β’ (π΅ β π β (π΅ β ran πΉ) β V) |
12 | 11 | 3ad2ant3 1136 |
. . . . . . . . 9
β’ ((πΉ:π΄β1-1βπ΅ β§ π΄ β π β§ π΅ β π) β (π΅ β ran πΉ) β V) |
13 | | disjen 9081 |
. . . . . . . . 9
β’ ((π΄ β π β§ (π΅ β ran πΉ) β V) β ((π΄ β© ((π΅ β ran πΉ) Γ {π« βͺ ran π΄})) = β
β§ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄}) β (π΅ β ran πΉ))) |
14 | 3, 12, 13 | syl2anc 585 |
. . . . . . . 8
β’ ((πΉ:π΄β1-1βπ΅ β§ π΄ β π β§ π΅ β π) β ((π΄ β© ((π΅ β ran πΉ) Γ {π« βͺ ran π΄})) = β
β§ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄}) β (π΅ β ran πΉ))) |
15 | 14 | simpld 496 |
. . . . . . 7
β’ ((πΉ:π΄β1-1βπ΅ β§ π΄ β π β§ π΅ β π) β (π΄ β© ((π΅ β ran πΉ) Γ {π« βͺ ran π΄})) = β
) |
16 | | disjdif 4432 |
. . . . . . . 8
β’ (ran
πΉ β© (π΅ β ran πΉ)) = β
|
17 | 16 | a1i 11 |
. . . . . . 7
β’ ((πΉ:π΄β1-1βπ΅ β§ π΄ β π β§ π΅ β π) β (ran πΉ β© (π΅ β ran πΉ)) = β
) |
18 | | f1oun 6804 |
. . . . . . 7
β’ (((πΉ:π΄β1-1-ontoβran
πΉ β§ (1st
βΎ ((π΅ β ran
πΉ) Γ {π« βͺ ran π΄})):((π΅ β ran πΉ) Γ {π« βͺ ran π΄})β1-1-ontoβ(π΅ β ran πΉ)) β§ ((π΄ β© ((π΅ β ran πΉ) Γ {π« βͺ ran π΄})) = β
β§ (ran πΉ β© (π΅ β ran πΉ)) = β
)) β (πΉ βͺ (1st βΎ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄}))):(π΄ βͺ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄}))β1-1-ontoβ(ran
πΉ βͺ (π΅ β ran πΉ))) |
19 | 2, 10, 15, 17, 18 | syl22anc 838 |
. . . . . 6
β’ ((πΉ:π΄β1-1βπ΅ β§ π΄ β π β§ π΅ β π) β (πΉ βͺ (1st βΎ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄}))):(π΄ βͺ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄}))β1-1-ontoβ(ran
πΉ βͺ (π΅ β ran πΉ))) |
20 | | undif2 4437 |
. . . . . . . 8
β’ (ran
πΉ βͺ (π΅ β ran πΉ)) = (ran πΉ βͺ π΅) |
21 | | f1f 6739 |
. . . . . . . . . . 11
β’ (πΉ:π΄β1-1βπ΅ β πΉ:π΄βΆπ΅) |
22 | 21 | 3ad2ant1 1134 |
. . . . . . . . . 10
β’ ((πΉ:π΄β1-1βπ΅ β§ π΄ β π β§ π΅ β π) β πΉ:π΄βΆπ΅) |
23 | 22 | frnd 6677 |
. . . . . . . . 9
β’ ((πΉ:π΄β1-1βπ΅ β§ π΄ β π β§ π΅ β π) β ran πΉ β π΅) |
24 | | ssequn1 4141 |
. . . . . . . . 9
β’ (ran
πΉ β π΅ β (ran πΉ βͺ π΅) = π΅) |
25 | 23, 24 | sylib 217 |
. . . . . . . 8
β’ ((πΉ:π΄β1-1βπ΅ β§ π΄ β π β§ π΅ β π) β (ran πΉ βͺ π΅) = π΅) |
26 | 20, 25 | eqtrid 2785 |
. . . . . . 7
β’ ((πΉ:π΄β1-1βπ΅ β§ π΄ β π β§ π΅ β π) β (ran πΉ βͺ (π΅ β ran πΉ)) = π΅) |
27 | 26 | f1oeq3d 6782 |
. . . . . 6
β’ ((πΉ:π΄β1-1βπ΅ β§ π΄ β π β§ π΅ β π) β ((πΉ βͺ (1st βΎ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄}))):(π΄ βͺ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄}))β1-1-ontoβ(ran
πΉ βͺ (π΅ β ran πΉ)) β (πΉ βͺ (1st βΎ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄}))):(π΄ βͺ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄}))β1-1-ontoβπ΅)) |
28 | 19, 27 | mpbid 231 |
. . . . 5
β’ ((πΉ:π΄β1-1βπ΅ β§ π΄ β π β§ π΅ β π) β (πΉ βͺ (1st βΎ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄}))):(π΄ βͺ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄}))β1-1-ontoβπ΅) |
29 | | f1ocnv 6797 |
. . . . 5
β’ ((πΉ βͺ (1st βΎ
((π΅ β ran πΉ) Γ {π« βͺ ran π΄}))):(π΄ βͺ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄}))β1-1-ontoβπ΅ β β‘(πΉ βͺ (1st βΎ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄}))):π΅β1-1-ontoβ(π΄ βͺ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄}))) |
30 | 28, 29 | syl 17 |
. . . 4
β’ ((πΉ:π΄β1-1βπ΅ β§ π΄ β π β§ π΅ β π) β β‘(πΉ βͺ (1st βΎ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄}))):π΅β1-1-ontoβ(π΄ βͺ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄}))) |
31 | | domss2.1 |
. . . . 5
β’ πΊ = β‘(πΉ βͺ (1st βΎ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄}))) |
32 | | f1oeq1 6773 |
. . . . 5
β’ (πΊ = β‘(πΉ βͺ (1st βΎ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄}))) β (πΊ:π΅β1-1-ontoβ(π΄ βͺ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄})) β β‘(πΉ βͺ (1st βΎ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄}))):π΅β1-1-ontoβ(π΄ βͺ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄})))) |
33 | 31, 32 | ax-mp 5 |
. . . 4
β’ (πΊ:π΅β1-1-ontoβ(π΄ βͺ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄})) β β‘(πΉ βͺ (1st βΎ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄}))):π΅β1-1-ontoβ(π΄ βͺ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄}))) |
34 | 30, 33 | sylibr 233 |
. . 3
β’ ((πΉ:π΄β1-1βπ΅ β§ π΄ β π β§ π΅ β π) β πΊ:π΅β1-1-ontoβ(π΄ βͺ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄}))) |
35 | | f1ofo 6792 |
. . . . 5
β’ (πΊ:π΅β1-1-ontoβ(π΄ βͺ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄})) β πΊ:π΅βontoβ(π΄ βͺ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄}))) |
36 | | forn 6760 |
. . . . 5
β’ (πΊ:π΅βontoβ(π΄ βͺ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄})) β ran πΊ = (π΄ βͺ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄}))) |
37 | 34, 35, 36 | 3syl 18 |
. . . 4
β’ ((πΉ:π΄β1-1βπ΅ β§ π΄ β π β§ π΅ β π) β ran πΊ = (π΄ βͺ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄}))) |
38 | 37 | f1oeq3d 6782 |
. . 3
β’ ((πΉ:π΄β1-1βπ΅ β§ π΄ β π β§ π΅ β π) β (πΊ:π΅β1-1-ontoβran
πΊ β πΊ:π΅β1-1-ontoβ(π΄ βͺ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄})))) |
39 | 34, 38 | mpbird 257 |
. 2
β’ ((πΉ:π΄β1-1βπ΅ β§ π΄ β π β§ π΅ β π) β πΊ:π΅β1-1-ontoβran
πΊ) |
40 | | ssun1 4133 |
. . 3
β’ π΄ β (π΄ βͺ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄})) |
41 | 40, 37 | sseqtrrid 3998 |
. 2
β’ ((πΉ:π΄β1-1βπ΅ β§ π΄ β π β§ π΅ β π) β π΄ β ran πΊ) |
42 | | ssid 3967 |
. . . 4
β’ ran πΉ β ran πΉ |
43 | | cores 6202 |
. . . 4
β’ (ran
πΉ β ran πΉ β ((πΊ βΎ ran πΉ) β πΉ) = (πΊ β πΉ)) |
44 | 42, 43 | ax-mp 5 |
. . 3
β’ ((πΊ βΎ ran πΉ) β πΉ) = (πΊ β πΉ) |
45 | | dmres 5960 |
. . . . . . . . 9
β’ dom
(β‘(1st βΎ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄})) βΎ ran πΉ) = (ran πΉ β© dom β‘(1st βΎ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄}))) |
46 | | f1ocnv 6797 |
. . . . . . . . . . . 12
β’
((1st βΎ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄})):((π΅ β ran πΉ) Γ {π« βͺ ran π΄})β1-1-ontoβ(π΅ β ran πΉ) β β‘(1st βΎ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄})):(π΅ β ran πΉ)β1-1-ontoβ((π΅ β ran πΉ) Γ {π« βͺ ran π΄})) |
47 | | f1odm 6789 |
. . . . . . . . . . . 12
β’ (β‘(1st βΎ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄})):(π΅ β ran πΉ)β1-1-ontoβ((π΅ β ran πΉ) Γ {π« βͺ ran π΄}) β dom β‘(1st βΎ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄})) = (π΅ β ran πΉ)) |
48 | 10, 46, 47 | 3syl 18 |
. . . . . . . . . . 11
β’ ((πΉ:π΄β1-1βπ΅ β§ π΄ β π β§ π΅ β π) β dom β‘(1st βΎ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄})) = (π΅ β ran πΉ)) |
49 | 48 | ineq2d 4173 |
. . . . . . . . . 10
β’ ((πΉ:π΄β1-1βπ΅ β§ π΄ β π β§ π΅ β π) β (ran πΉ β© dom β‘(1st βΎ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄}))) = (ran πΉ β© (π΅ β ran πΉ))) |
50 | 49, 16 | eqtrdi 2789 |
. . . . . . . . 9
β’ ((πΉ:π΄β1-1βπ΅ β§ π΄ β π β§ π΅ β π) β (ran πΉ β© dom β‘(1st βΎ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄}))) = β
) |
51 | 45, 50 | eqtrid 2785 |
. . . . . . . 8
β’ ((πΉ:π΄β1-1βπ΅ β§ π΄ β π β§ π΅ β π) β dom (β‘(1st βΎ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄})) βΎ ran πΉ) = β
) |
52 | | relres 5967 |
. . . . . . . . 9
β’ Rel
(β‘(1st βΎ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄})) βΎ ran πΉ) |
53 | | reldm0 5884 |
. . . . . . . . 9
β’ (Rel
(β‘(1st βΎ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄})) βΎ ran πΉ) β ((β‘(1st βΎ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄})) βΎ ran πΉ) = β
β dom (β‘(1st βΎ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄})) βΎ ran πΉ) = β
)) |
54 | 52, 53 | ax-mp 5 |
. . . . . . . 8
β’ ((β‘(1st βΎ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄})) βΎ ran πΉ) = β
β dom (β‘(1st βΎ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄})) βΎ ran πΉ) = β
) |
55 | 51, 54 | sylibr 233 |
. . . . . . 7
β’ ((πΉ:π΄β1-1βπ΅ β§ π΄ β π β§ π΅ β π) β (β‘(1st βΎ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄})) βΎ ran πΉ) = β
) |
56 | 55 | uneq2d 4124 |
. . . . . 6
β’ ((πΉ:π΄β1-1βπ΅ β§ π΄ β π β§ π΅ β π) β (β‘πΉ βͺ (β‘(1st βΎ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄})) βΎ ran πΉ)) = (β‘πΉ βͺ β
)) |
57 | | cnvun 6096 |
. . . . . . . . 9
β’ β‘(πΉ βͺ (1st βΎ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄}))) = (β‘πΉ βͺ β‘(1st βΎ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄}))) |
58 | 31, 57 | eqtri 2761 |
. . . . . . . 8
β’ πΊ = (β‘πΉ βͺ β‘(1st βΎ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄}))) |
59 | 58 | reseq1i 5934 |
. . . . . . 7
β’ (πΊ βΎ ran πΉ) = ((β‘πΉ βͺ β‘(1st βΎ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄}))) βΎ ran πΉ) |
60 | | resundir 5953 |
. . . . . . 7
β’ ((β‘πΉ βͺ β‘(1st βΎ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄}))) βΎ ran πΉ) = ((β‘πΉ βΎ ran πΉ) βͺ (β‘(1st βΎ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄})) βΎ ran πΉ)) |
61 | | df-rn 5645 |
. . . . . . . . . 10
β’ ran πΉ = dom β‘πΉ |
62 | 61 | reseq2i 5935 |
. . . . . . . . 9
β’ (β‘πΉ βΎ ran πΉ) = (β‘πΉ βΎ dom β‘πΉ) |
63 | | relcnv 6057 |
. . . . . . . . . 10
β’ Rel β‘πΉ |
64 | | resdm 5983 |
. . . . . . . . . 10
β’ (Rel
β‘πΉ β (β‘πΉ βΎ dom β‘πΉ) = β‘πΉ) |
65 | 63, 64 | ax-mp 5 |
. . . . . . . . 9
β’ (β‘πΉ βΎ dom β‘πΉ) = β‘πΉ |
66 | 62, 65 | eqtri 2761 |
. . . . . . . 8
β’ (β‘πΉ βΎ ran πΉ) = β‘πΉ |
67 | 66 | uneq1i 4120 |
. . . . . . 7
β’ ((β‘πΉ βΎ ran πΉ) βͺ (β‘(1st βΎ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄})) βΎ ran πΉ)) = (β‘πΉ βͺ (β‘(1st βΎ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄})) βΎ ran πΉ)) |
68 | 59, 60, 67 | 3eqtrri 2766 |
. . . . . 6
β’ (β‘πΉ βͺ (β‘(1st βΎ ((π΅ β ran πΉ) Γ {π« βͺ ran π΄})) βΎ ran πΉ)) = (πΊ βΎ ran πΉ) |
69 | | un0 4351 |
. . . . . 6
β’ (β‘πΉ βͺ β
) = β‘πΉ |
70 | 56, 68, 69 | 3eqtr3g 2796 |
. . . . 5
β’ ((πΉ:π΄β1-1βπ΅ β§ π΄ β π β§ π΅ β π) β (πΊ βΎ ran πΉ) = β‘πΉ) |
71 | 70 | coeq1d 5818 |
. . . 4
β’ ((πΉ:π΄β1-1βπ΅ β§ π΄ β π β§ π΅ β π) β ((πΊ βΎ ran πΉ) β πΉ) = (β‘πΉ β πΉ)) |
72 | | f1cocnv1 6815 |
. . . . 5
β’ (πΉ:π΄β1-1βπ΅ β (β‘πΉ β πΉ) = ( I βΎ π΄)) |
73 | 72 | 3ad2ant1 1134 |
. . . 4
β’ ((πΉ:π΄β1-1βπ΅ β§ π΄ β π β§ π΅ β π) β (β‘πΉ β πΉ) = ( I βΎ π΄)) |
74 | 71, 73 | eqtrd 2773 |
. . 3
β’ ((πΉ:π΄β1-1βπ΅ β§ π΄ β π β§ π΅ β π) β ((πΊ βΎ ran πΉ) β πΉ) = ( I βΎ π΄)) |
75 | 44, 74 | eqtr3id 2787 |
. 2
β’ ((πΉ:π΄β1-1βπ΅ β§ π΄ β π β§ π΅ β π) β (πΊ β πΉ) = ( I βΎ π΄)) |
76 | 39, 41, 75 | 3jca 1129 |
1
β’ ((πΉ:π΄β1-1βπ΅ β§ π΄ β π β§ π΅ β π) β (πΊ:π΅β1-1-ontoβran
πΊ β§ π΄ β ran πΊ β§ (πΊ β πΉ) = ( I βΎ π΄))) |