Step | Hyp | Ref
| Expression |
1 | | nnfoctb 43343 |
. 2
β’ ((π΄ βΌ Ο β§ π΄ β β
) β
βπ π:ββontoβπ΄) |
2 | | fofn 6759 |
. . . . . 6
β’ (π:ββontoβπ΄ β π Fn β) |
3 | | nnex 12164 |
. . . . . . 7
β’ β
β V |
4 | 3 | a1i 11 |
. . . . . 6
β’ (π:ββontoβπ΄ β β β V) |
5 | | ltwenn 13873 |
. . . . . . 7
β’ < We
β |
6 | 5 | a1i 11 |
. . . . . 6
β’ (π:ββontoβπ΄ β < We β) |
7 | 2, 4, 6 | wessf1orn 43492 |
. . . . 5
β’ (π:ββontoβπ΄ β βπ₯ β π« β(π βΎ π₯):π₯β1-1-ontoβran
π) |
8 | | f1odm 6789 |
. . . . . . . . . . 11
β’ ((π βΎ π₯):π₯β1-1-ontoβran
π β dom (π βΎ π₯) = π₯) |
9 | 8 | adantl 483 |
. . . . . . . . . 10
β’ ((π₯ β π« β β§
(π βΎ π₯):π₯β1-1-ontoβran
π) β dom (π βΎ π₯) = π₯) |
10 | | elpwi 4568 |
. . . . . . . . . . 11
β’ (π₯ β π« β β
π₯ β
β) |
11 | 10 | adantr 482 |
. . . . . . . . . 10
β’ ((π₯ β π« β β§
(π βΎ π₯):π₯β1-1-ontoβran
π) β π₯ β
β) |
12 | 9, 11 | eqsstrd 3983 |
. . . . . . . . 9
β’ ((π₯ β π« β β§
(π βΎ π₯):π₯β1-1-ontoβran
π) β dom (π βΎ π₯) β β) |
13 | 12 | 3adant1 1131 |
. . . . . . . 8
β’ ((π:ββontoβπ΄ β§ π₯ β π« β β§ (π βΎ π₯):π₯β1-1-ontoβran
π) β dom (π βΎ π₯) β β) |
14 | | simpr 486 |
. . . . . . . . . 10
β’ ((π:ββontoβπ΄ β§ (π βΎ π₯):π₯β1-1-ontoβran
π) β (π βΎ π₯):π₯β1-1-ontoβran
π) |
15 | | eqidd 2734 |
. . . . . . . . . . 11
β’ ((π:ββontoβπ΄ β§ (π βΎ π₯):π₯β1-1-ontoβran
π) β (π βΎ π₯) = (π βΎ π₯)) |
16 | 8 | eqcomd 2739 |
. . . . . . . . . . . 12
β’ ((π βΎ π₯):π₯β1-1-ontoβran
π β π₯ = dom (π βΎ π₯)) |
17 | 16 | adantl 483 |
. . . . . . . . . . 11
β’ ((π:ββontoβπ΄ β§ (π βΎ π₯):π₯β1-1-ontoβran
π) β π₯ = dom (π βΎ π₯)) |
18 | | forn 6760 |
. . . . . . . . . . . 12
β’ (π:ββontoβπ΄ β ran π = π΄) |
19 | 18 | adantr 482 |
. . . . . . . . . . 11
β’ ((π:ββontoβπ΄ β§ (π βΎ π₯):π₯β1-1-ontoβran
π) β ran π = π΄) |
20 | 15, 17, 19 | f1oeq123d 6779 |
. . . . . . . . . 10
β’ ((π:ββontoβπ΄ β§ (π βΎ π₯):π₯β1-1-ontoβran
π) β ((π βΎ π₯):π₯β1-1-ontoβran
π β (π βΎ π₯):dom (π βΎ π₯)β1-1-ontoβπ΄)) |
21 | 14, 20 | mpbid 231 |
. . . . . . . . 9
β’ ((π:ββontoβπ΄ β§ (π βΎ π₯):π₯β1-1-ontoβran
π) β (π βΎ π₯):dom (π βΎ π₯)β1-1-ontoβπ΄) |
22 | 21 | 3adant2 1132 |
. . . . . . . 8
β’ ((π:ββontoβπ΄ β§ π₯ β π« β β§ (π βΎ π₯):π₯β1-1-ontoβran
π) β (π βΎ π₯):dom (π βΎ π₯)β1-1-ontoβπ΄) |
23 | | vex 3448 |
. . . . . . . . . 10
β’ π β V |
24 | 23 | resex 5986 |
. . . . . . . . 9
β’ (π βΎ π₯) β V |
25 | | dmeq 5860 |
. . . . . . . . . . 11
β’ (π = (π βΎ π₯) β dom π = dom (π βΎ π₯)) |
26 | 25 | sseq1d 3976 |
. . . . . . . . . 10
β’ (π = (π βΎ π₯) β (dom π β β β dom (π βΎ π₯) β β)) |
27 | | id 22 |
. . . . . . . . . . 11
β’ (π = (π βΎ π₯) β π = (π βΎ π₯)) |
28 | | eqidd 2734 |
. . . . . . . . . . 11
β’ (π = (π βΎ π₯) β π΄ = π΄) |
29 | 27, 25, 28 | f1oeq123d 6779 |
. . . . . . . . . 10
β’ (π = (π βΎ π₯) β (π:dom πβ1-1-ontoβπ΄ β (π βΎ π₯):dom (π βΎ π₯)β1-1-ontoβπ΄)) |
30 | 26, 29 | anbi12d 632 |
. . . . . . . . 9
β’ (π = (π βΎ π₯) β ((dom π β β β§ π:dom πβ1-1-ontoβπ΄) β (dom (π βΎ π₯) β β β§ (π βΎ π₯):dom (π βΎ π₯)β1-1-ontoβπ΄))) |
31 | 24, 30 | spcev 3564 |
. . . . . . . 8
β’ ((dom
(π βΎ π₯) β β β§ (π βΎ π₯):dom (π βΎ π₯)β1-1-ontoβπ΄) β βπ(dom π β β β§ π:dom πβ1-1-ontoβπ΄)) |
32 | 13, 22, 31 | syl2anc 585 |
. . . . . . 7
β’ ((π:ββontoβπ΄ β§ π₯ β π« β β§ (π βΎ π₯):π₯β1-1-ontoβran
π) β βπ(dom π β β β§ π:dom πβ1-1-ontoβπ΄)) |
33 | 32 | 3exp 1120 |
. . . . . 6
β’ (π:ββontoβπ΄ β (π₯ β π« β β ((π βΎ π₯):π₯β1-1-ontoβran
π β βπ(dom π β β β§ π:dom πβ1-1-ontoβπ΄)))) |
34 | 33 | rexlimdv 3147 |
. . . . 5
β’ (π:ββontoβπ΄ β (βπ₯ β π« β(π βΎ π₯):π₯β1-1-ontoβran
π β βπ(dom π β β β§ π:dom πβ1-1-ontoβπ΄))) |
35 | 7, 34 | mpd 15 |
. . . 4
β’ (π:ββontoβπ΄ β βπ(dom π β β β§ π:dom πβ1-1-ontoβπ΄)) |
36 | 35 | a1i 11 |
. . 3
β’ ((π΄ βΌ Ο β§ π΄ β β
) β (π:ββontoβπ΄ β βπ(dom π β β β§ π:dom πβ1-1-ontoβπ΄))) |
37 | 36 | exlimdv 1937 |
. 2
β’ ((π΄ βΌ Ο β§ π΄ β β
) β
(βπ π:ββontoβπ΄ β βπ(dom π β β β§ π:dom πβ1-1-ontoβπ΄))) |
38 | 1, 37 | mpd 15 |
1
β’ ((π΄ βΌ Ο β§ π΄ β β
) β
βπ(dom π β β β§ π:dom πβ1-1-ontoβπ΄)) |