Step | Hyp | Ref
| Expression |
1 | | brdomi 8953 |
. 2
β’ (π΄ βΌ π΅ β βπ π:π΄β1-1βπ΅) |
2 | | reldom 8944 |
. . 3
β’ Rel
βΌ |
3 | 2 | brrelex2i 5733 |
. 2
β’ (π΄ βΌ π΅ β π΅ β V) |
4 | | vex 3478 |
. . . . . . . 8
β’ π β V |
5 | | f1stres 7998 |
. . . . . . . . 9
β’
(1st βΎ ((π΅ β ran π) Γ {π« βͺ ran π΄})):((π΅ β ran π) Γ {π« βͺ ran π΄})βΆ(π΅ β ran π) |
6 | | difexg 5327 |
. . . . . . . . . . 11
β’ (π΅ β V β (π΅ β ran π) β V) |
7 | 6 | adantl 482 |
. . . . . . . . . 10
β’ ((π:π΄β1-1βπ΅ β§ π΅ β V) β (π΅ β ran π) β V) |
8 | | snex 5431 |
. . . . . . . . . 10
β’
{π« βͺ ran π΄} β V |
9 | | xpexg 7736 |
. . . . . . . . . 10
β’ (((π΅ β ran π) β V β§ {π« βͺ ran π΄} β V) β ((π΅ β ran π) Γ {π« βͺ ran π΄}) β V) |
10 | 7, 8, 9 | sylancl 586 |
. . . . . . . . 9
β’ ((π:π΄β1-1βπ΅ β§ π΅ β V) β ((π΅ β ran π) Γ {π« βͺ ran π΄}) β V) |
11 | | fex2 7923 |
. . . . . . . . 9
β’
(((1st βΎ ((π΅ β ran π) Γ {π« βͺ ran π΄})):((π΅ β ran π) Γ {π« βͺ ran π΄})βΆ(π΅ β ran π) β§ ((π΅ β ran π) Γ {π« βͺ ran π΄}) β V β§ (π΅ β ran π) β V) β (1st βΎ
((π΅ β ran π) Γ {π« βͺ ran π΄})) β V) |
12 | 5, 10, 7, 11 | mp3an2i 1466 |
. . . . . . . 8
β’ ((π:π΄β1-1βπ΅ β§ π΅ β V) β (1st βΎ
((π΅ β ran π) Γ {π« βͺ ran π΄})) β V) |
13 | | unexg 7735 |
. . . . . . . 8
β’ ((π β V β§ (1st
βΎ ((π΅ β ran
π) Γ {π« βͺ ran π΄})) β V) β (π βͺ (1st βΎ ((π΅ β ran π) Γ {π« βͺ ran π΄}))) β V) |
14 | 4, 12, 13 | sylancr 587 |
. . . . . . 7
β’ ((π:π΄β1-1βπ΅ β§ π΅ β V) β (π βͺ (1st βΎ ((π΅ β ran π) Γ {π« βͺ ran π΄}))) β V) |
15 | | cnvexg 7914 |
. . . . . . 7
β’ ((π βͺ (1st βΎ
((π΅ β ran π) Γ {π« βͺ ran π΄}))) β V β β‘(π βͺ (1st βΎ ((π΅ β ran π) Γ {π« βͺ ran π΄}))) β V) |
16 | 14, 15 | syl 17 |
. . . . . 6
β’ ((π:π΄β1-1βπ΅ β§ π΅ β V) β β‘(π βͺ (1st βΎ ((π΅ β ran π) Γ {π« βͺ ran π΄}))) β V) |
17 | | rnexg 7894 |
. . . . . 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 483 |
. . . . . . . 8
β’ ((π:π΄β1-1βπ΅ β§ π΅ β V) β π:π΄β1-1βπ΅) |
20 | | f1dm 6791 |
. . . . . . . . . 10
β’ (π:π΄β1-1βπ΅ β dom π = π΄) |
21 | 4 | dmex 7901 |
. . . . . . . . . 10
β’ dom π β V |
22 | 20, 21 | eqeltrrdi 2842 |
. . . . . . . . 9
β’ (π:π΄β1-1βπ΅ β π΄ β V) |
23 | 22 | adantr 481 |
. . . . . . . 8
β’ ((π:π΄β1-1βπ΅ β§ π΅ β V) β π΄ β V) |
24 | | simpr 485 |
. . . . . . . 8
β’ ((π:π΄β1-1βπ΅ β§ π΅ β V) β π΅ β V) |
25 | | eqid 2732 |
. . . . . . . . 9
β’ β‘(π βͺ (1st βΎ ((π΅ β ran π) Γ {π« βͺ ran π΄}))) = β‘(π βͺ (1st βΎ ((π΅ β ran π) Γ {π« βͺ ran π΄}))) |
26 | 25 | domss2 9135 |
. . . . . . . 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 1371 |
. . . . . . 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 1143 |
. . . . . 6
β’ ((π:π΄β1-1βπ΅ β§ π΅ β V) β π΄ β ran β‘(π βͺ (1st βΎ ((π΅ β ran π) Γ {π« βͺ ran π΄})))) |
29 | 27 | simp1d 1142 |
. . . . . . 7
β’ ((π:π΄β1-1βπ΅ β§ π΅ β V) β β‘(π βͺ (1st βΎ ((π΅ β ran π) Γ {π« βͺ ran π΄}))):π΅β1-1-ontoβran
β‘(π βͺ (1st βΎ ((π΅ β ran π) Γ {π« βͺ ran π΄})))) |
30 | | f1oen3g 8961 |
. . . . . . 7
β’ ((β‘(π βͺ (1st βΎ ((π΅ β ran π) Γ {π« βͺ ran π΄}))) β V β§ β‘(π βͺ (1st βΎ ((π΅ β ran π) Γ {π« βͺ ran π΄}))):π΅β1-1-ontoβran
β‘(π βͺ (1st βΎ ((π΅ β ran π) Γ {π« βͺ ran π΄})))) β π΅ β ran β‘(π βͺ (1st βΎ ((π΅ β ran π) Γ {π« βͺ ran π΄})))) |
31 | 16, 29, 30 | syl2anc 584 |
. . . . . 6
β’ ((π:π΄β1-1βπ΅ β§ π΅ β V) β π΅ β ran β‘(π βͺ (1st βΎ ((π΅ β ran π) Γ {π« βͺ ran π΄})))) |
32 | 28, 31 | jca 512 |
. . . . 5
β’ ((π:π΄β1-1βπ΅ β§ π΅ β V) β (π΄ β ran β‘(π βͺ (1st βΎ ((π΅ β ran π) Γ {π« βͺ ran π΄}))) β§ π΅ β ran β‘(π βͺ (1st βΎ ((π΅ β ran π) Γ {π« βͺ ran π΄}))))) |
33 | | sseq2 4008 |
. . . . . 6
β’ (π₯ = ran β‘(π βͺ (1st βΎ ((π΅ β ran π) Γ {π« βͺ ran π΄}))) β (π΄ β π₯ β π΄ β ran β‘(π βͺ (1st βΎ ((π΅ β ran π) Γ {π« βͺ ran π΄}))))) |
34 | | breq2 5152 |
. . . . . 6
β’ (π₯ = ran β‘(π βͺ (1st βΎ ((π΅ β ran π) Γ {π« βͺ ran π΄}))) β (π΅ β π₯ β π΅ β ran β‘(π βͺ (1st βΎ ((π΅ β ran π) Γ {π« βͺ ran π΄}))))) |
35 | 33, 34 | anbi12d 631 |
. . . . 5
β’ (π₯ = ran β‘(π βͺ (1st βΎ ((π΅ β ran π) Γ {π« βͺ ran π΄}))) β ((π΄ β π₯ β§ π΅ β π₯) β (π΄ β ran β‘(π βͺ (1st βΎ ((π΅ β ran π) Γ {π« βͺ ran π΄}))) β§ π΅ β ran β‘(π βͺ (1st βΎ ((π΅ β ran π) Γ {π« βͺ ran π΄})))))) |
36 | 18, 32, 35 | spcedv 3588 |
. . . 4
β’ ((π:π΄β1-1βπ΅ β§ π΅ β V) β βπ₯(π΄ β π₯ β§ π΅ β π₯)) |
37 | 36 | ex 413 |
. . 3
β’ (π:π΄β1-1βπ΅ β (π΅ β V β βπ₯(π΄ β π₯ β§ π΅ β π₯))) |
38 | 37 | exlimiv 1933 |
. 2
β’
(βπ π:π΄β1-1βπ΅ β (π΅ β V β βπ₯(π΄ β π₯ β§ π΅ β π₯))) |
39 | 1, 3, 38 | sylc 65 |
1
β’ (π΄ βΌ π΅ β βπ₯(π΄ β π₯ β§ π΅ β π₯)) |