Step | Hyp | Ref
| Expression |
1 | | fdmrn 6748 |
. . . . . . . 8
β’ (Fun
πΉ β πΉ:dom πΉβΆran πΉ) |
2 | 1 | biimpi 215 |
. . . . . . 7
β’ (Fun
πΉ β πΉ:dom πΉβΆran πΉ) |
3 | 2 | 3ad2ant1 1131 |
. . . . . 6
β’ ((Fun
πΉ β§ πΊ:π΄βΆπ΅ β§ π΄ β ran πΉ) β πΉ:dom πΉβΆran πΉ) |
4 | 3 | adantr 479 |
. . . . 5
β’ (((Fun
πΉ β§ πΊ:π΄βΆπ΅ β§ π΄ β ran πΉ) β§ (πΊ β πΉ):(β‘πΉ β π΄)βontoβπ΅) β πΉ:dom πΉβΆran πΉ) |
5 | | eqid 2730 |
. . . . 5
β’ (ran
πΉ β© π΄) = (ran πΉ β© π΄) |
6 | | eqid 2730 |
. . . . 5
β’ (β‘πΉ β π΄) = (β‘πΉ β π΄) |
7 | | eqid 2730 |
. . . . 5
β’ (πΉ βΎ (β‘πΉ β π΄)) = (πΉ βΎ (β‘πΉ β π΄)) |
8 | | simp2 1135 |
. . . . . 6
β’ ((Fun
πΉ β§ πΊ:π΄βΆπ΅ β§ π΄ β ran πΉ) β πΊ:π΄βΆπ΅) |
9 | 8 | adantr 479 |
. . . . 5
β’ (((Fun
πΉ β§ πΊ:π΄βΆπ΅ β§ π΄ β ran πΉ) β§ (πΊ β πΉ):(β‘πΉ β π΄)βontoβπ΅) β πΊ:π΄βΆπ΅) |
10 | | eqid 2730 |
. . . . 5
β’ (πΊ βΎ (ran πΉ β© π΄)) = (πΊ βΎ (ran πΉ β© π΄)) |
11 | | simpr 483 |
. . . . 5
β’ (((Fun
πΉ β§ πΊ:π΄βΆπ΅ β§ π΄ β ran πΉ) β§ (πΊ β πΉ):(β‘πΉ β π΄)βontoβπ΅) β (πΊ β πΉ):(β‘πΉ β π΄)βontoβπ΅) |
12 | 4, 5, 6, 7, 9, 10,
11 | fcoresfo 46079 |
. . . 4
β’ (((Fun
πΉ β§ πΊ:π΄βΆπ΅ β§ π΄ β ran πΉ) β§ (πΊ β πΉ):(β‘πΉ β π΄)βontoβπ΅) β (πΊ βΎ (ran πΉ β© π΄)):(ran πΉ β© π΄)βontoβπ΅) |
13 | 12 | ex 411 |
. . 3
β’ ((Fun
πΉ β§ πΊ:π΄βΆπ΅ β§ π΄ β ran πΉ) β ((πΊ β πΉ):(β‘πΉ β π΄)βontoβπ΅ β (πΊ βΎ (ran πΉ β© π΄)):(ran πΉ β© π΄)βontoβπ΅)) |
14 | | sseqin2 4214 |
. . . . . . . . 9
β’ (π΄ β ran πΉ β (ran πΉ β© π΄) = π΄) |
15 | 14 | biimpi 215 |
. . . . . . . 8
β’ (π΄ β ran πΉ β (ran πΉ β© π΄) = π΄) |
16 | 15 | 3ad2ant3 1133 |
. . . . . . 7
β’ ((Fun
πΉ β§ πΊ:π΄βΆπ΅ β§ π΄ β ran πΉ) β (ran πΉ β© π΄) = π΄) |
17 | 8 | fdmd 6727 |
. . . . . . 7
β’ ((Fun
πΉ β§ πΊ:π΄βΆπ΅ β§ π΄ β ran πΉ) β dom πΊ = π΄) |
18 | 16, 17 | eqtr4d 2773 |
. . . . . 6
β’ ((Fun
πΉ β§ πΊ:π΄βΆπ΅ β§ π΄ β ran πΉ) β (ran πΉ β© π΄) = dom πΊ) |
19 | 18 | reseq2d 5980 |
. . . . 5
β’ ((Fun
πΉ β§ πΊ:π΄βΆπ΅ β§ π΄ β ran πΉ) β (πΊ βΎ (ran πΉ β© π΄)) = (πΊ βΎ dom πΊ)) |
20 | 8 | freld 6722 |
. . . . . 6
β’ ((Fun
πΉ β§ πΊ:π΄βΆπ΅ β§ π΄ β ran πΉ) β Rel πΊ) |
21 | | resdm 6025 |
. . . . . 6
β’ (Rel
πΊ β (πΊ βΎ dom πΊ) = πΊ) |
22 | 20, 21 | syl 17 |
. . . . 5
β’ ((Fun
πΉ β§ πΊ:π΄βΆπ΅ β§ π΄ β ran πΉ) β (πΊ βΎ dom πΊ) = πΊ) |
23 | 19, 22 | eqtrd 2770 |
. . . 4
β’ ((Fun
πΉ β§ πΊ:π΄βΆπ΅ β§ π΄ β ran πΉ) β (πΊ βΎ (ran πΉ β© π΄)) = πΊ) |
24 | | eqidd 2731 |
. . . 4
β’ ((Fun
πΉ β§ πΊ:π΄βΆπ΅ β§ π΄ β ran πΉ) β π΅ = π΅) |
25 | 23, 16, 24 | foeq123d 6825 |
. . 3
β’ ((Fun
πΉ β§ πΊ:π΄βΆπ΅ β§ π΄ β ran πΉ) β ((πΊ βΎ (ran πΉ β© π΄)):(ran πΉ β© π΄)βontoβπ΅ β πΊ:π΄βontoβπ΅)) |
26 | 13, 25 | sylibd 238 |
. 2
β’ ((Fun
πΉ β§ πΊ:π΄βΆπ΅ β§ π΄ β ran πΉ) β ((πΊ β πΉ):(β‘πΉ β π΄)βontoβπ΅ β πΊ:π΄βontoβπ΅)) |
27 | | simpr 483 |
. . . 4
β’ (((Fun
πΉ β§ πΊ:π΄βΆπ΅ β§ π΄ β ran πΉ) β§ πΊ:π΄βontoβπ΅) β πΊ:π΄βontoβπ΅) |
28 | | simpl1 1189 |
. . . 4
β’ (((Fun
πΉ β§ πΊ:π΄βΆπ΅ β§ π΄ β ran πΉ) β§ πΊ:π΄βontoβπ΅) β Fun πΉ) |
29 | | simpl3 1191 |
. . . 4
β’ (((Fun
πΉ β§ πΊ:π΄βΆπ΅ β§ π΄ β ran πΉ) β§ πΊ:π΄βontoβπ΅) β π΄ β ran πΉ) |
30 | | focofo 6817 |
. . . 4
β’ ((πΊ:π΄βontoβπ΅ β§ Fun πΉ β§ π΄ β ran πΉ) β (πΊ β πΉ):(β‘πΉ β π΄)βontoβπ΅) |
31 | 27, 28, 29, 30 | syl3anc 1369 |
. . 3
β’ (((Fun
πΉ β§ πΊ:π΄βΆπ΅ β§ π΄ β ran πΉ) β§ πΊ:π΄βontoβπ΅) β (πΊ β πΉ):(β‘πΉ β π΄)βontoβπ΅) |
32 | 31 | ex 411 |
. 2
β’ ((Fun
πΉ β§ πΊ:π΄βΆπ΅ β§ π΄ β ran πΉ) β (πΊ:π΄βontoβπ΅ β (πΊ β πΉ):(β‘πΉ β π΄)βontoβπ΅)) |
33 | 26, 32 | impbid 211 |
1
β’ ((Fun
πΉ β§ πΊ:π΄βΆπ΅ β§ π΄ β ran πΉ) β ((πΊ β πΉ):(β‘πΉ β π΄)βontoβπ΅ β πΊ:π΄βontoβπ΅)) |