Step | Hyp | Ref
| Expression |
1 | | sdomdom 8927 |
. . 3
β’ (π΄ βΊ π΅ β π΄ βΌ π΅) |
2 | | brdomi 8905 |
. . 3
β’ (π΄ βΌ π΅ β βπ π:π΄β1-1βπ΅) |
3 | 1, 2 | syl 17 |
. 2
β’ (π΄ βΊ π΅ β βπ π:π΄β1-1βπ΅) |
4 | | relsdom 8897 |
. . . . . . 7
β’ Rel
βΊ |
5 | 4 | brrelex1i 5693 |
. . . . . 6
β’ (π΄ βΊ π΅ β π΄ β V) |
6 | 5 | adantr 482 |
. . . . 5
β’ ((π΄ βΊ π΅ β§ π:π΄β1-1βπ΅) β π΄ β V) |
7 | | vex 3452 |
. . . . . . 7
β’ π β V |
8 | 7 | rnex 7854 |
. . . . . 6
β’ ran π β V |
9 | 8 | a1i 11 |
. . . . 5
β’ ((π΄ βΊ π΅ β§ π:π΄β1-1βπ΅) β ran π β V) |
10 | | f1f1orn 6800 |
. . . . . . 7
β’ (π:π΄β1-1βπ΅ β π:π΄β1-1-ontoβran
π) |
11 | 10 | adantl 483 |
. . . . . 6
β’ ((π΄ βΊ π΅ β§ π:π΄β1-1βπ΅) β π:π΄β1-1-ontoβran
π) |
12 | | f1of1 6788 |
. . . . . 6
β’ (π:π΄β1-1-ontoβran
π β π:π΄β1-1βran π) |
13 | 11, 12 | syl 17 |
. . . . 5
β’ ((π΄ βΊ π΅ β§ π:π΄β1-1βπ΅) β π:π΄β1-1βran π) |
14 | | f1dom2g 8916 |
. . . . 5
β’ ((π΄ β V β§ ran π β V β§ π:π΄β1-1βran π) β π΄ βΌ ran π) |
15 | 6, 9, 13, 14 | syl3anc 1372 |
. . . 4
β’ ((π΄ βΊ π΅ β§ π:π΄β1-1βπ΅) β π΄ βΌ ran π) |
16 | | sdomnen 8928 |
. . . . . . . 8
β’ (π΄ βΊ π΅ β Β¬ π΄ β π΅) |
17 | 16 | adantr 482 |
. . . . . . 7
β’ ((π΄ βΊ π΅ β§ π:π΄β1-1βπ΅) β Β¬ π΄ β π΅) |
18 | | ssdif0 4328 |
. . . . . . . 8
β’ (π΅ β ran π β (π΅ β ran π) = β
) |
19 | | simplr 768 |
. . . . . . . . . . 11
β’ (((π΄ βΊ π΅ β§ π:π΄β1-1βπ΅) β§ π΅ β ran π) β π:π΄β1-1βπ΅) |
20 | | f1f 6743 |
. . . . . . . . . . . . . 14
β’ (π:π΄β1-1βπ΅ β π:π΄βΆπ΅) |
21 | 20 | frnd 6681 |
. . . . . . . . . . . . 13
β’ (π:π΄β1-1βπ΅ β ran π β π΅) |
22 | 19, 21 | syl 17 |
. . . . . . . . . . . 12
β’ (((π΄ βΊ π΅ β§ π:π΄β1-1βπ΅) β§ π΅ β ran π) β ran π β π΅) |
23 | | simpr 486 |
. . . . . . . . . . . 12
β’ (((π΄ βΊ π΅ β§ π:π΄β1-1βπ΅) β§ π΅ β ran π) β π΅ β ran π) |
24 | 22, 23 | eqssd 3966 |
. . . . . . . . . . 11
β’ (((π΄ βΊ π΅ β§ π:π΄β1-1βπ΅) β§ π΅ β ran π) β ran π = π΅) |
25 | | dff1o5 6798 |
. . . . . . . . . . 11
β’ (π:π΄β1-1-ontoβπ΅ β (π:π΄β1-1βπ΅ β§ ran π = π΅)) |
26 | 19, 24, 25 | sylanbrc 584 |
. . . . . . . . . 10
β’ (((π΄ βΊ π΅ β§ π:π΄β1-1βπ΅) β§ π΅ β ran π) β π:π΄β1-1-ontoβπ΅) |
27 | | f1oen3g 8913 |
. . . . . . . . . 10
β’ ((π β V β§ π:π΄β1-1-ontoβπ΅) β π΄ β π΅) |
28 | 7, 26, 27 | sylancr 588 |
. . . . . . . . 9
β’ (((π΄ βΊ π΅ β§ π:π΄β1-1βπ΅) β§ π΅ β ran π) β π΄ β π΅) |
29 | 28 | ex 414 |
. . . . . . . 8
β’ ((π΄ βΊ π΅ β§ π:π΄β1-1βπ΅) β (π΅ β ran π β π΄ β π΅)) |
30 | 18, 29 | biimtrrid 242 |
. . . . . . 7
β’ ((π΄ βΊ π΅ β§ π:π΄β1-1βπ΅) β ((π΅ β ran π) = β
β π΄ β π΅)) |
31 | 17, 30 | mtod 197 |
. . . . . 6
β’ ((π΄ βΊ π΅ β§ π:π΄β1-1βπ΅) β Β¬ (π΅ β ran π) = β
) |
32 | | neq0 4310 |
. . . . . 6
β’ (Β¬
(π΅ β ran π) = β
β βπ€ π€ β (π΅ β ran π)) |
33 | 31, 32 | sylib 217 |
. . . . 5
β’ ((π΄ βΊ π΅ β§ π:π΄β1-1βπ΅) β βπ€ π€ β (π΅ β ran π)) |
34 | | snssi 4773 |
. . . . . . 7
β’ (π€ β (π΅ β ran π) β {π€} β (π΅ β ran π)) |
35 | | vex 3452 |
. . . . . . . . 9
β’ π€ β V |
36 | | en2sn 8992 |
. . . . . . . . 9
β’ ((π΄ β V β§ π€ β V) β {π΄} β {π€}) |
37 | 6, 35, 36 | sylancl 587 |
. . . . . . . 8
β’ ((π΄ βΊ π΅ β§ π:π΄β1-1βπ΅) β {π΄} β {π€}) |
38 | 4 | brrelex2i 5694 |
. . . . . . . . . 10
β’ (π΄ βΊ π΅ β π΅ β V) |
39 | 38 | adantr 482 |
. . . . . . . . 9
β’ ((π΄ βΊ π΅ β§ π:π΄β1-1βπ΅) β π΅ β V) |
40 | | difexg 5289 |
. . . . . . . . 9
β’ (π΅ β V β (π΅ β ran π) β V) |
41 | | ssdomg 8947 |
. . . . . . . . 9
β’ ((π΅ β ran π) β V β ({π€} β (π΅ β ran π) β {π€} βΌ (π΅ β ran π))) |
42 | 39, 40, 41 | 3syl 18 |
. . . . . . . 8
β’ ((π΄ βΊ π΅ β§ π:π΄β1-1βπ΅) β ({π€} β (π΅ β ran π) β {π€} βΌ (π΅ β ran π))) |
43 | | endomtr 8959 |
. . . . . . . 8
β’ (({π΄} β {π€} β§ {π€} βΌ (π΅ β ran π)) β {π΄} βΌ (π΅ β ran π)) |
44 | 37, 42, 43 | syl6an 683 |
. . . . . . 7
β’ ((π΄ βΊ π΅ β§ π:π΄β1-1βπ΅) β ({π€} β (π΅ β ran π) β {π΄} βΌ (π΅ β ran π))) |
45 | 34, 44 | syl5 34 |
. . . . . 6
β’ ((π΄ βΊ π΅ β§ π:π΄β1-1βπ΅) β (π€ β (π΅ β ran π) β {π΄} βΌ (π΅ β ran π))) |
46 | 45 | exlimdv 1937 |
. . . . 5
β’ ((π΄ βΊ π΅ β§ π:π΄β1-1βπ΅) β (βπ€ π€ β (π΅ β ran π) β {π΄} βΌ (π΅ β ran π))) |
47 | 33, 46 | mpd 15 |
. . . 4
β’ ((π΄ βΊ π΅ β§ π:π΄β1-1βπ΅) β {π΄} βΌ (π΅ β ran π)) |
48 | | disjdif 4436 |
. . . . 5
β’ (ran
π β© (π΅ β ran π)) = β
|
49 | 48 | a1i 11 |
. . . 4
β’ ((π΄ βΊ π΅ β§ π:π΄β1-1βπ΅) β (ran π β© (π΅ β ran π)) = β
) |
50 | | undom 9010 |
. . . 4
β’ (((π΄ βΌ ran π β§ {π΄} βΌ (π΅ β ran π)) β§ (ran π β© (π΅ β ran π)) = β
) β (π΄ βͺ {π΄}) βΌ (ran π βͺ (π΅ β ran π))) |
51 | 15, 47, 49, 50 | syl21anc 837 |
. . 3
β’ ((π΄ βΊ π΅ β§ π:π΄β1-1βπ΅) β (π΄ βͺ {π΄}) βΌ (ran π βͺ (π΅ β ran π))) |
52 | | df-suc 6328 |
. . . 4
β’ suc π΄ = (π΄ βͺ {π΄}) |
53 | 52 | a1i 11 |
. . 3
β’ ((π΄ βΊ π΅ β§ π:π΄β1-1βπ΅) β suc π΄ = (π΄ βͺ {π΄})) |
54 | | undif2 4441 |
. . . 4
β’ (ran
π βͺ (π΅ β ran π)) = (ran π βͺ π΅) |
55 | 21 | adantl 483 |
. . . . 5
β’ ((π΄ βΊ π΅ β§ π:π΄β1-1βπ΅) β ran π β π΅) |
56 | | ssequn1 4145 |
. . . . 5
β’ (ran
π β π΅ β (ran π βͺ π΅) = π΅) |
57 | 55, 56 | sylib 217 |
. . . 4
β’ ((π΄ βΊ π΅ β§ π:π΄β1-1βπ΅) β (ran π βͺ π΅) = π΅) |
58 | 54, 57 | eqtr2id 2790 |
. . 3
β’ ((π΄ βΊ π΅ β§ π:π΄β1-1βπ΅) β π΅ = (ran π βͺ (π΅ β ran π))) |
59 | 51, 53, 58 | 3brtr4d 5142 |
. 2
β’ ((π΄ βΊ π΅ β§ π:π΄β1-1βπ΅) β suc π΄ βΌ π΅) |
60 | 3, 59 | exlimddv 1939 |
1
β’ (π΄ βΊ π΅ β suc π΄ βΌ π΅) |