Step | Hyp | Ref
| Expression |
1 | | brdomi 8956 |
. 2
β’ (π΄ βΌ π΅ β βπ π:π΄β1-1βπ΅) |
2 | | reldom 8947 |
. . 3
β’ Rel
βΌ |
3 | 2 | brrelex2i 5732 |
. 2
β’ (π΄ βΌ π΅ β π΅ β V) |
4 | | vex 3476 |
. . . . . . . 8
β’ π β V |
5 | | f1stres 8001 |
. . . . . . . . 9
β’
(1st βΎ ((π΅ β ran π) Γ {π« βͺ ran π΄})):((π΅ β ran π) Γ {π« βͺ ran π΄})βΆ(π΅ β ran π) |
6 | | difexg 5326 |
. . . . . . . . . . 11
β’ (π΅ β V β (π΅ β ran π) β V) |
7 | 6 | adantl 480 |
. . . . . . . . . 10
β’ ((π:π΄β1-1βπ΅ β§ π΅ β V) β (π΅ β ran π) β V) |
8 | | snex 5430 |
. . . . . . . . . 10
β’
{π« βͺ ran π΄} β V |
9 | | xpexg 7739 |
. . . . . . . . . 10
β’ (((π΅ β ran π) β V β§ {π« βͺ ran π΄} β V) β ((π΅ β ran π) Γ {π« βͺ ran π΄}) β V) |
10 | 7, 8, 9 | sylancl 584 |
. . . . . . . . 9
β’ ((π:π΄β1-1βπ΅ β§ π΅ β V) β ((π΅ β ran π) Γ {π« βͺ ran π΄}) β V) |
11 | | fex2 7926 |
. . . . . . . . 9
β’
(((1st βΎ ((π΅ β ran π) Γ {π« βͺ ran π΄})):((π΅ β ran π) Γ {π« βͺ ran π΄})βΆ(π΅ β ran π) β§ ((π΅ β ran π) Γ {π« βͺ ran π΄}) β V β§ (π΅ β ran π) β V) β (1st βΎ
((π΅ β ran π) Γ {π« βͺ ran π΄})) β V) |
12 | 5, 10, 7, 11 | mp3an2i 1464 |
. . . . . . . 8
β’ ((π:π΄β1-1βπ΅ β§ π΅ β V) β (1st βΎ
((π΅ β ran π) Γ {π« βͺ ran π΄})) β V) |
13 | | unexg 7738 |
. . . . . . . 8
β’ ((π β V β§ (1st
βΎ ((π΅ β ran
π) Γ {π« βͺ ran π΄})) β V) β (π βͺ (1st βΎ ((π΅ β ran π) Γ {π« βͺ ran π΄}))) β V) |
14 | 4, 12, 13 | sylancr 585 |
. . . . . . 7
β’ ((π:π΄β1-1βπ΅ β§ π΅ β V) β (π βͺ (1st βΎ ((π΅ β ran π) Γ {π« βͺ ran π΄}))) β V) |
15 | | cnvexg 7917 |
. . . . . . 7
β’ ((π βͺ (1st βΎ
((π΅ β ran π) Γ {π« βͺ ran π΄}))) β V β β‘(π βͺ (1st βΎ ((π΅ β ran π) Γ {π« βͺ ran π΄}))) β V) |
16 | 14, 15 | syl 17 |
. . . . . 6
β’ ((π:π΄β1-1βπ΅ β§ π΅ β V) β β‘(π βͺ (1st βΎ ((π΅ β ran π) Γ {π« βͺ ran π΄}))) β V) |
17 | | rnexg 7897 |
. . . . . 6
β’ (β‘(π βͺ (1st βΎ ((π΅ β ran π) Γ {π« βͺ ran π΄}))) β V β ran β‘(π βͺ (1st βΎ ((π΅ β ran π) Γ {π« βͺ ran π΄}))) β V) |
18 | 16, 17 | syl 17 |
. . . . 5
β’ ((π:π΄β1-1βπ΅ β§ π΅ β V) β ran β‘(π βͺ (1st βΎ ((π΅ β ran π) Γ {π« βͺ ran π΄}))) β V) |
19 | | simpl 481 |
. . . . . . . 8
β’ ((π:π΄β1-1βπ΅ β§ π΅ β V) β π:π΄β1-1βπ΅) |
20 | | f1dm 6790 |
. . . . . . . . . 10
β’ (π:π΄β1-1βπ΅ β dom π = π΄) |
21 | 4 | dmex 7904 |
. . . . . . . . . 10
β’ dom π β V |
22 | 20, 21 | eqeltrrdi 2840 |
. . . . . . . . 9
β’ (π:π΄β1-1βπ΅ β π΄ β V) |
23 | 22 | adantr 479 |
. . . . . . . 8
β’ ((π:π΄β1-1βπ΅ β§ π΅ β V) β π΄ β V) |
24 | | simpr 483 |
. . . . . . . 8
β’ ((π:π΄β1-1βπ΅ β§ π΅ β V) β π΅ β V) |
25 | | eqid 2730 |
. . . . . . . . 9
β’ β‘(π βͺ (1st βΎ ((π΅ β ran π) Γ {π« βͺ ran π΄}))) = β‘(π βͺ (1st βΎ ((π΅ β ran π) Γ {π« βͺ ran π΄}))) |
26 | 25 | domss2 9138 |
. . . . . . . 8
β’ ((π:π΄β1-1βπ΅ β§ π΄ β V β§ π΅ β V) β (β‘(π βͺ (1st βΎ ((π΅ β ran π) Γ {π« βͺ ran π΄}))):π΅β1-1-ontoβran
β‘(π βͺ (1st βΎ ((π΅ β ran π) Γ {π« βͺ ran π΄}))) β§ π΄ β ran β‘(π βͺ (1st βΎ ((π΅ β ran π) Γ {π« βͺ ran π΄}))) β§ (β‘(π βͺ (1st βΎ ((π΅ β ran π) Γ {π« βͺ ran π΄}))) β π) = ( I βΎ π΄))) |
27 | 19, 23, 24, 26 | syl3anc 1369 |
. . . . . . 7
β’ ((π:π΄β1-1βπ΅ β§ π΅ β V) β (β‘(π βͺ (1st βΎ ((π΅ β ran π) Γ {π« βͺ ran π΄}))):π΅β1-1-ontoβran
β‘(π βͺ (1st βΎ ((π΅ β ran π) Γ {π« βͺ ran π΄}))) β§ π΄ β ran β‘(π βͺ (1st βΎ ((π΅ β ran π) Γ {π« βͺ ran π΄}))) β§ (β‘(π βͺ (1st βΎ ((π΅ β ran π) Γ {π« βͺ ran π΄}))) β π) = ( I βΎ π΄))) |
28 | 27 | simp2d 1141 |
. . . . . 6
β’ ((π:π΄β1-1βπ΅ β§ π΅ β V) β π΄ β ran β‘(π βͺ (1st βΎ ((π΅ β ran π) Γ {π« βͺ ran π΄})))) |
29 | 27 | simp1d 1140 |
. . . . . . 7
β’ ((π:π΄β1-1βπ΅ β§ π΅ β V) β β‘(π βͺ (1st βΎ ((π΅ β ran π) Γ {π« βͺ ran π΄}))):π΅β1-1-ontoβran
β‘(π βͺ (1st βΎ ((π΅ β ran π) Γ {π« βͺ ran π΄})))) |
30 | | f1oen3g 8964 |
. . . . . . 7
β’ ((β‘(π βͺ (1st βΎ ((π΅ β ran π) Γ {π« βͺ ran π΄}))) β V β§ β‘(π βͺ (1st βΎ ((π΅ β ran π) Γ {π« βͺ ran π΄}))):π΅β1-1-ontoβran
β‘(π βͺ (1st βΎ ((π΅ β ran π) Γ {π« βͺ ran π΄})))) β π΅ β ran β‘(π βͺ (1st βΎ ((π΅ β ran π) Γ {π« βͺ ran π΄})))) |
31 | 16, 29, 30 | syl2anc 582 |
. . . . . 6
β’ ((π:π΄β1-1βπ΅ β§ π΅ β V) β π΅ β ran β‘(π βͺ (1st βΎ ((π΅ β ran π) Γ {π« βͺ ran π΄})))) |
32 | 28, 31 | jca 510 |
. . . . 5
β’ ((π:π΄β1-1βπ΅ β§ π΅ β V) β (π΄ β ran β‘(π βͺ (1st βΎ ((π΅ β ran π) Γ {π« βͺ ran π΄}))) β§ π΅ β ran β‘(π βͺ (1st βΎ ((π΅ β ran π) Γ {π« βͺ ran π΄}))))) |
33 | | sseq2 4007 |
. . . . . 6
β’ (π₯ = ran β‘(π βͺ (1st βΎ ((π΅ β ran π) Γ {π« βͺ ran π΄}))) β (π΄ β π₯ β π΄ β ran β‘(π βͺ (1st βΎ ((π΅ β ran π) Γ {π« βͺ ran π΄}))))) |
34 | | breq2 5151 |
. . . . . 6
β’ (π₯ = ran β‘(π βͺ (1st βΎ ((π΅ β ran π) Γ {π« βͺ ran π΄}))) β (π΅ β π₯ β π΅ β ran β‘(π βͺ (1st βΎ ((π΅ β ran π) Γ {π« βͺ ran π΄}))))) |
35 | 33, 34 | anbi12d 629 |
. . . . 5
β’ (π₯ = ran β‘(π βͺ (1st βΎ ((π΅ β ran π) Γ {π« βͺ ran π΄}))) β ((π΄ β π₯ β§ π΅ β π₯) β (π΄ β ran β‘(π βͺ (1st βΎ ((π΅ β ran π) Γ {π« βͺ ran π΄}))) β§ π΅ β ran β‘(π βͺ (1st βΎ ((π΅ β ran π) Γ {π« βͺ ran π΄})))))) |
36 | 18, 32, 35 | spcedv 3587 |
. . . 4
β’ ((π:π΄β1-1βπ΅ β§ π΅ β V) β βπ₯(π΄ β π₯ β§ π΅ β π₯)) |
37 | 36 | ex 411 |
. . 3
β’ (π:π΄β1-1βπ΅ β (π΅ β V β βπ₯(π΄ β π₯ β§ π΅ β π₯))) |
38 | 37 | exlimiv 1931 |
. 2
β’
(βπ π:π΄β1-1βπ΅ β (π΅ β V β βπ₯(π΄ β π₯ β§ π΅ β π₯))) |
39 | 1, 3, 38 | sylc 65 |
1
β’ (π΄ βΌ π΅ β βπ₯(π΄ β π₯ β§ π΅ β π₯)) |