Step | Hyp | Ref
| Expression |
1 | | ctex 8956 |
. . . . 5
β’ (π΄ βΌ Ο β π΄ β V) |
2 | 1 | adantl 481 |
. . . 4
β’ ((πΉ Fn π΄ β§ π΄ βΌ Ο) β π΄ β V) |
3 | | fndm 6643 |
. . . . . . . 8
β’ (πΉ Fn π΄ β dom πΉ = π΄) |
4 | 3 | eleq1d 2810 |
. . . . . . 7
β’ (πΉ Fn π΄ β (dom πΉ β V β π΄ β V)) |
5 | 4 | adantr 480 |
. . . . . 6
β’ ((πΉ Fn π΄ β§ π΄ βΌ Ο) β (dom πΉ β V β π΄ β V)) |
6 | 2, 5 | mpbird 257 |
. . . . 5
β’ ((πΉ Fn π΄ β§ π΄ βΌ Ο) β dom πΉ β V) |
7 | | fnfun 6640 |
. . . . . 6
β’ (πΉ Fn π΄ β Fun πΉ) |
8 | 7 | adantr 480 |
. . . . 5
β’ ((πΉ Fn π΄ β§ π΄ βΌ Ο) β Fun πΉ) |
9 | | funrnex 7934 |
. . . . 5
β’ (dom
πΉ β V β (Fun
πΉ β ran πΉ β V)) |
10 | 6, 8, 9 | sylc 65 |
. . . 4
β’ ((πΉ Fn π΄ β§ π΄ βΌ Ο) β ran πΉ β V) |
11 | 2, 10 | xpexd 7732 |
. . 3
β’ ((πΉ Fn π΄ β§ π΄ βΌ Ο) β (π΄ Γ ran πΉ) β V) |
12 | | simpl 482 |
. . . . 5
β’ ((πΉ Fn π΄ β§ π΄ βΌ Ο) β πΉ Fn π΄) |
13 | | dffn3 6721 |
. . . . 5
β’ (πΉ Fn π΄ β πΉ:π΄βΆran πΉ) |
14 | 12, 13 | sylib 217 |
. . . 4
β’ ((πΉ Fn π΄ β§ π΄ βΌ Ο) β πΉ:π΄βΆran πΉ) |
15 | | fssxp 6736 |
. . . 4
β’ (πΉ:π΄βΆran πΉ β πΉ β (π΄ Γ ran πΉ)) |
16 | 14, 15 | syl 17 |
. . 3
β’ ((πΉ Fn π΄ β§ π΄ βΌ Ο) β πΉ β (π΄ Γ ran πΉ)) |
17 | | ssdomg 8993 |
. . 3
β’ ((π΄ Γ ran πΉ) β V β (πΉ β (π΄ Γ ran πΉ) β πΉ βΌ (π΄ Γ ran πΉ))) |
18 | 11, 16, 17 | sylc 65 |
. 2
β’ ((πΉ Fn π΄ β§ π΄ βΌ Ο) β πΉ βΌ (π΄ Γ ran πΉ)) |
19 | | xpdom1g 9066 |
. . . . 5
β’ ((ran
πΉ β V β§ π΄ βΌ Ο) β (π΄ Γ ran πΉ) βΌ (Ο Γ ran πΉ)) |
20 | 10, 19 | sylancom 587 |
. . . 4
β’ ((πΉ Fn π΄ β§ π΄ βΌ Ο) β (π΄ Γ ran πΉ) βΌ (Ο Γ ran πΉ)) |
21 | | omex 9635 |
. . . . 5
β’ Ο
β V |
22 | | fnrndomg 10528 |
. . . . . . 7
β’ (π΄ β V β (πΉ Fn π΄ β ran πΉ βΌ π΄)) |
23 | 2, 12, 22 | sylc 65 |
. . . . . 6
β’ ((πΉ Fn π΄ β§ π΄ βΌ Ο) β ran πΉ βΌ π΄) |
24 | | domtr 9000 |
. . . . . 6
β’ ((ran
πΉ βΌ π΄ β§ π΄ βΌ Ο) β ran πΉ βΌ
Ο) |
25 | 23, 24 | sylancom 587 |
. . . . 5
β’ ((πΉ Fn π΄ β§ π΄ βΌ Ο) β ran πΉ βΌ
Ο) |
26 | | xpdom2g 9065 |
. . . . 5
β’ ((Ο
β V β§ ran πΉ
βΌ Ο) β (Ο Γ ran πΉ) βΌ (Ο Γ
Ο)) |
27 | 21, 25, 26 | sylancr 586 |
. . . 4
β’ ((πΉ Fn π΄ β§ π΄ βΌ Ο) β (Ο Γ
ran πΉ) βΌ (Ο
Γ Ο)) |
28 | | domtr 9000 |
. . . 4
β’ (((π΄ Γ ran πΉ) βΌ (Ο Γ ran πΉ) β§ (Ο Γ ran
πΉ) βΌ (Ο Γ
Ο)) β (π΄ Γ
ran πΉ) βΌ (Ο
Γ Ο)) |
29 | 20, 27, 28 | syl2anc 583 |
. . 3
β’ ((πΉ Fn π΄ β§ π΄ βΌ Ο) β (π΄ Γ ran πΉ) βΌ (Ο Γ
Ο)) |
30 | | xpomen 10007 |
. . 3
β’ (Ο
Γ Ο) β Ο |
31 | | domentr 9006 |
. . 3
β’ (((π΄ Γ ran πΉ) βΌ (Ο Γ Ο) β§
(Ο Γ Ο) β Ο) β (π΄ Γ ran πΉ) βΌ Ο) |
32 | 29, 30, 31 | sylancl 585 |
. 2
β’ ((πΉ Fn π΄ β§ π΄ βΌ Ο) β (π΄ Γ ran πΉ) βΌ Ο) |
33 | | domtr 9000 |
. 2
β’ ((πΉ βΌ (π΄ Γ ran πΉ) β§ (π΄ Γ ran πΉ) βΌ Ο) β πΉ βΌ Ο) |
34 | 18, 32, 33 | syl2anc 583 |
1
β’ ((πΉ Fn π΄ β§ π΄ βΌ Ο) β πΉ βΌ Ο) |