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