Step | Hyp | Ref
| Expression |
1 | | brdomi 8954 |
. 2
β’ (π΄ βΌ π΅ β βπ π:π΄β1-1βπ΅) |
2 | | reldom 8945 |
. . 3
β’ Rel
βΌ |
3 | 2 | brrelex2i 5734 |
. 2
β’ (π΄ βΌ π΅ β π΅ β V) |
4 | | vex 3479 |
. . . . . . . 8
β’ π β V |
5 | | f1stres 7999 |
. . . . . . . . 9
β’
(1st βΎ ((π΅ β ran π) Γ {π« βͺ ran π΄})):((π΅ β ran π) Γ {π« βͺ ran π΄})βΆ(π΅ β ran π) |
6 | | difexg 5328 |
. . . . . . . . . . 11
β’ (π΅ β V β (π΅ β ran π) β V) |
7 | 6 | adantl 483 |
. . . . . . . . . 10
β’ ((π:π΄β1-1βπ΅ β§ π΅ β V) β (π΅ β ran π) β V) |
8 | | snex 5432 |
. . . . . . . . . 10
β’
{π« βͺ ran π΄} β V |
9 | | xpexg 7737 |
. . . . . . . . . 10
β’ (((π΅ β ran π) β V β§ {π« βͺ ran π΄} β V) β ((π΅ β ran π) Γ {π« βͺ ran π΄}) β V) |
10 | 7, 8, 9 | sylancl 587 |
. . . . . . . . 9
β’ ((π:π΄β1-1βπ΅ β§ π΅ β V) β ((π΅ β ran π) Γ {π« βͺ ran π΄}) β V) |
11 | | fex2 7924 |
. . . . . . . . 9
β’
(((1st βΎ ((π΅ β ran π) Γ {π« βͺ ran π΄})):((π΅ β ran π) Γ {π« βͺ ran π΄})βΆ(π΅ β ran π) β§ ((π΅ β ran π) Γ {π« βͺ ran π΄}) β V β§ (π΅ β ran π) β V) β (1st βΎ
((π΅ β ran π) Γ {π« βͺ ran π΄})) β V) |
12 | 5, 10, 7, 11 | mp3an2i 1467 |
. . . . . . . 8
β’ ((π:π΄β1-1βπ΅ β§ π΅ β V) β (1st βΎ
((π΅ β ran π) Γ {π« βͺ ran π΄})) β V) |
13 | | unexg 7736 |
. . . . . . . 8
β’ ((π β V β§ (1st
βΎ ((π΅ β ran
π) Γ {π« βͺ ran π΄})) β V) β (π βͺ (1st βΎ ((π΅ β ran π) Γ {π« βͺ ran π΄}))) β V) |
14 | 4, 12, 13 | sylancr 588 |
. . . . . . 7
β’ ((π:π΄β1-1βπ΅ β§ π΅ β V) β (π βͺ (1st βΎ ((π΅ β ran π) Γ {π« βͺ ran π΄}))) β V) |
15 | | cnvexg 7915 |
. . . . . . 7
β’ ((π βͺ (1st βΎ
((π΅ β ran π) Γ {π« βͺ ran π΄}))) β V β β‘(π βͺ (1st βΎ ((π΅ β ran π) Γ {π« βͺ ran π΄}))) β V) |
16 | 14, 15 | syl 17 |
. . . . . 6
β’ ((π:π΄β1-1βπ΅ β§ π΅ β V) β β‘(π βͺ (1st βΎ ((π΅ β ran π) Γ {π« βͺ ran π΄}))) β V) |
17 | | rnexg 7895 |
. . . . . 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 484 |
. . . . . . . 8
β’ ((π:π΄β1-1βπ΅ β§ π΅ β V) β π:π΄β1-1βπ΅) |
20 | | f1dm 6792 |
. . . . . . . . . 10
β’ (π:π΄β1-1βπ΅ β dom π = π΄) |
21 | 4 | dmex 7902 |
. . . . . . . . . 10
β’ dom π β V |
22 | 20, 21 | eqeltrrdi 2843 |
. . . . . . . . 9
β’ (π:π΄β1-1βπ΅ β π΄ β V) |
23 | 22 | adantr 482 |
. . . . . . . 8
β’ ((π:π΄β1-1βπ΅ β§ π΅ β V) β π΄ β V) |
24 | | simpr 486 |
. . . . . . . 8
β’ ((π:π΄β1-1βπ΅ β§ π΅ β V) β π΅ β V) |
25 | | eqid 2733 |
. . . . . . . . 9
β’ β‘(π βͺ (1st βΎ ((π΅ β ran π) Γ {π« βͺ ran π΄}))) = β‘(π βͺ (1st βΎ ((π΅ β ran π) Γ {π« βͺ ran π΄}))) |
26 | 25 | domss2 9136 |
. . . . . . . 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 1372 |
. . . . . . 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 1144 |
. . . . . 6
β’ ((π:π΄β1-1βπ΅ β§ π΅ β V) β π΄ β ran β‘(π βͺ (1st βΎ ((π΅ β ran π) Γ {π« βͺ ran π΄})))) |
29 | 27 | simp1d 1143 |
. . . . . . 7
β’ ((π:π΄β1-1βπ΅ β§ π΅ β V) β β‘(π βͺ (1st βΎ ((π΅ β ran π) Γ {π« βͺ ran π΄}))):π΅β1-1-ontoβran
β‘(π βͺ (1st βΎ ((π΅ β ran π) Γ {π« βͺ ran π΄})))) |
30 | | f1oen3g 8962 |
. . . . . . 7
β’ ((β‘(π βͺ (1st βΎ ((π΅ β ran π) Γ {π« βͺ ran π΄}))) β V β§ β‘(π βͺ (1st βΎ ((π΅ β ran π) Γ {π« βͺ ran π΄}))):π΅β1-1-ontoβran
β‘(π βͺ (1st βΎ ((π΅ β ran π) Γ {π« βͺ ran π΄})))) β π΅ β ran β‘(π βͺ (1st βΎ ((π΅ β ran π) Γ {π« βͺ ran π΄})))) |
31 | 16, 29, 30 | syl2anc 585 |
. . . . . 6
β’ ((π:π΄β1-1βπ΅ β§ π΅ β V) β π΅ β ran β‘(π βͺ (1st βΎ ((π΅ β ran π) Γ {π« βͺ ran π΄})))) |
32 | 28, 31 | jca 513 |
. . . . 5
β’ ((π:π΄β1-1βπ΅ β§ π΅ β V) β (π΄ β ran β‘(π βͺ (1st βΎ ((π΅ β ran π) Γ {π« βͺ ran π΄}))) β§ π΅ β ran β‘(π βͺ (1st βΎ ((π΅ β ran π) Γ {π« βͺ ran π΄}))))) |
33 | | sseq2 4009 |
. . . . . 6
β’ (π₯ = ran β‘(π βͺ (1st βΎ ((π΅ β ran π) Γ {π« βͺ ran π΄}))) β (π΄ β π₯ β π΄ β ran β‘(π βͺ (1st βΎ ((π΅ β ran π) Γ {π« βͺ ran π΄}))))) |
34 | | breq2 5153 |
. . . . . 6
β’ (π₯ = ran β‘(π βͺ (1st βΎ ((π΅ β ran π) Γ {π« βͺ ran π΄}))) β (π΅ β π₯ β π΅ β ran β‘(π βͺ (1st βΎ ((π΅ β ran π) Γ {π« βͺ ran π΄}))))) |
35 | 33, 34 | anbi12d 632 |
. . . . 5
β’ (π₯ = ran β‘(π βͺ (1st βΎ ((π΅ β ran π) Γ {π« βͺ ran π΄}))) β ((π΄ β π₯ β§ π΅ β π₯) β (π΄ β ran β‘(π βͺ (1st βΎ ((π΅ β ran π) Γ {π« βͺ ran π΄}))) β§ π΅ β ran β‘(π βͺ (1st βΎ ((π΅ β ran π) Γ {π« βͺ ran π΄})))))) |
36 | 18, 32, 35 | spcedv 3589 |
. . . 4
β’ ((π:π΄β1-1βπ΅ β§ π΅ β V) β βπ₯(π΄ β π₯ β§ π΅ β π₯)) |
37 | 36 | ex 414 |
. . 3
β’ (π:π΄β1-1βπ΅ β (π΅ β V β βπ₯(π΄ β π₯ β§ π΅ β π₯))) |
38 | 37 | exlimiv 1934 |
. 2
β’
(βπ π:π΄β1-1βπ΅ β (π΅ β V β βπ₯(π΄ β π₯ β§ π΅ β π₯))) |
39 | 1, 3, 38 | sylc 65 |
1
β’ (π΄ βΌ π΅ β βπ₯(π΄ β π₯ β§ π΅ β π₯)) |