Step | Hyp | Ref
| Expression |
1 | | ctex 8904 |
. . . . 5
β’ (π΄ βΌ Ο β π΄ β V) |
2 | 1 | adantl 483 |
. . . 4
β’ ((πΉ Fn π΄ β§ π΄ βΌ Ο) β π΄ β V) |
3 | | fndm 6606 |
. . . . . . . 8
β’ (πΉ Fn π΄ β dom πΉ = π΄) |
4 | 3 | eleq1d 2823 |
. . . . . . 7
β’ (πΉ Fn π΄ β (dom πΉ β V β π΄ β V)) |
5 | 4 | adantr 482 |
. . . . . 6
β’ ((πΉ Fn π΄ β§ π΄ βΌ Ο) β (dom πΉ β V β π΄ β V)) |
6 | 2, 5 | mpbird 257 |
. . . . 5
β’ ((πΉ Fn π΄ β§ π΄ βΌ Ο) β dom πΉ β V) |
7 | | fnfun 6603 |
. . . . . 6
β’ (πΉ Fn π΄ β Fun πΉ) |
8 | 7 | adantr 482 |
. . . . 5
β’ ((πΉ Fn π΄ β§ π΄ βΌ Ο) β Fun πΉ) |
9 | | funrnex 7887 |
. . . . 5
β’ (dom
πΉ β V β (Fun
πΉ β ran πΉ β V)) |
10 | 6, 8, 9 | sylc 65 |
. . . 4
β’ ((πΉ Fn π΄ β§ π΄ βΌ Ο) β ran πΉ β V) |
11 | 2, 10 | xpexd 7686 |
. . 3
β’ ((πΉ Fn π΄ β§ π΄ βΌ Ο) β (π΄ Γ ran πΉ) β V) |
12 | | simpl 484 |
. . . . 5
β’ ((πΉ Fn π΄ β§ π΄ βΌ Ο) β πΉ Fn π΄) |
13 | | dffn3 6682 |
. . . . 5
β’ (πΉ Fn π΄ β πΉ:π΄βΆran πΉ) |
14 | 12, 13 | sylib 217 |
. . . 4
β’ ((πΉ Fn π΄ β§ π΄ βΌ Ο) β πΉ:π΄βΆran πΉ) |
15 | | fssxp 6697 |
. . . 4
β’ (πΉ:π΄βΆran πΉ β πΉ β (π΄ Γ ran πΉ)) |
16 | 14, 15 | syl 17 |
. . 3
β’ ((πΉ Fn π΄ β§ π΄ βΌ Ο) β πΉ β (π΄ Γ ran πΉ)) |
17 | | ssdomg 8941 |
. . 3
β’ ((π΄ Γ ran πΉ) β V β (πΉ β (π΄ Γ ran πΉ) β πΉ βΌ (π΄ Γ ran πΉ))) |
18 | 11, 16, 17 | sylc 65 |
. 2
β’ ((πΉ Fn π΄ β§ π΄ βΌ Ο) β πΉ βΌ (π΄ Γ ran πΉ)) |
19 | | xpdom1g 9014 |
. . . . 5
β’ ((ran
πΉ β V β§ π΄ βΌ Ο) β (π΄ Γ ran πΉ) βΌ (Ο Γ ran πΉ)) |
20 | 10, 19 | sylancom 589 |
. . . 4
β’ ((πΉ Fn π΄ β§ π΄ βΌ Ο) β (π΄ Γ ran πΉ) βΌ (Ο Γ ran πΉ)) |
21 | | omex 9580 |
. . . . 5
β’ Ο
β V |
22 | | fnrndomg 10473 |
. . . . . . 7
β’ (π΄ β V β (πΉ Fn π΄ β ran πΉ βΌ π΄)) |
23 | 2, 12, 22 | sylc 65 |
. . . . . 6
β’ ((πΉ Fn π΄ β§ π΄ βΌ Ο) β ran πΉ βΌ π΄) |
24 | | domtr 8948 |
. . . . . 6
β’ ((ran
πΉ βΌ π΄ β§ π΄ βΌ Ο) β ran πΉ βΌ
Ο) |
25 | 23, 24 | sylancom 589 |
. . . . 5
β’ ((πΉ Fn π΄ β§ π΄ βΌ Ο) β ran πΉ βΌ
Ο) |
26 | | xpdom2g 9013 |
. . . . 5
β’ ((Ο
β V β§ ran πΉ
βΌ Ο) β (Ο Γ ran πΉ) βΌ (Ο Γ
Ο)) |
27 | 21, 25, 26 | sylancr 588 |
. . . 4
β’ ((πΉ Fn π΄ β§ π΄ βΌ Ο) β (Ο Γ
ran πΉ) βΌ (Ο
Γ Ο)) |
28 | | domtr 8948 |
. . . 4
β’ (((π΄ Γ ran πΉ) βΌ (Ο Γ ran πΉ) β§ (Ο Γ ran
πΉ) βΌ (Ο Γ
Ο)) β (π΄ Γ
ran πΉ) βΌ (Ο
Γ Ο)) |
29 | 20, 27, 28 | syl2anc 585 |
. . 3
β’ ((πΉ Fn π΄ β§ π΄ βΌ Ο) β (π΄ Γ ran πΉ) βΌ (Ο Γ
Ο)) |
30 | | xpomen 9952 |
. . 3
β’ (Ο
Γ Ο) β Ο |
31 | | domentr 8954 |
. . 3
β’ (((π΄ Γ ran πΉ) βΌ (Ο Γ Ο) β§
(Ο Γ Ο) β Ο) β (π΄ Γ ran πΉ) βΌ Ο) |
32 | 29, 30, 31 | sylancl 587 |
. 2
β’ ((πΉ Fn π΄ β§ π΄ βΌ Ο) β (π΄ Γ ran πΉ) βΌ Ο) |
33 | | domtr 8948 |
. 2
β’ ((πΉ βΌ (π΄ Γ ran πΉ) β§ (π΄ Γ ran πΉ) βΌ Ο) β πΉ βΌ Ο) |
34 | 18, 32, 33 | syl2anc 585 |
1
β’ ((πΉ Fn π΄ β§ π΄ βΌ Ο) β πΉ βΌ Ο) |