Step | Hyp | Ref
| Expression |
1 | | fdmrn 6750 |
. . . . . . . 8
β’ (Fun
πΉ β πΉ:dom πΉβΆran πΉ) |
2 | 1 | biimpi 215 |
. . . . . . 7
β’ (Fun
πΉ β πΉ:dom πΉβΆran πΉ) |
3 | 2 | 3ad2ant1 1134 |
. . . . . 6
β’ ((Fun
πΉ β§ πΊ:π΄βΆπ΅ β§ π΄ β ran πΉ) β πΉ:dom πΉβΆran πΉ) |
4 | 3 | adantr 482 |
. . . . 5
β’ (((Fun
πΉ β§ πΊ:π΄βΆπ΅ β§ π΄ β ran πΉ) β§ (πΊ β πΉ):(β‘πΉ β π΄)βontoβπ΅) β πΉ:dom πΉβΆran πΉ) |
5 | | eqid 2733 |
. . . . 5
β’ (ran
πΉ β© π΄) = (ran πΉ β© π΄) |
6 | | eqid 2733 |
. . . . 5
β’ (β‘πΉ β π΄) = (β‘πΉ β π΄) |
7 | | eqid 2733 |
. . . . 5
β’ (πΉ βΎ (β‘πΉ β π΄)) = (πΉ βΎ (β‘πΉ β π΄)) |
8 | | simp2 1138 |
. . . . . 6
β’ ((Fun
πΉ β§ πΊ:π΄βΆπ΅ β§ π΄ β ran πΉ) β πΊ:π΄βΆπ΅) |
9 | 8 | adantr 482 |
. . . . 5
β’ (((Fun
πΉ β§ πΊ:π΄βΆπ΅ β§ π΄ β ran πΉ) β§ (πΊ β πΉ):(β‘πΉ β π΄)βontoβπ΅) β πΊ:π΄βΆπ΅) |
10 | | eqid 2733 |
. . . . 5
β’ (πΊ βΎ (ran πΉ β© π΄)) = (πΊ βΎ (ran πΉ β© π΄)) |
11 | | simpr 486 |
. . . . 5
β’ (((Fun
πΉ β§ πΊ:π΄βΆπ΅ β§ π΄ β ran πΉ) β§ (πΊ β πΉ):(β‘πΉ β π΄)βontoβπ΅) β (πΊ β πΉ):(β‘πΉ β π΄)βontoβπ΅) |
12 | 4, 5, 6, 7, 9, 10,
11 | fcoresfo 45781 |
. . . 4
β’ (((Fun
πΉ β§ πΊ:π΄βΆπ΅ β§ π΄ β ran πΉ) β§ (πΊ β πΉ):(β‘πΉ β π΄)βontoβπ΅) β (πΊ βΎ (ran πΉ β© π΄)):(ran πΉ β© π΄)βontoβπ΅) |
13 | 12 | ex 414 |
. . 3
β’ ((Fun
πΉ β§ πΊ:π΄βΆπ΅ β§ π΄ β ran πΉ) β ((πΊ β πΉ):(β‘πΉ β π΄)βontoβπ΅ β (πΊ βΎ (ran πΉ β© π΄)):(ran πΉ β© π΄)βontoβπ΅)) |
14 | | sseqin2 4216 |
. . . . . . . . 9
β’ (π΄ β ran πΉ β (ran πΉ β© π΄) = π΄) |
15 | 14 | biimpi 215 |
. . . . . . . 8
β’ (π΄ β ran πΉ β (ran πΉ β© π΄) = π΄) |
16 | 15 | 3ad2ant3 1136 |
. . . . . . 7
β’ ((Fun
πΉ β§ πΊ:π΄βΆπ΅ β§ π΄ β ran πΉ) β (ran πΉ β© π΄) = π΄) |
17 | 8 | fdmd 6729 |
. . . . . . 7
β’ ((Fun
πΉ β§ πΊ:π΄βΆπ΅ β§ π΄ β ran πΉ) β dom πΊ = π΄) |
18 | 16, 17 | eqtr4d 2776 |
. . . . . 6
β’ ((Fun
πΉ β§ πΊ:π΄βΆπ΅ β§ π΄ β ran πΉ) β (ran πΉ β© π΄) = dom πΊ) |
19 | 18 | reseq2d 5982 |
. . . . 5
β’ ((Fun
πΉ β§ πΊ:π΄βΆπ΅ β§ π΄ β ran πΉ) β (πΊ βΎ (ran πΉ β© π΄)) = (πΊ βΎ dom πΊ)) |
20 | 8 | freld 6724 |
. . . . . 6
β’ ((Fun
πΉ β§ πΊ:π΄βΆπ΅ β§ π΄ β ran πΉ) β Rel πΊ) |
21 | | resdm 6027 |
. . . . . 6
β’ (Rel
πΊ β (πΊ βΎ dom πΊ) = πΊ) |
22 | 20, 21 | syl 17 |
. . . . 5
β’ ((Fun
πΉ β§ πΊ:π΄βΆπ΅ β§ π΄ β ran πΉ) β (πΊ βΎ dom πΊ) = πΊ) |
23 | 19, 22 | eqtrd 2773 |
. . . 4
β’ ((Fun
πΉ β§ πΊ:π΄βΆπ΅ β§ π΄ β ran πΉ) β (πΊ βΎ (ran πΉ β© π΄)) = πΊ) |
24 | | eqidd 2734 |
. . . 4
β’ ((Fun
πΉ β§ πΊ:π΄βΆπ΅ β§ π΄ β ran πΉ) β π΅ = π΅) |
25 | 23, 16, 24 | foeq123d 6827 |
. . 3
β’ ((Fun
πΉ β§ πΊ:π΄βΆπ΅ β§ π΄ β ran πΉ) β ((πΊ βΎ (ran πΉ β© π΄)):(ran πΉ β© π΄)βontoβπ΅ β πΊ:π΄βontoβπ΅)) |
26 | 13, 25 | sylibd 238 |
. 2
β’ ((Fun
πΉ β§ πΊ:π΄βΆπ΅ β§ π΄ β ran πΉ) β ((πΊ β πΉ):(β‘πΉ β π΄)βontoβπ΅ β πΊ:π΄βontoβπ΅)) |
27 | | simpr 486 |
. . . 4
β’ (((Fun
πΉ β§ πΊ:π΄βΆπ΅ β§ π΄ β ran πΉ) β§ πΊ:π΄βontoβπ΅) β πΊ:π΄βontoβπ΅) |
28 | | simpl1 1192 |
. . . 4
β’ (((Fun
πΉ β§ πΊ:π΄βΆπ΅ β§ π΄ β ran πΉ) β§ πΊ:π΄βontoβπ΅) β Fun πΉ) |
29 | | simpl3 1194 |
. . . 4
β’ (((Fun
πΉ β§ πΊ:π΄βΆπ΅ β§ π΄ β ran πΉ) β§ πΊ:π΄βontoβπ΅) β π΄ β ran πΉ) |
30 | | focofo 6819 |
. . . 4
β’ ((πΊ:π΄βontoβπ΅ β§ Fun πΉ β§ π΄ β ran πΉ) β (πΊ β πΉ):(β‘πΉ β π΄)βontoβπ΅) |
31 | 27, 28, 29, 30 | syl3anc 1372 |
. . 3
β’ (((Fun
πΉ β§ πΊ:π΄βΆπ΅ β§ π΄ β ran πΉ) β§ πΊ:π΄βontoβπ΅) β (πΊ β πΉ):(β‘πΉ β π΄)βontoβπ΅) |
32 | 31 | ex 414 |
. 2
β’ ((Fun
πΉ β§ πΊ:π΄βΆπ΅ β§ π΄ β ran πΉ) β (πΊ:π΄βontoβπ΅ β (πΊ β πΉ):(β‘πΉ β π΄)βontoβπ΅)) |
33 | 26, 32 | impbid 211 |
1
β’ ((Fun
πΉ β§ πΊ:π΄βΆπ΅ β§ π΄ β ran πΉ) β ((πΊ β πΉ):(β‘πΉ β π΄)βontoβπ΅ β πΊ:π΄βontoβπ΅)) |