Step | Hyp | Ref
| Expression |
1 | | ralcom 3271 |
. . 3
β’
(βπ β
π΄ βπ β π΅ π <s π β βπ β π΅ βπ β π΄ π <s π) |
2 | | simplll 774 |
. . . . . 6
β’ ((((π΄ β
No β§ π΄ β
V) β§ (π΅ β No β§ π΅ β V)) β§ π β π΅) β π΄ β No
) |
3 | | simpllr 775 |
. . . . . 6
β’ ((((π΄ β
No β§ π΄ β
V) β§ (π΅ β No β§ π΅ β V)) β§ π β π΅) β π΄ β V) |
4 | | simprl 770 |
. . . . . . 7
β’ (((π΄ β
No β§ π΄ β
V) β§ (π΅ β No β§ π΅ β V)) β π΅ β No
) |
5 | 4 | sselda 3945 |
. . . . . 6
β’ ((((π΄ β
No β§ π΄ β
V) β§ (π΅ β No β§ π΅ β V)) β§ π β π΅) β π β No
) |
6 | | noetasuplem.1 |
. . . . . . 7
β’ π = if(βπ₯ β π΄ βπ¦ β π΄ Β¬ π₯ <s π¦, ((β©π₯ β π΄ βπ¦ β π΄ Β¬ π₯ <s π¦) βͺ {β¨dom (β©π₯ β π΄ βπ¦ β π΄ Β¬ π₯ <s π¦), 2oβ©}), (π β {π¦ β£ βπ’ β π΄ (π¦ β dom π’ β§ βπ£ β π΄ (Β¬ π£ <s π’ β (π’ βΎ suc π¦) = (π£ βΎ suc π¦)))} β¦ (β©π₯βπ’ β π΄ (π β dom π’ β§ βπ£ β π΄ (Β¬ π£ <s π’ β (π’ βΎ suc π) = (π£ βΎ suc π)) β§ (π’βπ) = π₯)))) |
7 | 6 | nosupbnd2 27080 |
. . . . . 6
β’ ((π΄ β
No β§ π΄ β V
β§ π β No ) β (βπ β π΄ π <s π β Β¬ (π βΎ dom π) <s π)) |
8 | 2, 3, 5, 7 | syl3anc 1372 |
. . . . 5
β’ ((((π΄ β
No β§ π΄ β
V) β§ (π΅ β No β§ π΅ β V)) β§ π β π΅) β (βπ β π΄ π <s π β Β¬ (π βΎ dom π) <s π)) |
9 | | simpl 484 |
. . . . . . . . . . 11
β’ ((π β π΅ β§ Β¬ (π βΎ dom π) <s π) β π β π΅) |
10 | | ssel2 3940 |
. . . . . . . . . . 11
β’ ((π΅ β
No β§ π β
π΅) β π β
No ) |
11 | 4, 9, 10 | syl2an 597 |
. . . . . . . . . 10
β’ ((((π΄ β
No β§ π΄ β
V) β§ (π΅ β No β§ π΅ β V)) β§ (π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β π β No
) |
12 | | nodmord 27017 |
. . . . . . . . . 10
β’ (π β
No β Ord dom π) |
13 | | ordirr 6336 |
. . . . . . . . . 10
β’ (Ord dom
π β Β¬ dom π β dom π) |
14 | 11, 12, 13 | 3syl 18 |
. . . . . . . . 9
β’ ((((π΄ β
No β§ π΄ β
V) β§ (π΅ β No β§ π΅ β V)) β§ (π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β Β¬ dom π β dom π) |
15 | | ssun2 4134 |
. . . . . . . . . . 11
β’ suc βͺ ( bday β π΅) β (dom π βͺ suc βͺ
( bday β π΅)) |
16 | | bdayval 27012 |
. . . . . . . . . . . . . . 15
β’ (π β
No β ( bday βπ) = dom π) |
17 | 11, 16 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((((π΄ β
No β§ π΄ β
V) β§ (π΅ β No β§ π΅ β V)) β§ (π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β ( bday
βπ) = dom
π) |
18 | | bdayfo 27041 |
. . . . . . . . . . . . . . . . 17
β’ bday : No βontoβOn |
19 | | fofn 6759 |
. . . . . . . . . . . . . . . . 17
β’ ( bday : No βontoβOn β bday
Fn No ) |
20 | 18, 19 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
β’ bday Fn No
|
21 | | fnfvima 7184 |
. . . . . . . . . . . . . . . 16
β’ (( bday Fn No β§ π΅ β
No β§ π β
π΅) β ( bday βπ) β ( bday
β π΅)) |
22 | 20, 21 | mp3an1 1449 |
. . . . . . . . . . . . . . 15
β’ ((π΅ β
No β§ π β
π΅) β ( bday βπ) β ( bday
β π΅)) |
23 | 4, 9, 22 | syl2an 597 |
. . . . . . . . . . . . . 14
β’ ((((π΄ β
No β§ π΄ β
V) β§ (π΅ β No β§ π΅ β V)) β§ (π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β ( bday
βπ) β
( bday β π΅)) |
24 | 17, 23 | eqeltrrd 2835 |
. . . . . . . . . . . . 13
β’ ((((π΄ β
No β§ π΄ β
V) β§ (π΅ β No β§ π΅ β V)) β§ (π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β dom π β ( bday
β π΅)) |
25 | | elssuni 4899 |
. . . . . . . . . . . . 13
β’ (dom
π β ( bday β π΅) β dom π β βͺ ( bday β π΅)) |
26 | 24, 25 | syl 17 |
. . . . . . . . . . . 12
β’ ((((π΄ β
No β§ π΄ β
V) β§ (π΅ β No β§ π΅ β V)) β§ (π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β dom π β βͺ ( bday β π΅)) |
27 | | nodmon 27014 |
. . . . . . . . . . . . 13
β’ (π β
No β dom π
β On) |
28 | | imassrn 6025 |
. . . . . . . . . . . . . . . 16
β’ ( bday β π΅) β ran bday
|
29 | | forn 6760 |
. . . . . . . . . . . . . . . . 17
β’ ( bday : No βontoβOn β ran
bday = On) |
30 | 18, 29 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
β’ ran bday = On |
31 | 28, 30 | sseqtri 3981 |
. . . . . . . . . . . . . . 15
β’ ( bday β π΅) β On |
32 | | ssorduni 7714 |
. . . . . . . . . . . . . . 15
β’ (( bday β π΅) β On β Ord βͺ ( bday β π΅)) |
33 | 31, 32 | ax-mp 5 |
. . . . . . . . . . . . . 14
β’ Ord βͺ ( bday β π΅) |
34 | | ordsssuc 6407 |
. . . . . . . . . . . . . 14
β’ ((dom
π β On β§ Ord βͺ ( bday β π΅)) β (dom π β βͺ ( bday β π΅) β dom π β suc βͺ
( bday β π΅))) |
35 | 33, 34 | mpan2 690 |
. . . . . . . . . . . . 13
β’ (dom
π β On β (dom
π β βͺ ( bday β π΅) β dom π β suc βͺ
( bday β π΅))) |
36 | 11, 27, 35 | 3syl 18 |
. . . . . . . . . . . 12
β’ ((((π΄ β
No β§ π΄ β
V) β§ (π΅ β No β§ π΅ β V)) β§ (π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β (dom π β βͺ ( bday β π΅) β dom π β suc βͺ
( bday β π΅))) |
37 | 26, 36 | mpbid 231 |
. . . . . . . . . . 11
β’ ((((π΄ β
No β§ π΄ β
V) β§ (π΅ β No β§ π΅ β V)) β§ (π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β dom π β suc βͺ
( bday β π΅)) |
38 | 15, 37 | sselid 3943 |
. . . . . . . . . 10
β’ ((((π΄ β
No β§ π΄ β
V) β§ (π΅ β No β§ π΅ β V)) β§ (π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β dom π β (dom π βͺ suc βͺ
( bday β π΅))) |
39 | | eleq2 2823 |
. . . . . . . . . 10
β’ ((dom
π βͺ suc βͺ ( bday β π΅)) = dom π β (dom π β (dom π βͺ suc βͺ
( bday β π΅)) β dom π β dom π)) |
40 | 38, 39 | syl5ibcom 244 |
. . . . . . . . 9
β’ ((((π΄ β
No β§ π΄ β
V) β§ (π΅ β No β§ π΅ β V)) β§ (π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β ((dom π βͺ suc βͺ
( bday β π΅)) = dom π β dom π β dom π)) |
41 | 14, 40 | mtod 197 |
. . . . . . . 8
β’ ((((π΄ β
No β§ π΄ β
V) β§ (π΅ β No β§ π΅ β V)) β§ (π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β Β¬ (dom π βͺ suc βͺ
( bday β π΅)) = dom π) |
42 | | noetasuplem.2 |
. . . . . . . . . . . 12
β’ π = (π βͺ ((suc βͺ
( bday β π΅) β dom π) Γ {1o})) |
43 | 42 | dmeqi 5861 |
. . . . . . . . . . 11
β’ dom π = dom (π βͺ ((suc βͺ
( bday β π΅) β dom π) Γ {1o})) |
44 | | dmun 5867 |
. . . . . . . . . . 11
β’ dom
(π βͺ ((suc βͺ ( bday β π΅) β dom π) Γ {1o})) = (dom π βͺ dom ((suc βͺ ( bday β π΅) β dom π) Γ {1o})) |
45 | 43, 44 | eqtri 2761 |
. . . . . . . . . 10
β’ dom π = (dom π βͺ dom ((suc βͺ ( bday β π΅) β dom π) Γ {1o})) |
46 | | 1oex 8423 |
. . . . . . . . . . . . 13
β’
1o β V |
47 | 46 | snnz 4738 |
. . . . . . . . . . . 12
β’
{1o} β β
|
48 | | dmxp 5885 |
. . . . . . . . . . . 12
β’
({1o} β β
β dom ((suc βͺ ( bday β π΅) β dom π) Γ {1o}) = (suc βͺ ( bday β π΅) β dom π)) |
49 | 47, 48 | ax-mp 5 |
. . . . . . . . . . 11
β’ dom ((suc
βͺ ( bday β π΅) β dom π) Γ {1o}) = (suc βͺ ( bday β π΅) β dom π) |
50 | 49 | uneq2i 4121 |
. . . . . . . . . 10
β’ (dom
π βͺ dom ((suc βͺ ( bday β π΅) β dom π) Γ {1o})) = (dom π βͺ (suc βͺ ( bday β π΅) β dom π)) |
51 | | undif2 4437 |
. . . . . . . . . 10
β’ (dom
π βͺ (suc βͺ ( bday β π΅) β dom π)) = (dom π βͺ suc βͺ
( bday β π΅)) |
52 | 45, 50, 51 | 3eqtri 2765 |
. . . . . . . . 9
β’ dom π = (dom π βͺ suc βͺ
( bday β π΅)) |
53 | | dmeq 5860 |
. . . . . . . . 9
β’ (π = π β dom π = dom π) |
54 | 52, 53 | eqtr3id 2787 |
. . . . . . . 8
β’ (π = π β (dom π βͺ suc βͺ
( bday β π΅)) = dom π) |
55 | 41, 54 | nsyl 140 |
. . . . . . 7
β’ ((((π΄ β
No β§ π΄ β
V) β§ (π΅ β No β§ π΅ β V)) β§ (π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β Β¬ π = π) |
56 | | df-ne 2941 |
. . . . . . . 8
β’ (π β π β Β¬ π = π) |
57 | | notnotr 130 |
. . . . . . . . . . . . . . 15
β’ (Β¬
Β¬ dom (π βΎ dom
π) = dom π β dom (π βΎ dom π) = dom π) |
58 | | simpr 486 |
. . . . . . . . . . . . . . . . . 18
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β§ π β π) β§ β© {π β On β£ (πβπ) β (πβπ)} β dom π) β β© {π β On β£ (πβπ) β (πβπ)} β dom π) |
59 | 58 | fvresd 6863 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β§ π β π) β§ β© {π β On β£ (πβπ) β (πβπ)} β dom π) β ((π βΎ dom π)ββ© {π β On β£ (πβπ) β (πβπ)}) = (πββ© {π β On β£ (πβπ) β (πβπ)})) |
60 | 42 | reseq1i 5934 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π βΎ dom π) = ((π βͺ ((suc βͺ
( bday β π΅) β dom π) Γ {1o})) βΎ dom
π) |
61 | | resundir 5953 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π βͺ ((suc βͺ ( bday β π΅) β dom π) Γ {1o})) βΎ dom
π) = ((π βΎ dom π) βͺ (((suc βͺ
( bday β π΅) β dom π) Γ {1o}) βΎ dom π)) |
62 | | df-res 5646 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((suc
βͺ ( bday β π΅) β dom π) Γ {1o}) βΎ dom π) = (((suc βͺ ( bday β π΅) β dom π) Γ {1o}) β© (dom π Γ V)) |
63 | | disjdifr 4433 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((suc
βͺ ( bday β π΅) β dom π) β© dom π) = β
|
64 | | xpdisj1 6114 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (((suc
βͺ ( bday β π΅) β dom π) β© dom π) = β
β (((suc βͺ ( bday β π΅) β dom π) Γ {1o}) β© (dom π Γ V)) =
β
) |
65 | 63, 64 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((suc
βͺ ( bday β π΅) β dom π) Γ {1o}) β© (dom π Γ V)) =
β
|
66 | 62, 65 | eqtri 2761 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((suc
βͺ ( bday β π΅) β dom π) Γ {1o}) βΎ dom π) = β
|
67 | 66 | uneq2i 4121 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π βΎ dom π) βͺ (((suc βͺ
( bday β π΅) β dom π) Γ {1o}) βΎ dom π)) = ((π βΎ dom π) βͺ β
) |
68 | | un0 4351 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π βΎ dom π) βͺ β
) = (π βΎ dom π) |
69 | 67, 68 | eqtri 2761 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π βΎ dom π) βͺ (((suc βͺ
( bday β π΅) β dom π) Γ {1o}) βΎ dom π)) = (π βΎ dom π) |
70 | 60, 61, 69 | 3eqtri 2765 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π βΎ dom π) = (π βΎ dom π) |
71 | | simplll 774 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
(((((π΄ β No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β§ π β π) β (π΄ β No
β§ π΄ β
V)) |
72 | 6 | nosupno 27067 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π΄ β
No β§ π΄ β
V) β π β No ) |
73 | 71, 72 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
(((((π΄ β No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β§ π β π) β π β No
) |
74 | 73 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β§ π β π) β§ β© {π β On β£ (πβπ) β (πβπ)} β dom π) β π β No
) |
75 | | nofun 27013 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β
No β Fun π) |
76 | 74, 75 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β§ π β π) β§ β© {π β On β£ (πβπ) β (πβπ)} β dom π) β Fun π) |
77 | | funrel 6519 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (Fun
π β Rel π) |
78 | | resdm 5983 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (Rel
π β (π βΎ dom π) = π) |
79 | 76, 77, 78 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β§ π β π) β§ β© {π β On β£ (πβπ) β (πβπ)} β dom π) β (π βΎ dom π) = π) |
80 | 70, 79 | eqtrid 2785 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β§ π β π) β§ β© {π β On β£ (πβπ) β (πβπ)} β dom π) β (π βΎ dom π) = π) |
81 | 80 | fveq1d 6845 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β§ π β π) β§ β© {π β On β£ (πβπ) β (πβπ)} β dom π) β ((π βΎ dom π)ββ© {π β On β£ (πβπ) β (πβπ)}) = (πββ© {π β On β£ (πβπ) β (πβπ)})) |
82 | 59, 81 | eqtr3d 2775 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β§ π β π) β§ β© {π β On β£ (πβπ) β (πβπ)} β dom π) β (πββ© {π β On β£ (πβπ) β (πβπ)}) = (πββ© {π β On β£ (πβπ) β (πβπ)})) |
83 | | simp-4l 782 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(((((π΄ β No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β§ π β π) β π΄ β No
) |
84 | | simp-4r 783 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(((((π΄ β No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β§ π β π) β π΄ β V) |
85 | | simplrr 777 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π΄ β
No β§ π΄ β
V) β§ (π΅ β No β§ π΅ β V)) β§ (π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β π΅ β V) |
86 | 85 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(((((π΄ β No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β§ π β π) β π΅ β V) |
87 | 6, 42 | noetasuplem1 27097 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π΄ β
No β§ π΄ β V
β§ π΅ β V) β
π β No ) |
88 | 83, 84, 86, 87 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((((π΄ β No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β§ π β π) β π β No
) |
89 | 88 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β§ π β π) β§ β© {π β On β£ (πβπ) β (πβπ)} β dom π) β π β No
) |
90 | 11 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((((π΄ β No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β§ π β π) β π β No
) |
91 | 90 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β§ π β π) β§ β© {π β On β£ (πβπ) β (πβπ)} β dom π) β π β No
) |
92 | | simplr 768 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β§ π β π) β§ β© {π β On β£ (πβπ) β (πβπ)} β dom π) β π β π) |
93 | | nosepne 27044 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β
No β§ π β
No β§ π β π) β (πββ© {π β On β£ (πβπ) β (πβπ)}) β (πββ© {π β On β£ (πβπ) β (πβπ)})) |
94 | 89, 91, 92, 93 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β§ π β π) β§ β© {π β On β£ (πβπ) β (πβπ)} β dom π) β (πββ© {π β On β£ (πβπ) β (πβπ)}) β (πββ© {π β On β£ (πβπ) β (πβπ)})) |
95 | 82, 94 | eqnetrrd 3009 |
. . . . . . . . . . . . . . . . . . 19
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β§ π β π) β§ β© {π β On β£ (πβπ) β (πβπ)} β dom π) β (πββ© {π β On β£ (πβπ) β (πβπ)}) β (πββ© {π β On β£ (πβπ) β (πβπ)})) |
96 | 58 | fvresd 6863 |
. . . . . . . . . . . . . . . . . . 19
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β§ π β π) β§ β© {π β On β£ (πβπ) β (πβπ)} β dom π) β ((π βΎ dom π)ββ© {π β On β£ (πβπ) β (πβπ)}) = (πββ© {π β On β£ (πβπ) β (πβπ)})) |
97 | 95, 96 | neeqtrrd 3015 |
. . . . . . . . . . . . . . . . . 18
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β§ π β π) β§ β© {π β On β£ (πβπ) β (πβπ)} β dom π) β (πββ© {π β On β£ (πβπ) β (πβπ)}) β ((π βΎ dom π)ββ© {π β On β£ (πβπ) β (πβπ)})) |
98 | | fveq2 6843 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = β©
{π β On β£ (πβπ) β (πβπ)} β ((π βΎ dom π)βπ) = ((π βΎ dom π)ββ© {π β On β£ (πβπ) β (πβπ)})) |
99 | | fveq2 6843 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = β©
{π β On β£ (πβπ) β (πβπ)} β (πβπ) = (πββ© {π β On β£ (πβπ) β (πβπ)})) |
100 | 98, 99 | neeq12d 3002 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = β©
{π β On β£ (πβπ) β (πβπ)} β (((π βΎ dom π)βπ) β (πβπ) β ((π βΎ dom π)ββ© {π β On β£ (πβπ) β (πβπ)}) β (πββ© {π β On β£ (πβπ) β (πβπ)}))) |
101 | | df-ne 2941 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π βΎ dom π)βπ) β (πβπ) β Β¬ ((π βΎ dom π)βπ) = (πβπ)) |
102 | | necom 2994 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π βΎ dom π)ββ© {π β On β£ (πβπ) β (πβπ)}) β (πββ© {π β On β£ (πβπ) β (πβπ)}) β (πββ© {π β On β£ (πβπ) β (πβπ)}) β ((π βΎ dom π)ββ© {π β On β£ (πβπ) β (πβπ)})) |
103 | 100, 101,
102 | 3bitr3g 313 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = β©
{π β On β£ (πβπ) β (πβπ)} β (Β¬ ((π βΎ dom π)βπ) = (πβπ) β (πββ© {π β On β£ (πβπ) β (πβπ)}) β ((π βΎ dom π)ββ© {π β On β£ (πβπ) β (πβπ)}))) |
104 | 103 | rspcev 3580 |
. . . . . . . . . . . . . . . . . 18
β’ ((β© {π
β On β£ (πβπ) β (πβπ)} β dom π β§ (πββ© {π β On β£ (πβπ) β (πβπ)}) β ((π βΎ dom π)ββ© {π β On β£ (πβπ) β (πβπ)})) β βπ β dom π Β¬ ((π βΎ dom π)βπ) = (πβπ)) |
105 | 58, 97, 104 | syl2anc 585 |
. . . . . . . . . . . . . . . . 17
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β§ π β π) β§ β© {π β On β£ (πβπ) β (πβπ)} β dom π) β βπ β dom π Β¬ ((π βΎ dom π)βπ) = (πβπ)) |
106 | | rexeq 3309 |
. . . . . . . . . . . . . . . . 17
β’ (dom
(π βΎ dom π) = dom π β (βπ β dom (π βΎ dom π) Β¬ ((π βΎ dom π)βπ) = (πβπ) β βπ β dom π Β¬ ((π βΎ dom π)βπ) = (πβπ))) |
107 | 105, 106 | syl5ibrcom 247 |
. . . . . . . . . . . . . . . 16
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β§ π β π) β§ β© {π β On β£ (πβπ) β (πβπ)} β dom π) β (dom (π βΎ dom π) = dom π β βπ β dom (π βΎ dom π) Β¬ ((π βΎ dom π)βπ) = (πβπ))) |
108 | | rexnal 3100 |
. . . . . . . . . . . . . . . 16
β’
(βπ β dom
(π βΎ dom π) Β¬ ((π βΎ dom π)βπ) = (πβπ) β Β¬ βπ β dom (π βΎ dom π)((π βΎ dom π)βπ) = (πβπ)) |
109 | 107, 108 | syl6ib 251 |
. . . . . . . . . . . . . . 15
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β§ π β π) β§ β© {π β On β£ (πβπ) β (πβπ)} β dom π) β (dom (π βΎ dom π) = dom π β Β¬ βπ β dom (π βΎ dom π)((π βΎ dom π)βπ) = (πβπ))) |
110 | 57, 109 | syl5 34 |
. . . . . . . . . . . . . 14
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β§ π β π) β§ β© {π β On β£ (πβπ) β (πβπ)} β dom π) β (Β¬ Β¬ dom (π βΎ dom π) = dom π β Β¬ βπ β dom (π βΎ dom π)((π βΎ dom π)βπ) = (πβπ))) |
111 | 110 | orrd 862 |
. . . . . . . . . . . . 13
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β§ π β π) β§ β© {π β On β£ (πβπ) β (πβπ)} β dom π) β (Β¬ dom (π βΎ dom π) = dom π β¨ Β¬ βπ β dom (π βΎ dom π)((π βΎ dom π)βπ) = (πβπ))) |
112 | | nofun 27013 |
. . . . . . . . . . . . . . . . 17
β’ (π β
No β Fun π) |
113 | | funres 6544 |
. . . . . . . . . . . . . . . . 17
β’ (Fun
π β Fun (π βΎ dom π)) |
114 | 91, 112, 113 | 3syl 18 |
. . . . . . . . . . . . . . . 16
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β§ π β π) β§ β© {π β On β£ (πβπ) β (πβπ)} β dom π) β Fun (π βΎ dom π)) |
115 | | eqfunfv 6988 |
. . . . . . . . . . . . . . . 16
β’ ((Fun
(π βΎ dom π) β§ Fun π) β ((π βΎ dom π) = π β (dom (π βΎ dom π) = dom π β§ βπ β dom (π βΎ dom π)((π βΎ dom π)βπ) = (πβπ)))) |
116 | 114, 76, 115 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β§ π β π) β§ β© {π β On β£ (πβπ) β (πβπ)} β dom π) β ((π βΎ dom π) = π β (dom (π βΎ dom π) = dom π β§ βπ β dom (π βΎ dom π)((π βΎ dom π)βπ) = (πβπ)))) |
117 | | ianor 981 |
. . . . . . . . . . . . . . . 16
β’ (Β¬
(dom (π βΎ dom π) = dom π β§ βπ β dom (π βΎ dom π)((π βΎ dom π)βπ) = (πβπ)) β (Β¬ dom (π βΎ dom π) = dom π β¨ Β¬ βπ β dom (π βΎ dom π)((π βΎ dom π)βπ) = (πβπ))) |
118 | 117 | con1bii 357 |
. . . . . . . . . . . . . . 15
β’ (Β¬
(Β¬ dom (π βΎ dom
π) = dom π β¨ Β¬ βπ β dom (π βΎ dom π)((π βΎ dom π)βπ) = (πβπ)) β (dom (π βΎ dom π) = dom π β§ βπ β dom (π βΎ dom π)((π βΎ dom π)βπ) = (πβπ))) |
119 | 116, 118 | bitr4di 289 |
. . . . . . . . . . . . . 14
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β§ π β π) β§ β© {π β On β£ (πβπ) β (πβπ)} β dom π) β ((π βΎ dom π) = π β Β¬ (Β¬ dom (π βΎ dom π) = dom π β¨ Β¬ βπ β dom (π βΎ dom π)((π βΎ dom π)βπ) = (πβπ)))) |
120 | 119 | con2bid 355 |
. . . . . . . . . . . . 13
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β§ π β π) β§ β© {π β On β£ (πβπ) β (πβπ)} β dom π) β ((Β¬ dom (π βΎ dom π) = dom π β¨ Β¬ βπ β dom (π βΎ dom π)((π βΎ dom π)βπ) = (πβπ)) β Β¬ (π βΎ dom π) = π)) |
121 | 111, 120 | mpbid 231 |
. . . . . . . . . . . 12
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β§ π β π) β§ β© {π β On β£ (πβπ) β (πβπ)} β dom π) β Β¬ (π βΎ dom π) = π) |
122 | 121 | pm2.21d 121 |
. . . . . . . . . . 11
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β§ π β π) β§ β© {π β On β£ (πβπ) β (πβπ)} β dom π) β ((π βΎ dom π) = π β π <s π)) |
123 | 80 | breq1d 5116 |
. . . . . . . . . . . 12
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β§ π β π) β§ β© {π β On β£ (πβπ) β (πβπ)} β dom π) β ((π βΎ dom π) <s (π βΎ dom π) β π <s (π βΎ dom π))) |
124 | | nodmon 27014 |
. . . . . . . . . . . . . 14
β’ (π β
No β dom π
β On) |
125 | 74, 124 | syl 17 |
. . . . . . . . . . . . 13
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β§ π β π) β§ β© {π β On β£ (πβπ) β (πβπ)} β dom π) β dom π β On) |
126 | | sltres 27026 |
. . . . . . . . . . . . 13
β’ ((π β
No β§ π β
No β§ dom π β On) β ((π βΎ dom π) <s (π βΎ dom π) β π <s π)) |
127 | 89, 91, 125, 126 | syl3anc 1372 |
. . . . . . . . . . . 12
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β§ π β π) β§ β© {π β On β£ (πβπ) β (πβπ)} β dom π) β ((π βΎ dom π) <s (π βΎ dom π) β π <s π)) |
128 | 123, 127 | sylbird 260 |
. . . . . . . . . . 11
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β§ π β π) β§ β© {π β On β£ (πβπ) β (πβπ)} β dom π) β (π <s (π βΎ dom π) β π <s π)) |
129 | | simplrr 777 |
. . . . . . . . . . . . 13
β’
(((((π΄ β No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β§ π β π) β Β¬ (π βΎ dom π) <s π) |
130 | 129 | adantr 482 |
. . . . . . . . . . . 12
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β§ π β π) β§ β© {π β On β£ (πβπ) β (πβπ)} β dom π) β Β¬ (π βΎ dom π) <s π) |
131 | | noreson 27024 |
. . . . . . . . . . . . . . 15
β’ ((π β
No β§ dom π
β On) β (π
βΎ dom π) β No ) |
132 | 91, 125, 131 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β§ π β π) β§ β© {π β On β£ (πβπ) β (πβπ)} β dom π) β (π βΎ dom π) β No
) |
133 | | sltso 27040 |
. . . . . . . . . . . . . . 15
β’ <s Or
No |
134 | | sotric 5574 |
. . . . . . . . . . . . . . 15
β’ (( <s
Or No β§ ((π βΎ dom π) β No
β§ π β No )) β ((π βΎ dom π) <s π β Β¬ ((π βΎ dom π) = π β¨ π <s (π βΎ dom π)))) |
135 | 133, 134 | mpan 689 |
. . . . . . . . . . . . . 14
β’ (((π βΎ dom π) β No
β§ π β No ) β ((π βΎ dom π) <s π β Β¬ ((π βΎ dom π) = π β¨ π <s (π βΎ dom π)))) |
136 | 132, 74, 135 | syl2anc 585 |
. . . . . . . . . . . . 13
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β§ π β π) β§ β© {π β On β£ (πβπ) β (πβπ)} β dom π) β ((π βΎ dom π) <s π β Β¬ ((π βΎ dom π) = π β¨ π <s (π βΎ dom π)))) |
137 | 136 | con2bid 355 |
. . . . . . . . . . . 12
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β§ π β π) β§ β© {π β On β£ (πβπ) β (πβπ)} β dom π) β (((π βΎ dom π) = π β¨ π <s (π βΎ dom π)) β Β¬ (π βΎ dom π) <s π)) |
138 | 130, 137 | mpbird 257 |
. . . . . . . . . . 11
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β§ π β π) β§ β© {π β On β£ (πβπ) β (πβπ)} β dom π) β ((π βΎ dom π) = π β¨ π <s (π βΎ dom π))) |
139 | 122, 128,
138 | mpjaod 859 |
. . . . . . . . . 10
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β§ π β π) β§ β© {π β On β£ (πβπ) β (πβπ)} β dom π) β π <s π) |
140 | 88 | adantr 482 |
. . . . . . . . . . 11
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β§ π β π) β§ dom π β β© {π β On β£ (πβπ) β (πβπ)}) β π β No
) |
141 | 90 | adantr 482 |
. . . . . . . . . . 11
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β§ π β π) β§ dom π β β© {π β On β£ (πβπ) β (πβπ)}) β π β No
) |
142 | | simplr 768 |
. . . . . . . . . . 11
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β§ π β π) β§ dom π β β© {π β On β£ (πβπ) β (πβπ)}) β π β π) |
143 | 42 | fveq1i 6844 |
. . . . . . . . . . . . 13
β’ (πββ© {π
β On β£ (πβπ) β (πβπ)}) = ((π βͺ ((suc βͺ
( bday β π΅) β dom π) Γ {1o}))ββ© {π
β On β£ (πβπ) β (πβπ)}) |
144 | | simp-4l 782 |
. . . . . . . . . . . . . . . 16
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β§ π β π) β§ dom π β β© {π β On β£ (πβπ) β (πβπ)}) β (π΄ β No
β§ π΄ β
V)) |
145 | 144, 72, 75 | 3syl 18 |
. . . . . . . . . . . . . . 15
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β§ π β π) β§ dom π β β© {π β On β£ (πβπ) β (πβπ)}) β Fun π) |
146 | | funfn 6532 |
. . . . . . . . . . . . . . 15
β’ (Fun
π β π Fn dom π) |
147 | 145, 146 | sylib 217 |
. . . . . . . . . . . . . 14
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β§ π β π) β§ dom π β β© {π β On β£ (πβπ) β (πβπ)}) β π Fn dom π) |
148 | 46 | fconst 6729 |
. . . . . . . . . . . . . . . 16
β’ ((suc
βͺ ( bday β π΅) β dom π) Γ {1o}):(suc βͺ ( bday β π΅) β dom π)βΆ{1o} |
149 | | ffn 6669 |
. . . . . . . . . . . . . . . 16
β’ (((suc
βͺ ( bday β π΅) β dom π) Γ {1o}):(suc βͺ ( bday β π΅) β dom π)βΆ{1o} β ((suc βͺ ( bday β π΅) β dom π) Γ {1o}) Fn (suc βͺ ( bday β π΅) β dom π)) |
150 | 148, 149 | ax-mp 5 |
. . . . . . . . . . . . . . 15
β’ ((suc
βͺ ( bday β π΅) β dom π) Γ {1o}) Fn (suc βͺ ( bday β π΅) β dom π) |
151 | 150 | a1i 11 |
. . . . . . . . . . . . . 14
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β§ π β π) β§ dom π β β© {π β On β£ (πβπ) β (πβπ)}) β ((suc βͺ
( bday β π΅) β dom π) Γ {1o}) Fn (suc βͺ ( bday β π΅) β dom π)) |
152 | | disjdif 4432 |
. . . . . . . . . . . . . . 15
β’ (dom
π β© (suc βͺ ( bday β π΅) β dom π)) = β
|
153 | 152 | a1i 11 |
. . . . . . . . . . . . . 14
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β§ π β π) β§ dom π β β© {π β On β£ (πβπ) β (πβπ)}) β (dom π β© (suc βͺ
( bday β π΅) β dom π)) = β
) |
154 | | necom 2994 |
. . . . . . . . . . . . . . . . . . 19
β’ ((πβπ) β (πβπ) β (πβπ) β (πβπ)) |
155 | 154 | rabbii 3412 |
. . . . . . . . . . . . . . . . . 18
β’ {π β On β£ (πβπ) β (πβπ)} = {π β On β£ (πβπ) β (πβπ)} |
156 | 155 | inteqi 4912 |
. . . . . . . . . . . . . . . . 17
β’ β© {π
β On β£ (πβπ) β (πβπ)} = β© {π β On β£ (πβπ) β (πβπ)} |
157 | 142 | necomd 2996 |
. . . . . . . . . . . . . . . . . 18
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β§ π β π) β§ dom π β β© {π β On β£ (πβπ) β (πβπ)}) β π β π) |
158 | | nosepssdm 27050 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β
No β§ π β
No β§ π β π) β β© {π β On β£ (πβπ) β (πβπ)} β dom π) |
159 | 141, 140,
157, 158 | syl3anc 1372 |
. . . . . . . . . . . . . . . . 17
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β§ π β π) β§ dom π β β© {π β On β£ (πβπ) β (πβπ)}) β β©
{π β On β£ (πβπ) β (πβπ)} β dom π) |
160 | 156, 159 | eqsstrid 3993 |
. . . . . . . . . . . . . . . 16
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β§ π β π) β§ dom π β β© {π β On β£ (πβπ) β (πβπ)}) β β©
{π β On β£ (πβπ) β (πβπ)} β dom π) |
161 | 141, 16 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β§ π β π) β§ dom π β β© {π β On β£ (πβπ) β (πβπ)}) β ( bday
βπ) = dom
π) |
162 | | simplrl 776 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π΄ β
No β§ π΄ β
V) β§ (π΅ β No β§ π΅ β V)) β§ (π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β π΅ β No
) |
163 | 162 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((π΄ β No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β§ π β π) β π΅ β No
) |
164 | 163 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β§ π β π) β§ dom π β β© {π β On β£ (πβπ) β (πβπ)}) β π΅ β No
) |
165 | | simplrl 776 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((π΄ β No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β§ π β π) β π β π΅) |
166 | 165 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β§ π β π) β§ dom π β β© {π β On β£ (πβπ) β (πβπ)}) β π β π΅) |
167 | 164, 166,
22 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . 19
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β§ π β π) β§ dom π β β© {π β On β£ (πβπ) β (πβπ)}) β ( bday
βπ) β
( bday β π΅)) |
168 | 161, 167 | eqeltrrd 2835 |
. . . . . . . . . . . . . . . . . 18
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β§ π β π) β§ dom π β β© {π β On β£ (πβπ) β (πβπ)}) β dom π β ( bday
β π΅)) |
169 | 168, 25 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β§ π β π) β§ dom π β β© {π β On β£ (πβπ) β (πβπ)}) β dom π β βͺ ( bday β π΅)) |
170 | 141, 27, 35 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β§ π β π) β§ dom π β β© {π β On β£ (πβπ) β (πβπ)}) β (dom π β βͺ ( bday β π΅) β dom π β suc βͺ
( bday β π΅))) |
171 | 169, 170 | mpbid 231 |
. . . . . . . . . . . . . . . 16
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β§ π β π) β§ dom π β β© {π β On β£ (πβπ) β (πβπ)}) β dom π β suc βͺ
( bday β π΅)) |
172 | | nosepon 27029 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β
No β§ π β
No β§ π β π) β β© {π β On β£ (πβπ) β (πβπ)} β On) |
173 | 140, 141,
142, 172 | syl3anc 1372 |
. . . . . . . . . . . . . . . . 17
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β§ π β π) β§ dom π β β© {π β On β£ (πβπ) β (πβπ)}) β β©
{π β On β£ (πβπ) β (πβπ)} β On) |
174 | | eloni 6328 |
. . . . . . . . . . . . . . . . 17
β’ (β© {π
β On β£ (πβπ) β (πβπ)} β On β Ord β© {π
β On β£ (πβπ) β (πβπ)}) |
175 | | ordsuc 7749 |
. . . . . . . . . . . . . . . . . . 19
β’ (Ord
βͺ ( bday β π΅) β Ord suc βͺ ( bday β π΅)) |
176 | 33, 175 | mpbi 229 |
. . . . . . . . . . . . . . . . . 18
β’ Ord suc
βͺ ( bday β π΅) |
177 | | ordtr2 6362 |
. . . . . . . . . . . . . . . . . 18
β’ ((Ord
β© {π β On β£ (πβπ) β (πβπ)} β§ Ord suc βͺ
( bday β π΅)) β ((β©
{π β On β£ (πβπ) β (πβπ)} β dom π β§ dom π β suc βͺ
( bday β π΅)) β β©
{π β On β£ (πβπ) β (πβπ)} β suc βͺ
( bday β π΅))) |
178 | 176, 177 | mpan2 690 |
. . . . . . . . . . . . . . . . 17
β’ (Ord
β© {π β On β£ (πβπ) β (πβπ)} β ((β©
{π β On β£ (πβπ) β (πβπ)} β dom π β§ dom π β suc βͺ
( bday β π΅)) β β©
{π β On β£ (πβπ) β (πβπ)} β suc βͺ
( bday β π΅))) |
179 | 173, 174,
178 | 3syl 18 |
. . . . . . . . . . . . . . . 16
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β§ π β π) β§ dom π β β© {π β On β£ (πβπ) β (πβπ)}) β ((β©
{π β On β£ (πβπ) β (πβπ)} β dom π β§ dom π β suc βͺ
( bday β π΅)) β β©
{π β On β£ (πβπ) β (πβπ)} β suc βͺ
( bday β π΅))) |
180 | 160, 171,
179 | mp2and 698 |
. . . . . . . . . . . . . . 15
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β§ π β π) β§ dom π β β© {π β On β£ (πβπ) β (πβπ)}) β β©
{π β On β£ (πβπ) β (πβπ)} β suc βͺ
( bday β π΅)) |
181 | | simpr 486 |
. . . . . . . . . . . . . . . 16
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β§ π β π) β§ dom π β β© {π β On β£ (πβπ) β (πβπ)}) β dom π β β© {π β On β£ (πβπ) β (πβπ)}) |
182 | 144, 72, 124 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β§ π β π) β§ dom π β β© {π β On β£ (πβπ) β (πβπ)}) β dom π β On) |
183 | | ontri1 6352 |
. . . . . . . . . . . . . . . . 17
β’ ((dom
π β On β§ β© {π
β On β£ (πβπ) β (πβπ)} β On) β (dom π β β© {π β On β£ (πβπ) β (πβπ)} β Β¬ β©
{π β On β£ (πβπ) β (πβπ)} β dom π)) |
184 | 182, 173,
183 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β§ π β π) β§ dom π β β© {π β On β£ (πβπ) β (πβπ)}) β (dom π β β© {π β On β£ (πβπ) β (πβπ)} β Β¬ β©
{π β On β£ (πβπ) β (πβπ)} β dom π)) |
185 | 181, 184 | mpbid 231 |
. . . . . . . . . . . . . . 15
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β§ π β π) β§ dom π β β© {π β On β£ (πβπ) β (πβπ)}) β Β¬ β©
{π β On β£ (πβπ) β (πβπ)} β dom π) |
186 | 180, 185 | eldifd 3922 |
. . . . . . . . . . . . . 14
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β§ π β π) β§ dom π β β© {π β On β£ (πβπ) β (πβπ)}) β β©
{π β On β£ (πβπ) β (πβπ)} β (suc βͺ
( bday β π΅) β dom π)) |
187 | | fvun2 6934 |
. . . . . . . . . . . . . 14
β’ ((π Fn dom π β§ ((suc βͺ
( bday β π΅) β dom π) Γ {1o}) Fn (suc βͺ ( bday β π΅) β dom π) β§ ((dom π β© (suc βͺ
( bday β π΅) β dom π)) = β
β§ β© {π
β On β£ (πβπ) β (πβπ)} β (suc βͺ
( bday β π΅) β dom π))) β ((π βͺ ((suc βͺ
( bday β π΅) β dom π) Γ {1o}))ββ© {π
β On β£ (πβπ) β (πβπ)}) = (((suc βͺ
( bday β π΅) β dom π) Γ {1o})ββ© {π
β On β£ (πβπ) β (πβπ)})) |
188 | 147, 151,
153, 186, 187 | syl112anc 1375 |
. . . . . . . . . . . . 13
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β§ π β π) β§ dom π β β© {π β On β£ (πβπ) β (πβπ)}) β ((π βͺ ((suc βͺ
( bday β π΅) β dom π) Γ {1o}))ββ© {π
β On β£ (πβπ) β (πβπ)}) = (((suc βͺ
( bday β π΅) β dom π) Γ {1o})ββ© {π
β On β£ (πβπ) β (πβπ)})) |
189 | 143, 188 | eqtrid 2785 |
. . . . . . . . . . . 12
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β§ π β π) β§ dom π β β© {π β On β£ (πβπ) β (πβπ)}) β (πββ© {π β On β£ (πβπ) β (πβπ)}) = (((suc βͺ
( bday β π΅) β dom π) Γ {1o})ββ© {π
β On β£ (πβπ) β (πβπ)})) |
190 | 46 | fvconst2 7154 |
. . . . . . . . . . . . 13
β’ (β© {π
β On β£ (πβπ) β (πβπ)} β (suc βͺ
( bday β π΅) β dom π) β (((suc βͺ
( bday β π΅) β dom π) Γ {1o})ββ© {π
β On β£ (πβπ) β (πβπ)}) = 1o) |
191 | 186, 190 | syl 17 |
. . . . . . . . . . . 12
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β§ π β π) β§ dom π β β© {π β On β£ (πβπ) β (πβπ)}) β (((suc βͺ ( bday β π΅) β dom π) Γ {1o})ββ© {π
β On β£ (πβπ) β (πβπ)}) = 1o) |
192 | 189, 191 | eqtrd 2773 |
. . . . . . . . . . 11
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β§ π β π) β§ dom π β β© {π β On β£ (πβπ) β (πβπ)}) β (πββ© {π β On β£ (πβπ) β (πβπ)}) = 1o) |
193 | | nosep1o 27045 |
. . . . . . . . . . 11
β’ (((π β
No β§ π β
No β§ π β π) β§ (πββ© {π β On β£ (πβπ) β (πβπ)}) = 1o) β π <s π) |
194 | 140, 141,
142, 192, 193 | syl31anc 1374 |
. . . . . . . . . 10
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β§ π β π) β§ dom π β β© {π β On β£ (πβπ) β (πβπ)}) β π <s π) |
195 | | simpr 486 |
. . . . . . . . . . . . 13
β’
(((((π΄ β No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β§ π β π) β π β π) |
196 | 88, 90, 195, 172 | syl3anc 1372 |
. . . . . . . . . . . 12
β’
(((((π΄ β No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β§ π β π) β β© {π β On β£ (πβπ) β (πβπ)} β On) |
197 | 196, 174 | syl 17 |
. . . . . . . . . . 11
β’
(((((π΄ β No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β§ π β π) β Ord β©
{π β On β£ (πβπ) β (πβπ)}) |
198 | | nodmord 27017 |
. . . . . . . . . . . 12
β’ (π β
No β Ord dom π) |
199 | 71, 72, 198 | 3syl 18 |
. . . . . . . . . . 11
β’
(((((π΄ β No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β§ π β π) β Ord dom π) |
200 | | ordtri2or 6416 |
. . . . . . . . . . 11
β’ ((Ord
β© {π β On β£ (πβπ) β (πβπ)} β§ Ord dom π) β (β©
{π β On β£ (πβπ) β (πβπ)} β dom π β¨ dom π β β© {π β On β£ (πβπ) β (πβπ)})) |
201 | 197, 199,
200 | syl2anc 585 |
. . . . . . . . . 10
β’
(((((π΄ β No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β§ π β π) β (β© {π β On β£ (πβπ) β (πβπ)} β dom π β¨ dom π β β© {π β On β£ (πβπ) β (πβπ)})) |
202 | 139, 194,
201 | mpjaodan 958 |
. . . . . . . . 9
β’
(((((π΄ β No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β§ π β π) β π <s π) |
203 | 202 | ex 414 |
. . . . . . . 8
β’ ((((π΄ β
No β§ π΄ β
V) β§ (π΅ β No β§ π΅ β V)) β§ (π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β (π β π β π <s π)) |
204 | 56, 203 | biimtrrid 242 |
. . . . . . 7
β’ ((((π΄ β
No β§ π΄ β
V) β§ (π΅ β No β§ π΅ β V)) β§ (π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β (Β¬ π = π β π <s π)) |
205 | 55, 204 | mpd 15 |
. . . . . 6
β’ ((((π΄ β
No β§ π΄ β
V) β§ (π΅ β No β§ π΅ β V)) β§ (π β π΅ β§ Β¬ (π βΎ dom π) <s π)) β π <s π) |
206 | 205 | expr 458 |
. . . . 5
β’ ((((π΄ β
No β§ π΄ β
V) β§ (π΅ β No β§ π΅ β V)) β§ π β π΅) β (Β¬ (π βΎ dom π) <s π β π <s π)) |
207 | 8, 206 | sylbid 239 |
. . . 4
β’ ((((π΄ β
No β§ π΄ β
V) β§ (π΅ β No β§ π΅ β V)) β§ π β π΅) β (βπ β π΄ π <s π β π <s π)) |
208 | 207 | ralimdva 3161 |
. . 3
β’ (((π΄ β
No β§ π΄ β
V) β§ (π΅ β No β§ π΅ β V)) β (βπ β π΅ βπ β π΄ π <s π β βπ β π΅ π <s π)) |
209 | 1, 208 | biimtrid 241 |
. 2
β’ (((π΄ β
No β§ π΄ β
V) β§ (π΅ β No β§ π΅ β V)) β (βπ β π΄ βπ β π΅ π <s π β βπ β π΅ π <s π)) |
210 | 209 | 3impia 1118 |
1
β’ (((π΄ β
No β§ π΄ β
V) β§ (π΅ β No β§ π΅ β V) β§ βπ β π΄ βπ β π΅ π <s π) β βπ β π΅ π <s π) |