Step | Hyp | Ref
| Expression |
1 | | nnfoctbdj.ctb |
. . 3
β’ (π β π βΌ Ο) |
2 | | nnfoctbdj.n0 |
. . 3
β’ (π β π β β
) |
3 | | nnfoctb 43329 |
. . 3
β’ ((π βΌ Ο β§ π β β
) β
βπ π:ββontoβπ) |
4 | 1, 2, 3 | syl2anc 585 |
. 2
β’ (π β βπ π:ββontoβπ) |
5 | | fofn 6763 |
. . . . . . 7
β’ (π:ββontoβπ β π Fn β) |
6 | 5 | adantl 483 |
. . . . . 6
β’ ((π β§ π:ββontoβπ) β π Fn β) |
7 | | nnex 12166 |
. . . . . . 7
β’ β
β V |
8 | 7 | a1i 11 |
. . . . . 6
β’ ((π β§ π:ββontoβπ) β β β V) |
9 | | ltwenn 13874 |
. . . . . . 7
β’ < We
β |
10 | 9 | a1i 11 |
. . . . . 6
β’ ((π β§ π:ββontoβπ) β < We β) |
11 | 6, 8, 10 | wessf1orn 43478 |
. . . . 5
β’ ((π β§ π:ββontoβπ) β βπ₯ β π« β(π βΎ π₯):π₯β1-1-ontoβran
π) |
12 | | elpwi 4572 |
. . . . . . . . 9
β’ (π₯ β π« β β
π₯ β
β) |
13 | 12 | 3ad2ant2 1135 |
. . . . . . . 8
β’ (((π β§ π:ββontoβπ) β§ π₯ β π« β β§ (π βΎ π₯):π₯β1-1-ontoβran
π) β π₯ β
β) |
14 | | simpr 486 |
. . . . . . . . . . 11
β’ ((π:ββontoβπ β§ (π βΎ π₯):π₯β1-1-ontoβran
π) β (π βΎ π₯):π₯β1-1-ontoβran
π) |
15 | | forn 6764 |
. . . . . . . . . . . . 13
β’ (π:ββontoβπ β ran π = π) |
16 | 15 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π:ββontoβπ β§ (π βΎ π₯):π₯β1-1-ontoβran
π) β ran π = π) |
17 | 16 | f1oeq3d 6786 |
. . . . . . . . . . 11
β’ ((π:ββontoβπ β§ (π βΎ π₯):π₯β1-1-ontoβran
π) β ((π βΎ π₯):π₯β1-1-ontoβran
π β (π βΎ π₯):π₯β1-1-ontoβπ)) |
18 | 14, 17 | mpbid 231 |
. . . . . . . . . 10
β’ ((π:ββontoβπ β§ (π βΎ π₯):π₯β1-1-ontoβran
π) β (π βΎ π₯):π₯β1-1-ontoβπ) |
19 | 18 | adantll 713 |
. . . . . . . . 9
β’ (((π β§ π:ββontoβπ) β§ (π βΎ π₯):π₯β1-1-ontoβran
π) β (π βΎ π₯):π₯β1-1-ontoβπ) |
20 | 19 | 3adant2 1132 |
. . . . . . . 8
β’ (((π β§ π:ββontoβπ) β§ π₯ β π« β β§ (π βΎ π₯):π₯β1-1-ontoβran
π) β (π βΎ π₯):π₯β1-1-ontoβπ) |
21 | | nnfoctbdj.dj |
. . . . . . . . . 10
β’ (π β Disj π¦ β π π¦) |
22 | 21 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π:ββontoβπ) β Disj π¦ β π π¦) |
23 | 22 | 3ad2ant1 1134 |
. . . . . . . 8
β’ (((π β§ π:ββontoβπ) β§ π₯ β π« β β§ (π βΎ π₯):π₯β1-1-ontoβran
π) β Disj π¦ β π π¦) |
24 | | eqeq1 2741 |
. . . . . . . . . . 11
β’ (π = π β (π = 1 β π = 1)) |
25 | | oveq1 7369 |
. . . . . . . . . . . . 13
β’ (π = π β (π β 1) = (π β 1)) |
26 | 25 | eleq1d 2823 |
. . . . . . . . . . . 12
β’ (π = π β ((π β 1) β π₯ β (π β 1) β π₯)) |
27 | 26 | notbid 318 |
. . . . . . . . . . 11
β’ (π = π β (Β¬ (π β 1) β π₯ β Β¬ (π β 1) β π₯)) |
28 | 24, 27 | orbi12d 918 |
. . . . . . . . . 10
β’ (π = π β ((π = 1 β¨ Β¬ (π β 1) β π₯) β (π = 1 β¨ Β¬ (π β 1) β π₯))) |
29 | | fvoveq1 7385 |
. . . . . . . . . 10
β’ (π = π β ((π βΎ π₯)β(π β 1)) = ((π βΎ π₯)β(π β 1))) |
30 | 28, 29 | ifbieq2d 4517 |
. . . . . . . . 9
β’ (π = π β if((π = 1 β¨ Β¬ (π β 1) β π₯), β
, ((π βΎ π₯)β(π β 1))) = if((π = 1 β¨ Β¬ (π β 1) β π₯), β
, ((π βΎ π₯)β(π β 1)))) |
31 | 30 | cbvmptv 5223 |
. . . . . . . 8
β’ (π β β β¦
if((π = 1 β¨ Β¬ (π β 1) β π₯), β
, ((π βΎ π₯)β(π β 1)))) = (π β β β¦ if((π = 1 β¨ Β¬ (π β 1) β π₯), β
, ((π βΎ π₯)β(π β 1)))) |
32 | 13, 20, 23, 31 | nnfoctbdjlem 44770 |
. . . . . . 7
β’ (((π β§ π:ββontoβπ) β§ π₯ β π« β β§ (π βΎ π₯):π₯β1-1-ontoβran
π) β βπ(π:ββontoβ(π βͺ {β
}) β§ Disj π β β (πβπ))) |
33 | 32 | 3exp 1120 |
. . . . . 6
β’ ((π β§ π:ββontoβπ) β (π₯ β π« β β ((π βΎ π₯):π₯β1-1-ontoβran
π β βπ(π:ββontoβ(π βͺ {β
}) β§ Disj π β β (πβπ))))) |
34 | 33 | rexlimdv 3151 |
. . . . 5
β’ ((π β§ π:ββontoβπ) β (βπ₯ β π« β(π βΎ π₯):π₯β1-1-ontoβran
π β βπ(π:ββontoβ(π βͺ {β
}) β§ Disj π β β (πβπ)))) |
35 | 11, 34 | mpd 15 |
. . . 4
β’ ((π β§ π:ββontoβπ) β βπ(π:ββontoβ(π βͺ {β
}) β§ Disj π β β (πβπ))) |
36 | 35 | ex 414 |
. . 3
β’ (π β (π:ββontoβπ β βπ(π:ββontoβ(π βͺ {β
}) β§ Disj π β β (πβπ)))) |
37 | 36 | exlimdv 1937 |
. 2
β’ (π β (βπ π:ββontoβπ β βπ(π:ββontoβ(π βͺ {β
}) β§ Disj π β β (πβπ)))) |
38 | 4, 37 | mpd 15 |
1
β’ (π β βπ(π:ββontoβ(π βͺ {β
}) β§ Disj π β β (πβπ))) |