Step | Hyp | Ref
| Expression |
1 | | simplrl 776 |
. . . . 5
β’ ((((π΄ β
No β§ π΄ β
V) β§ (π΅ β No β§ π΅ β V)) β§ π β π΄) β π΅ β No
) |
2 | | simplrr 777 |
. . . . 5
β’ ((((π΄ β
No β§ π΄ β
V) β§ (π΅ β No β§ π΅ β V)) β§ π β π΄) β π΅ β V) |
3 | | simpll 766 |
. . . . . 6
β’ (((π΄ β
No β§ π΄ β
V) β§ (π΅ β No β§ π΅ β V)) β π΄ β No
) |
4 | 3 | sselda 3945 |
. . . . 5
β’ ((((π΄ β
No β§ π΄ β
V) β§ (π΅ β No β§ π΅ β V)) β§ π β π΄) β π β No
) |
5 | | noetainflem.1 |
. . . . . 6
β’ π = if(βπ₯ β π΅ βπ¦ β π΅ Β¬ π¦ <s π₯, ((β©π₯ β π΅ βπ¦ β π΅ Β¬ π¦ <s π₯) βͺ {β¨dom (β©π₯ β π΅ βπ¦ β π΅ Β¬ π¦ <s π₯), 1oβ©}), (π β {π¦ β£ βπ’ β π΅ (π¦ β dom π’ β§ βπ£ β π΅ (Β¬ π’ <s π£ β (π’ βΎ suc π¦) = (π£ βΎ suc π¦)))} β¦ (β©π₯βπ’ β π΅ (π β dom π’ β§ βπ£ β π΅ (Β¬ π’ <s π£ β (π’ βΎ suc π) = (π£ βΎ suc π)) β§ (π’βπ) = π₯)))) |
6 | 5 | noinfbnd2 27095 |
. . . . 5
β’ ((π΅ β
No β§ π΅ β V
β§ π β No ) β (βπ β π΅ π <s π β Β¬ π <s (π βΎ dom π))) |
7 | 1, 2, 4, 6 | syl3anc 1372 |
. . . 4
β’ ((((π΄ β
No β§ π΄ β
V) β§ (π΅ β No β§ π΅ β V)) β§ π β π΄) β (βπ β π΅ π <s π β Β¬ π <s (π βΎ dom π))) |
8 | | simplll 774 |
. . . . . . . . . . 11
β’ ((((π΄ β
No β§ π΄ β
V) β§ (π΅ β No β§ π΅ β V)) β§ (π β π΄ β§ Β¬ π <s (π βΎ dom π))) β π΄ β No
) |
9 | | simprl 770 |
. . . . . . . . . . 11
β’ ((((π΄ β
No β§ π΄ β
V) β§ (π΅ β No β§ π΅ β V)) β§ (π β π΄ β§ Β¬ π <s (π βΎ dom π))) β π β π΄) |
10 | 8, 9 | sseldd 3946 |
. . . . . . . . . 10
β’ ((((π΄ β
No β§ π΄ β
V) β§ (π΅ β No β§ π΅ β V)) β§ (π β π΄ β§ Β¬ π <s (π βΎ dom π))) β π β No
) |
11 | | nodmord 27017 |
. . . . . . . . . 10
β’ (π β
No β Ord dom π) |
12 | | ordirr 6336 |
. . . . . . . . . 10
β’ (Ord dom
π β Β¬ dom π β dom π) |
13 | 10, 11, 12 | 3syl 18 |
. . . . . . . . 9
β’ ((((π΄ β
No β§ π΄ β
V) β§ (π΅ β No β§ π΅ β V)) β§ (π β π΄ β§ Β¬ π <s (π βΎ dom π))) β Β¬ dom π β dom π) |
14 | | bdayval 27012 |
. . . . . . . . . . . . . . 15
β’ (π β
No β ( bday βπ) = dom π) |
15 | 10, 14 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((((π΄ β
No β§ π΄ β
V) β§ (π΅ β No β§ π΅ β V)) β§ (π β π΄ β§ Β¬ π <s (π βΎ dom π))) β ( bday
βπ) = dom
π) |
16 | | bdayfo 27041 |
. . . . . . . . . . . . . . . 16
β’ bday : No βontoβOn |
17 | | fofn 6759 |
. . . . . . . . . . . . . . . 16
β’ ( bday : No βontoβOn β bday
Fn No ) |
18 | 16, 17 | ax-mp 5 |
. . . . . . . . . . . . . . 15
β’ bday Fn No
|
19 | | fnfvima 7184 |
. . . . . . . . . . . . . . 15
β’ (( bday Fn No β§ π΄ β
No β§ π β
π΄) β ( bday βπ) β ( bday
β π΄)) |
20 | 18, 8, 9, 19 | mp3an2i 1467 |
. . . . . . . . . . . . . 14
β’ ((((π΄ β
No β§ π΄ β
V) β§ (π΅ β No β§ π΅ β V)) β§ (π β π΄ β§ Β¬ π <s (π βΎ dom π))) β ( bday
βπ) β
( bday β π΄)) |
21 | 15, 20 | eqeltrrd 2835 |
. . . . . . . . . . . . 13
β’ ((((π΄ β
No β§ π΄ β
V) β§ (π΅ β No β§ π΅ β V)) β§ (π β π΄ β§ Β¬ π <s (π βΎ dom π))) β dom π β ( bday
β π΄)) |
22 | | elssuni 4899 |
. . . . . . . . . . . . 13
β’ (dom
π β ( bday β π΄) β dom π β βͺ ( bday β π΄)) |
23 | 21, 22 | syl 17 |
. . . . . . . . . . . 12
β’ ((((π΄ β
No β§ π΄ β
V) β§ (π΅ β No β§ π΅ β V)) β§ (π β π΄ β§ Β¬ π <s (π βΎ dom π))) β dom π β βͺ ( bday β π΄)) |
24 | | nodmon 27014 |
. . . . . . . . . . . . 13
β’ (π β
No β dom π
β On) |
25 | | imassrn 6025 |
. . . . . . . . . . . . . . . 16
β’ ( bday β π΄) β ran bday
|
26 | | forn 6760 |
. . . . . . . . . . . . . . . . 17
β’ ( bday : No βontoβOn β ran
bday = On) |
27 | 16, 26 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
β’ ran bday = On |
28 | 25, 27 | sseqtri 3981 |
. . . . . . . . . . . . . . 15
β’ ( bday β π΄) β On |
29 | | ssorduni 7714 |
. . . . . . . . . . . . . . 15
β’ (( bday β π΄) β On β Ord βͺ ( bday β π΄)) |
30 | 28, 29 | ax-mp 5 |
. . . . . . . . . . . . . 14
β’ Ord βͺ ( bday β π΄) |
31 | | ordsssuc 6407 |
. . . . . . . . . . . . . 14
β’ ((dom
π β On β§ Ord βͺ ( bday β π΄)) β (dom π β βͺ ( bday β π΄) β dom π β suc βͺ
( bday β π΄))) |
32 | 30, 31 | mpan2 690 |
. . . . . . . . . . . . 13
β’ (dom
π β On β (dom
π β βͺ ( bday β π΄) β dom π β suc βͺ
( bday β π΄))) |
33 | 10, 24, 32 | 3syl 18 |
. . . . . . . . . . . 12
β’ ((((π΄ β
No β§ π΄ β
V) β§ (π΅ β No β§ π΅ β V)) β§ (π β π΄ β§ Β¬ π <s (π βΎ dom π))) β (dom π β βͺ ( bday β π΄) β dom π β suc βͺ
( bday β π΄))) |
34 | 23, 33 | mpbid 231 |
. . . . . . . . . . 11
β’ ((((π΄ β
No β§ π΄ β
V) β§ (π΅ β No β§ π΅ β V)) β§ (π β π΄ β§ Β¬ π <s (π βΎ dom π))) β dom π β suc βͺ
( bday β π΄)) |
35 | | elun2 4138 |
. . . . . . . . . . 11
β’ (dom
π β suc βͺ ( bday β π΄) β dom π β (dom π βͺ suc βͺ
( bday β π΄))) |
36 | 34, 35 | syl 17 |
. . . . . . . . . 10
β’ ((((π΄ β
No β§ π΄ β
V) β§ (π΅ β No β§ π΅ β V)) β§ (π β π΄ β§ Β¬ π <s (π βΎ dom π))) β dom π β (dom π βͺ suc βͺ
( bday β π΄))) |
37 | | eleq2 2823 |
. . . . . . . . . 10
β’ (dom
π = (dom π βͺ suc βͺ
( bday β π΄)) β (dom π β dom π β dom π β (dom π βͺ suc βͺ
( bday β π΄)))) |
38 | 36, 37 | syl5ibrcom 247 |
. . . . . . . . 9
β’ ((((π΄ β
No β§ π΄ β
V) β§ (π΅ β No β§ π΅ β V)) β§ (π β π΄ β§ Β¬ π <s (π βΎ dom π))) β (dom π = (dom π βͺ suc βͺ
( bday β π΄)) β dom π β dom π)) |
39 | 13, 38 | mtod 197 |
. . . . . . . 8
β’ ((((π΄ β
No β§ π΄ β
V) β§ (π΅ β No β§ π΅ β V)) β§ (π β π΄ β§ Β¬ π <s (π βΎ dom π))) β Β¬ dom π = (dom π βͺ suc βͺ
( bday β π΄))) |
40 | | dmeq 5860 |
. . . . . . . . 9
β’ (π = π β dom π = dom π) |
41 | | noetainflem.2 |
. . . . . . . . . . 11
β’ π = (π βͺ ((suc βͺ
( bday β π΄) β dom π) Γ {2o})) |
42 | 41 | dmeqi 5861 |
. . . . . . . . . 10
β’ dom π = dom (π βͺ ((suc βͺ
( bday β π΄) β dom π) Γ {2o})) |
43 | | dmun 5867 |
. . . . . . . . . 10
β’ dom
(π βͺ ((suc βͺ ( bday β π΄) β dom π) Γ {2o})) = (dom π βͺ dom ((suc βͺ ( bday β π΄) β dom π) Γ {2o})) |
44 | | 2oex 8424 |
. . . . . . . . . . . . . 14
β’
2o β V |
45 | 44 | snnz 4738 |
. . . . . . . . . . . . 13
β’
{2o} β β
|
46 | | dmxp 5885 |
. . . . . . . . . . . . 13
β’
({2o} β β
β dom ((suc βͺ ( bday β π΄) β dom π) Γ {2o}) = (suc βͺ ( bday β π΄) β dom π)) |
47 | 45, 46 | ax-mp 5 |
. . . . . . . . . . . 12
β’ dom ((suc
βͺ ( bday β π΄) β dom π) Γ {2o}) = (suc βͺ ( bday β π΄) β dom π) |
48 | 47 | uneq2i 4121 |
. . . . . . . . . . 11
β’ (dom
π βͺ dom ((suc βͺ ( bday β π΄) β dom π) Γ {2o})) = (dom π βͺ (suc βͺ ( bday β π΄) β dom π)) |
49 | | undif2 4437 |
. . . . . . . . . . 11
β’ (dom
π βͺ (suc βͺ ( bday β π΄) β dom π)) = (dom π βͺ suc βͺ
( bday β π΄)) |
50 | 48, 49 | eqtri 2761 |
. . . . . . . . . 10
β’ (dom
π βͺ dom ((suc βͺ ( bday β π΄) β dom π) Γ {2o})) = (dom π βͺ suc βͺ ( bday β π΄)) |
51 | 42, 43, 50 | 3eqtri 2765 |
. . . . . . . . 9
β’ dom π = (dom π βͺ suc βͺ
( bday β π΄)) |
52 | 40, 51 | eqtrdi 2789 |
. . . . . . . 8
β’ (π = π β dom π = (dom π βͺ suc βͺ
( bday β π΄))) |
53 | 39, 52 | nsyl 140 |
. . . . . . 7
β’ ((((π΄ β
No β§ π΄ β
V) β§ (π΅ β No β§ π΅ β V)) β§ (π β π΄ β§ Β¬ π <s (π βΎ dom π))) β Β¬ π = π) |
54 | 53 | neqned 2947 |
. . . . . 6
β’ ((((π΄ β
No β§ π΄ β
V) β§ (π΅ β No β§ π΅ β V)) β§ (π β π΄ β§ Β¬ π <s (π βΎ dom π))) β π β π) |
55 | | simpr 486 |
. . . . . . . . . . . . 13
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΄ β§ Β¬ π <s (π βΎ dom π))) β§ π β π) β§ β© {π β On β£ (πβπ) β (πβπ)} β dom π) β β© {π β On β£ (πβπ) β (πβπ)} β dom π) |
56 | 10 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’
(((((π΄ β No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΄ β§ Β¬ π <s (π βΎ dom π))) β§ π β π) β π β No
) |
57 | 56 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΄ β§ Β¬ π <s (π βΎ dom π))) β§ π β π) β§ β© {π β On β£ (πβπ) β (πβπ)} β dom π) β π β No
) |
58 | | simp-4r 783 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π΄ β No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΄ β§ Β¬ π <s (π βΎ dom π))) β§ π β π) β π΄ β V) |
59 | | simplrl 776 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π΄ β
No β§ π΄ β
V) β§ (π΅ β No β§ π΅ β V)) β§ (π β π΄ β§ Β¬ π <s (π βΎ dom π))) β π΅ β No
) |
60 | 59 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π΄ β No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΄ β§ Β¬ π <s (π βΎ dom π))) β§ π β π) β π΅ β No
) |
61 | | simplrr 777 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π΄ β
No β§ π΄ β
V) β§ (π΅ β No β§ π΅ β V)) β§ (π β π΄ β§ Β¬ π <s (π βΎ dom π))) β π΅ β V) |
62 | 61 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π΄ β No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΄ β§ Β¬ π <s (π βΎ dom π))) β§ π β π) β π΅ β V) |
63 | 5, 41 | noetainflem1 27101 |
. . . . . . . . . . . . . . . . . 18
β’ ((π΄ β V β§ π΅ β
No β§ π΅ β
V) β π β No ) |
64 | 58, 60, 62, 63 | syl3anc 1372 |
. . . . . . . . . . . . . . . . 17
β’
(((((π΄ β No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΄ β§ Β¬ π <s (π βΎ dom π))) β§ π β π) β π β No
) |
65 | 64 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΄ β§ Β¬ π <s (π βΎ dom π))) β§ π β π) β§ β© {π β On β£ (πβπ) β (πβπ)} β dom π) β π β No
) |
66 | | simplr 768 |
. . . . . . . . . . . . . . . 16
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΄ β§ Β¬ π <s (π βΎ dom π))) β§ π β π) β§ β© {π β On β£ (πβπ) β (πβπ)} β dom π) β π β π) |
67 | | nosepne 27044 |
. . . . . . . . . . . . . . . 16
β’ ((π β
No β§ π β
No β§ π β π) β (πββ© {π β On β£ (πβπ) β (πβπ)}) β (πββ© {π β On β£ (πβπ) β (πβπ)})) |
68 | 57, 65, 66, 67 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΄ β§ Β¬ π <s (π βΎ dom π))) β§ π β π) β§ β© {π β On β£ (πβπ) β (πβπ)} β dom π) β (πββ© {π β On β£ (πβπ) β (πβπ)}) β (πββ© {π β On β£ (πβπ) β (πβπ)})) |
69 | 55 | fvresd 6863 |
. . . . . . . . . . . . . . . 16
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΄ β§ Β¬ π <s (π βΎ dom π))) β§ π β π) β§ β© {π β On β£ (πβπ) β (πβπ)} β dom π) β ((π βΎ dom π)ββ© {π β On β£ (πβπ) β (πβπ)}) = (πββ© {π β On β£ (πβπ) β (πβπ)})) |
70 | | simp-4r 783 |
. . . . . . . . . . . . . . . . . 18
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΄ β§ Β¬ π <s (π βΎ dom π))) β§ π β π) β§ β© {π β On β£ (πβπ) β (πβπ)} β dom π) β (π΅ β No
β§ π΅ β
V)) |
71 | 5, 41 | noetainflem2 27102 |
. . . . . . . . . . . . . . . . . 18
β’ ((π΅ β
No β§ π΅ β
V) β (π βΎ dom
π) = π) |
72 | 70, 71 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΄ β§ Β¬ π <s (π βΎ dom π))) β§ π β π) β§ β© {π β On β£ (πβπ) β (πβπ)} β dom π) β (π βΎ dom π) = π) |
73 | 72 | fveq1d 6845 |
. . . . . . . . . . . . . . . 16
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΄ β§ Β¬ π <s (π βΎ dom π))) β§ π β π) β§ β© {π β On β£ (πβπ) β (πβπ)} β dom π) β ((π βΎ dom π)ββ© {π β On β£ (πβπ) β (πβπ)}) = (πββ© {π β On β£ (πβπ) β (πβπ)})) |
74 | 69, 73 | eqtr3d 2775 |
. . . . . . . . . . . . . . 15
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΄ β§ Β¬ π <s (π βΎ dom π))) β§ π β π) β§ β© {π β On β£ (πβπ) β (πβπ)} β dom π) β (πββ© {π β On β£ (πβπ) β (πβπ)}) = (πββ© {π β On β£ (πβπ) β (πβπ)})) |
75 | 68, 74 | neeqtrd 3010 |
. . . . . . . . . . . . . 14
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΄ β§ Β¬ π <s (π βΎ dom π))) β§ π β π) β§ β© {π β On β£ (πβπ) β (πβπ)} β dom π) β (πββ© {π β On β£ (πβπ) β (πβπ)}) β (πββ© {π β On β£ (πβπ) β (πβπ)})) |
76 | 75 | necomd 2996 |
. . . . . . . . . . . . 13
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΄ β§ Β¬ π <s (π βΎ dom π))) β§ π β π) β§ β© {π β On β£ (πβπ) β (πβπ)} β dom π) β (πββ© {π β On β£ (πβπ) β (πβπ)}) β (πββ© {π β On β£ (πβπ) β (πβπ)})) |
77 | | fveq2 6843 |
. . . . . . . . . . . . . . 15
β’ (π = β©
{π β On β£ (πβπ) β (πβπ)} β (πβπ) = (πββ© {π β On β£ (πβπ) β (πβπ)})) |
78 | | fveq2 6843 |
. . . . . . . . . . . . . . 15
β’ (π = β©
{π β On β£ (πβπ) β (πβπ)} β (πβπ) = (πββ© {π β On β£ (πβπ) β (πβπ)})) |
79 | 77, 78 | neeq12d 3002 |
. . . . . . . . . . . . . 14
β’ (π = β©
{π β On β£ (πβπ) β (πβπ)} β ((πβπ) β (πβπ) β (πββ© {π β On β£ (πβπ) β (πβπ)}) β (πββ© {π β On β£ (πβπ) β (πβπ)}))) |
80 | 79 | rspcev 3580 |
. . . . . . . . . . . . 13
β’ ((β© {π
β On β£ (πβπ) β (πβπ)} β dom π β§ (πββ© {π β On β£ (πβπ) β (πβπ)}) β (πββ© {π β On β£ (πβπ) β (πβπ)})) β βπ β dom π(πβπ) β (πβπ)) |
81 | 55, 76, 80 | syl2anc 585 |
. . . . . . . . . . . 12
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΄ β§ Β¬ π <s (π βΎ dom π))) β§ π β π) β§ β© {π β On β£ (πβπ) β (πβπ)} β dom π) β βπ β dom π(πβπ) β (πβπ)) |
82 | | df-ne 2941 |
. . . . . . . . . . . . . . 15
β’ ((πβπ) β ((π βΎ dom π)βπ) β Β¬ (πβπ) = ((π βΎ dom π)βπ)) |
83 | | fvres 6862 |
. . . . . . . . . . . . . . . 16
β’ (π β dom π β ((π βΎ dom π)βπ) = (πβπ)) |
84 | 83 | neeq2d 3001 |
. . . . . . . . . . . . . . 15
β’ (π β dom π β ((πβπ) β ((π βΎ dom π)βπ) β (πβπ) β (πβπ))) |
85 | 82, 84 | bitr3id 285 |
. . . . . . . . . . . . . 14
β’ (π β dom π β (Β¬ (πβπ) = ((π βΎ dom π)βπ) β (πβπ) β (πβπ))) |
86 | 85 | rexbiia 3092 |
. . . . . . . . . . . . 13
β’
(βπ β dom
π Β¬ (πβπ) = ((π βΎ dom π)βπ) β βπ β dom π(πβπ) β (πβπ)) |
87 | | rexnal 3100 |
. . . . . . . . . . . . 13
β’
(βπ β dom
π Β¬ (πβπ) = ((π βΎ dom π)βπ) β Β¬ βπ β dom π(πβπ) = ((π βΎ dom π)βπ)) |
88 | 86, 87 | bitr3i 277 |
. . . . . . . . . . . 12
β’
(βπ β dom
π(πβπ) β (πβπ) β Β¬ βπ β dom π(πβπ) = ((π βΎ dom π)βπ)) |
89 | 81, 88 | sylib 217 |
. . . . . . . . . . 11
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΄ β§ Β¬ π <s (π βΎ dom π))) β§ π β π) β§ β© {π β On β£ (πβπ) β (πβπ)} β dom π) β Β¬ βπ β dom π(πβπ) = ((π βΎ dom π)βπ)) |
90 | 89 | olcd 873 |
. . . . . . . . . 10
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΄ β§ Β¬ π <s (π βΎ dom π))) β§ π β π) β§ β© {π β On β£ (πβπ) β (πβπ)} β dom π) β (Β¬ dom π = dom (π βΎ dom π) β¨ Β¬ βπ β dom π(πβπ) = ((π βΎ dom π)βπ))) |
91 | 5 | noinfno 27082 |
. . . . . . . . . . . . . . . 16
β’ ((π΅ β
No β§ π΅ β
V) β π β No ) |
92 | 91 | ad3antlr 730 |
. . . . . . . . . . . . . . 15
β’
(((((π΄ β No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΄ β§ Β¬ π <s (π βΎ dom π))) β§ π β π) β π β No
) |
93 | 92 | adantr 482 |
. . . . . . . . . . . . . 14
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΄ β§ Β¬ π <s (π βΎ dom π))) β§ π β π) β§ β© {π β On β£ (πβπ) β (πβπ)} β dom π) β π β No
) |
94 | | nofun 27013 |
. . . . . . . . . . . . . 14
β’ (π β
No β Fun π) |
95 | 93, 94 | syl 17 |
. . . . . . . . . . . . 13
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΄ β§ Β¬ π <s (π βΎ dom π))) β§ π β π) β§ β© {π β On β£ (πβπ) β (πβπ)} β dom π) β Fun π) |
96 | | nofun 27013 |
. . . . . . . . . . . . . 14
β’ (π β
No β Fun π) |
97 | | funres 6544 |
. . . . . . . . . . . . . 14
β’ (Fun
π β Fun (π βΎ dom π)) |
98 | 57, 96, 97 | 3syl 18 |
. . . . . . . . . . . . 13
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΄ β§ Β¬ π <s (π βΎ dom π))) β§ π β π) β§ β© {π β On β£ (πβπ) β (πβπ)} β dom π) β Fun (π βΎ dom π)) |
99 | | eqfunfv 6988 |
. . . . . . . . . . . . 13
β’ ((Fun
π β§ Fun (π βΎ dom π)) β (π = (π βΎ dom π) β (dom π = dom (π βΎ dom π) β§ βπ β dom π(πβπ) = ((π βΎ dom π)βπ)))) |
100 | 95, 98, 99 | syl2anc 585 |
. . . . . . . . . . . 12
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΄ β§ Β¬ π <s (π βΎ dom π))) β§ π β π) β§ β© {π β On β£ (πβπ) β (πβπ)} β dom π) β (π = (π βΎ dom π) β (dom π = dom (π βΎ dom π) β§ βπ β dom π(πβπ) = ((π βΎ dom π)βπ)))) |
101 | | ianor 981 |
. . . . . . . . . . . . 13
β’ (Β¬
(dom π = dom (π βΎ dom π) β§ βπ β dom π(πβπ) = ((π βΎ dom π)βπ)) β (Β¬ dom π = dom (π βΎ dom π) β¨ Β¬ βπ β dom π(πβπ) = ((π βΎ dom π)βπ))) |
102 | 101 | con1bii 357 |
. . . . . . . . . . . 12
β’ (Β¬
(Β¬ dom π = dom (π βΎ dom π) β¨ Β¬ βπ β dom π(πβπ) = ((π βΎ dom π)βπ)) β (dom π = dom (π βΎ dom π) β§ βπ β dom π(πβπ) = ((π βΎ dom π)βπ))) |
103 | 100, 102 | bitr4di 289 |
. . . . . . . . . . 11
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΄ β§ Β¬ π <s (π βΎ dom π))) β§ π β π) β§ β© {π β On β£ (πβπ) β (πβπ)} β dom π) β (π = (π βΎ dom π) β Β¬ (Β¬ dom π = dom (π βΎ dom π) β¨ Β¬ βπ β dom π(πβπ) = ((π βΎ dom π)βπ)))) |
104 | 103 | con2bid 355 |
. . . . . . . . . 10
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΄ β§ Β¬ π <s (π βΎ dom π))) β§ π β π) β§ β© {π β On β£ (πβπ) β (πβπ)} β dom π) β ((Β¬ dom π = dom (π βΎ dom π) β¨ Β¬ βπ β dom π(πβπ) = ((π βΎ dom π)βπ)) β Β¬ π = (π βΎ dom π))) |
105 | 90, 104 | mpbid 231 |
. . . . . . . . 9
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΄ β§ Β¬ π <s (π βΎ dom π))) β§ π β π) β§ β© {π β On β£ (πβπ) β (πβπ)} β dom π) β Β¬ π = (π βΎ dom π)) |
106 | 105 | pm2.21d 121 |
. . . . . . . 8
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΄ β§ Β¬ π <s (π βΎ dom π))) β§ π β π) β§ β© {π β On β£ (πβπ) β (πβπ)} β dom π) β (π = (π βΎ dom π) β π <s π)) |
107 | 72 | breq2d 5118 |
. . . . . . . . 9
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΄ β§ Β¬ π <s (π βΎ dom π))) β§ π β π) β§ β© {π β On β£ (πβπ) β (πβπ)} β dom π) β ((π βΎ dom π) <s (π βΎ dom π) β (π βΎ dom π) <s π)) |
108 | | nodmon 27014 |
. . . . . . . . . . . 12
β’ (π β
No β dom π
β On) |
109 | 92, 108 | syl 17 |
. . . . . . . . . . 11
β’
(((((π΄ β No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΄ β§ Β¬ π <s (π βΎ dom π))) β§ π β π) β dom π β On) |
110 | 109 | adantr 482 |
. . . . . . . . . 10
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΄ β§ Β¬ π <s (π βΎ dom π))) β§ π β π) β§ β© {π β On β£ (πβπ) β (πβπ)} β dom π) β dom π β On) |
111 | | sltres 27026 |
. . . . . . . . . 10
β’ ((π β
No β§ π β
No β§ dom π β On) β ((π βΎ dom π) <s (π βΎ dom π) β π <s π)) |
112 | 57, 65, 110, 111 | syl3anc 1372 |
. . . . . . . . 9
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΄ β§ Β¬ π <s (π βΎ dom π))) β§ π β π) β§ β© {π β On β£ (πβπ) β (πβπ)} β dom π) β ((π βΎ dom π) <s (π βΎ dom π) β π <s π)) |
113 | 107, 112 | sylbird 260 |
. . . . . . . 8
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΄ β§ Β¬ π <s (π βΎ dom π))) β§ π β π) β§ β© {π β On β£ (πβπ) β (πβπ)} β dom π) β ((π βΎ dom π) <s π β π <s π)) |
114 | | simplrr 777 |
. . . . . . . . . 10
β’
(((((π΄ β No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΄ β§ Β¬ π <s (π βΎ dom π))) β§ π β π) β Β¬ π <s (π βΎ dom π)) |
115 | 114 | adantr 482 |
. . . . . . . . 9
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΄ β§ Β¬ π <s (π βΎ dom π))) β§ π β π) β§ β© {π β On β£ (πβπ) β (πβπ)} β dom π) β Β¬ π <s (π βΎ dom π)) |
116 | | noreson 27024 |
. . . . . . . . . . . . 13
β’ ((π β
No β§ dom π
β On) β (π
βΎ dom π) β No ) |
117 | 56, 109, 116 | syl2anc 585 |
. . . . . . . . . . . 12
β’
(((((π΄ β No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΄ β§ Β¬ π <s (π βΎ dom π))) β§ π β π) β (π βΎ dom π) β No
) |
118 | 117 | adantr 482 |
. . . . . . . . . . 11
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΄ β§ Β¬ π <s (π βΎ dom π))) β§ π β π) β§ β© {π β On β£ (πβπ) β (πβπ)} β dom π) β (π βΎ dom π) β No
) |
119 | | sltso 27040 |
. . . . . . . . . . . 12
β’ <s Or
No |
120 | | sotric 5574 |
. . . . . . . . . . . 12
β’ (( <s
Or No β§ (π β No
β§ (π βΎ dom π) β
No )) β (π
<s (π βΎ dom π) β Β¬ (π = (π βΎ dom π) β¨ (π βΎ dom π) <s π))) |
121 | 119, 120 | mpan 689 |
. . . . . . . . . . 11
β’ ((π β
No β§ (π βΎ
dom π) β No ) β (π <s (π βΎ dom π) β Β¬ (π = (π βΎ dom π) β¨ (π βΎ dom π) <s π))) |
122 | 93, 118, 121 | syl2anc 585 |
. . . . . . . . . 10
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΄ β§ Β¬ π <s (π βΎ dom π))) β§ π β π) β§ β© {π β On β£ (πβπ) β (πβπ)} β dom π) β (π <s (π βΎ dom π) β Β¬ (π = (π βΎ dom π) β¨ (π βΎ dom π) <s π))) |
123 | 122 | con2bid 355 |
. . . . . . . . 9
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΄ β§ Β¬ π <s (π βΎ dom π))) β§ π β π) β§ β© {π β On β£ (πβπ) β (πβπ)} β dom π) β ((π = (π βΎ dom π) β¨ (π βΎ dom π) <s π) β Β¬ π <s (π βΎ dom π))) |
124 | 115, 123 | mpbird 257 |
. . . . . . . 8
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΄ β§ Β¬ π <s (π βΎ dom π))) β§ π β π) β§ β© {π β On β£ (πβπ) β (πβπ)} β dom π) β (π = (π βΎ dom π) β¨ (π βΎ dom π) <s π)) |
125 | 106, 113,
124 | mpjaod 859 |
. . . . . . 7
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΄ β§ Β¬ π <s (π βΎ dom π))) β§ π β π) β§ β© {π β On β£ (πβπ) β (πβπ)} β dom π) β π <s π) |
126 | 64 | adantr 482 |
. . . . . . . 8
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΄ β§ Β¬ π <s (π βΎ dom π))) β§ π β π) β§ dom π β β© {π β On β£ (πβπ) β (πβπ)}) β π β No
) |
127 | 56 | adantr 482 |
. . . . . . . 8
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΄ β§ Β¬ π <s (π βΎ dom π))) β§ π β π) β§ dom π β β© {π β On β£ (πβπ) β (πβπ)}) β π β No
) |
128 | | simplr 768 |
. . . . . . . . 9
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΄ β§ Β¬ π <s (π βΎ dom π))) β§ π β π) β§ dom π β β© {π β On β£ (πβπ) β (πβπ)}) β π β π) |
129 | 128 | necomd 2996 |
. . . . . . . 8
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΄ β§ Β¬ π <s (π βΎ dom π))) β§ π β π) β§ dom π β β© {π β On β£ (πβπ) β (πβπ)}) β π β π) |
130 | 41 | fveq1i 6844 |
. . . . . . . . 9
β’ (πββ© {π
β On β£ (πβπ) β (πβπ)}) = ((π βͺ ((suc βͺ
( bday β π΄) β dom π) Γ {2o}))ββ© {π
β On β£ (πβπ) β (πβπ)}) |
131 | 92 | adantr 482 |
. . . . . . . . . . . . 13
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΄ β§ Β¬ π <s (π βΎ dom π))) β§ π β π) β§ dom π β β© {π β On β£ (πβπ) β (πβπ)}) β π β No
) |
132 | 131, 94 | syl 17 |
. . . . . . . . . . . 12
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΄ β§ Β¬ π <s (π βΎ dom π))) β§ π β π) β§ dom π β β© {π β On β£ (πβπ) β (πβπ)}) β Fun π) |
133 | 132 | funfnd 6533 |
. . . . . . . . . . 11
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΄ β§ Β¬ π <s (π βΎ dom π))) β§ π β π) β§ dom π β β© {π β On β£ (πβπ) β (πβπ)}) β π Fn dom π) |
134 | | fnconstg 6731 |
. . . . . . . . . . . . 13
β’
(2o β V β ((suc βͺ ( bday β π΄) β dom π) Γ {2o}) Fn (suc βͺ ( bday β π΄) β dom π)) |
135 | 44, 134 | ax-mp 5 |
. . . . . . . . . . . 12
β’ ((suc
βͺ ( bday β π΄) β dom π) Γ {2o}) Fn (suc βͺ ( bday β π΄) β dom π) |
136 | 135 | a1i 11 |
. . . . . . . . . . 11
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΄ β§ Β¬ π <s (π βΎ dom π))) β§ π β π) β§ dom π β β© {π β On β£ (πβπ) β (πβπ)}) β ((suc βͺ
( bday β π΄) β dom π) Γ {2o}) Fn (suc βͺ ( bday β π΄) β dom π)) |
137 | | disjdif 4432 |
. . . . . . . . . . . 12
β’ (dom
π β© (suc βͺ ( bday β π΄) β dom π)) = β
|
138 | 137 | a1i 11 |
. . . . . . . . . . 11
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΄ β§ Β¬ π <s (π βΎ dom π))) β§ π β π) β§ dom π β β© {π β On β£ (πβπ) β (πβπ)}) β (dom π β© (suc βͺ
( bday β π΄) β dom π)) = β
) |
139 | | nosepssdm 27050 |
. . . . . . . . . . . . . 14
β’ ((π β
No β§ π β
No β§ π β π) β β© {π β On β£ (πβπ) β (πβπ)} β dom π) |
140 | 127, 126,
128, 139 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΄ β§ Β¬ π <s (π βΎ dom π))) β§ π β π) β§ dom π β β© {π β On β£ (πβπ) β (πβπ)}) β β©
{π β On β£ (πβπ) β (πβπ)} β dom π) |
141 | 127, 14 | syl 17 |
. . . . . . . . . . . . . . 15
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΄ β§ Β¬ π <s (π βΎ dom π))) β§ π β π) β§ dom π β β© {π β On β£ (πβπ) β (πβπ)}) β ( bday
βπ) = dom
π) |
142 | | simp-5l 784 |
. . . . . . . . . . . . . . . . 17
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΄ β§ Β¬ π <s (π βΎ dom π))) β§ π β π) β§ dom π β β© {π β On β£ (πβπ) β (πβπ)}) β π΄ β No
) |
143 | | simplrl 776 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π΄ β No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΄ β§ Β¬ π <s (π βΎ dom π))) β§ π β π) β π β π΄) |
144 | 143 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΄ β§ Β¬ π <s (π βΎ dom π))) β§ π β π) β§ dom π β β© {π β On β£ (πβπ) β (πβπ)}) β π β π΄) |
145 | 18, 142, 144, 19 | mp3an2i 1467 |
. . . . . . . . . . . . . . . 16
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΄ β§ Β¬ π <s (π βΎ dom π))) β§ π β π) β§ dom π β β© {π β On β£ (πβπ) β (πβπ)}) β ( bday
βπ) β
( bday β π΄)) |
146 | | elssuni 4899 |
. . . . . . . . . . . . . . . 16
β’ (( bday βπ) β ( bday
β π΄) β ( bday βπ) β βͺ ( bday β π΄)) |
147 | 145, 146 | syl 17 |
. . . . . . . . . . . . . . 15
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΄ β§ Β¬ π <s (π βΎ dom π))) β§ π β π) β§ dom π β β© {π β On β£ (πβπ) β (πβπ)}) β ( bday
βπ) β
βͺ ( bday β π΄)) |
148 | 141, 147 | eqsstrrd 3984 |
. . . . . . . . . . . . . 14
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΄ β§ Β¬ π <s (π βΎ dom π))) β§ π β π) β§ dom π β β© {π β On β£ (πβπ) β (πβπ)}) β dom π β βͺ ( bday β π΄)) |
149 | 127, 24, 32 | 3syl 18 |
. . . . . . . . . . . . . 14
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΄ β§ Β¬ π <s (π βΎ dom π))) β§ π β π) β§ dom π β β© {π β On β£ (πβπ) β (πβπ)}) β (dom π β βͺ ( bday β π΄) β dom π β suc βͺ
( bday β π΄))) |
150 | 148, 149 | mpbid 231 |
. . . . . . . . . . . . 13
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΄ β§ Β¬ π <s (π βΎ dom π))) β§ π β π) β§ dom π β β© {π β On β£ (πβπ) β (πβπ)}) β dom π β suc βͺ
( bday β π΄)) |
151 | | simpr 486 |
. . . . . . . . . . . . . . . 16
β’
(((((π΄ β No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΄ β§ Β¬ π <s (π βΎ dom π))) β§ π β π) β π β π) |
152 | | nosepon 27029 |
. . . . . . . . . . . . . . . 16
β’ ((π β
No β§ π β
No β§ π β π) β β© {π β On β£ (πβπ) β (πβπ)} β On) |
153 | 56, 64, 151, 152 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
β’
(((((π΄ β No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΄ β§ Β¬ π <s (π βΎ dom π))) β§ π β π) β β© {π β On β£ (πβπ) β (πβπ)} β On) |
154 | 153 | adantr 482 |
. . . . . . . . . . . . . 14
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΄ β§ Β¬ π <s (π βΎ dom π))) β§ π β π) β§ dom π β β© {π β On β£ (πβπ) β (πβπ)}) β β©
{π β On β£ (πβπ) β (πβπ)} β On) |
155 | | eloni 6328 |
. . . . . . . . . . . . . 14
β’ (β© {π
β On β£ (πβπ) β (πβπ)} β On β Ord β© {π
β On β£ (πβπ) β (πβπ)}) |
156 | | ordsuc 7749 |
. . . . . . . . . . . . . . . 16
β’ (Ord
βͺ ( bday β π΄) β Ord suc βͺ ( bday β π΄)) |
157 | 30, 156 | mpbi 229 |
. . . . . . . . . . . . . . 15
β’ Ord suc
βͺ ( bday β π΄) |
158 | | ordtr2 6362 |
. . . . . . . . . . . . . . 15
β’ ((Ord
β© {π β On β£ (πβπ) β (πβπ)} β§ Ord suc βͺ
( bday β π΄)) β ((β©
{π β On β£ (πβπ) β (πβπ)} β dom π β§ dom π β suc βͺ
( bday β π΄)) β β©
{π β On β£ (πβπ) β (πβπ)} β suc βͺ
( bday β π΄))) |
159 | 157, 158 | mpan2 690 |
. . . . . . . . . . . . . 14
β’ (Ord
β© {π β On β£ (πβπ) β (πβπ)} β ((β©
{π β On β£ (πβπ) β (πβπ)} β dom π β§ dom π β suc βͺ
( bday β π΄)) β β©
{π β On β£ (πβπ) β (πβπ)} β suc βͺ
( bday β π΄))) |
160 | 154, 155,
159 | 3syl 18 |
. . . . . . . . . . . . 13
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΄ β§ Β¬ π <s (π βΎ dom π))) β§ π β π) β§ dom π β β© {π β On β£ (πβπ) β (πβπ)}) β ((β©
{π β On β£ (πβπ) β (πβπ)} β dom π β§ dom π β suc βͺ
( bday β π΄)) β β©
{π β On β£ (πβπ) β (πβπ)} β suc βͺ
( bday β π΄))) |
161 | 140, 150,
160 | mp2and 698 |
. . . . . . . . . . . 12
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΄ β§ Β¬ π <s (π βΎ dom π))) β§ π β π) β§ dom π β β© {π β On β£ (πβπ) β (πβπ)}) β β©
{π β On β£ (πβπ) β (πβπ)} β suc βͺ
( bday β π΄)) |
162 | | ontri1 6352 |
. . . . . . . . . . . . . 14
β’ ((dom
π β On β§ β© {π
β On β£ (πβπ) β (πβπ)} β On) β (dom π β β© {π β On β£ (πβπ) β (πβπ)} β Β¬ β©
{π β On β£ (πβπ) β (πβπ)} β dom π)) |
163 | 109, 153,
162 | syl2anc 585 |
. . . . . . . . . . . . 13
β’
(((((π΄ β No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΄ β§ Β¬ π <s (π βΎ dom π))) β§ π β π) β (dom π β β© {π β On β£ (πβπ) β (πβπ)} β Β¬ β©
{π β On β£ (πβπ) β (πβπ)} β dom π)) |
164 | 163 | biimpa 478 |
. . . . . . . . . . . 12
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΄ β§ Β¬ π <s (π βΎ dom π))) β§ π β π) β§ dom π β β© {π β On β£ (πβπ) β (πβπ)}) β Β¬ β©
{π β On β£ (πβπ) β (πβπ)} β dom π) |
165 | 161, 164 | eldifd 3922 |
. . . . . . . . . . 11
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΄ β§ Β¬ π <s (π βΎ dom π))) β§ π β π) β§ dom π β β© {π β On β£ (πβπ) β (πβπ)}) β β©
{π β On β£ (πβπ) β (πβπ)} β (suc βͺ
( bday β π΄) β dom π)) |
166 | 133, 136,
138, 165 | fvun2d 6936 |
. . . . . . . . . 10
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΄ β§ Β¬ π <s (π βΎ dom π))) β§ π β π) β§ dom π β β© {π β On β£ (πβπ) β (πβπ)}) β ((π βͺ ((suc βͺ
( bday β π΄) β dom π) Γ {2o}))ββ© {π
β On β£ (πβπ) β (πβπ)}) = (((suc βͺ
( bday β π΄) β dom π) Γ {2o})ββ© {π
β On β£ (πβπ) β (πβπ)})) |
167 | 44 | fvconst2 7154 |
. . . . . . . . . . 11
β’ (β© {π
β On β£ (πβπ) β (πβπ)} β (suc βͺ
( bday β π΄) β dom π) β (((suc βͺ
( bday β π΄) β dom π) Γ {2o})ββ© {π
β On β£ (πβπ) β (πβπ)}) = 2o) |
168 | 165, 167 | syl 17 |
. . . . . . . . . 10
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΄ β§ Β¬ π <s (π βΎ dom π))) β§ π β π) β§ dom π β β© {π β On β£ (πβπ) β (πβπ)}) β (((suc βͺ ( bday β π΄) β dom π) Γ {2o})ββ© {π
β On β£ (πβπ) β (πβπ)}) = 2o) |
169 | 166, 168 | eqtrd 2773 |
. . . . . . . . 9
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΄ β§ Β¬ π <s (π βΎ dom π))) β§ π β π) β§ dom π β β© {π β On β£ (πβπ) β (πβπ)}) β ((π βͺ ((suc βͺ
( bday β π΄) β dom π) Γ {2o}))ββ© {π
β On β£ (πβπ) β (πβπ)}) = 2o) |
170 | 130, 169 | eqtrid 2785 |
. . . . . . . 8
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΄ β§ Β¬ π <s (π βΎ dom π))) β§ π β π) β§ dom π β β© {π β On β£ (πβπ) β (πβπ)}) β (πββ© {π β On β£ (πβπ) β (πβπ)}) = 2o) |
171 | | nosep2o 27046 |
. . . . . . . 8
β’ (((π β
No β§ π β
No β§ π β π) β§ (πββ© {π β On β£ (πβπ) β (πβπ)}) = 2o) β π <s π) |
172 | 126, 127,
129, 170, 171 | syl31anc 1374 |
. . . . . . 7
β’
((((((π΄ β
No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΄ β§ Β¬ π <s (π βΎ dom π))) β§ π β π) β§ dom π β β© {π β On β£ (πβπ) β (πβπ)}) β π <s π) |
173 | 153, 155 | syl 17 |
. . . . . . . 8
β’
(((((π΄ β No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΄ β§ Β¬ π <s (π βΎ dom π))) β§ π β π) β Ord β©
{π β On β£ (πβπ) β (πβπ)}) |
174 | | nodmord 27017 |
. . . . . . . . 9
β’ (π β
No β Ord dom π) |
175 | 92, 174 | syl 17 |
. . . . . . . 8
β’
(((((π΄ β No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΄ β§ Β¬ π <s (π βΎ dom π))) β§ π β π) β Ord dom π) |
176 | | ordtri2or 6416 |
. . . . . . . 8
β’ ((Ord
β© {π β On β£ (πβπ) β (πβπ)} β§ Ord dom π) β (β©
{π β On β£ (πβπ) β (πβπ)} β dom π β¨ dom π β β© {π β On β£ (πβπ) β (πβπ)})) |
177 | 173, 175,
176 | syl2anc 585 |
. . . . . . 7
β’
(((((π΄ β No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΄ β§ Β¬ π <s (π βΎ dom π))) β§ π β π) β (β©
{π β On β£ (πβπ) β (πβπ)} β dom π β¨ dom π β β© {π β On β£ (πβπ) β (πβπ)})) |
178 | 125, 172,
177 | mpjaodan 958 |
. . . . . 6
β’
(((((π΄ β No β§ π΄ β V) β§ (π΅ β No
β§ π΅ β V)) β§
(π β π΄ β§ Β¬ π <s (π βΎ dom π))) β§ π β π) β π <s π) |
179 | 54, 178 | mpdan 686 |
. . . . 5
β’ ((((π΄ β
No β§ π΄ β
V) β§ (π΅ β No β§ π΅ β V)) β§ (π β π΄ β§ Β¬ π <s (π βΎ dom π))) β π <s π) |
180 | 179 | expr 458 |
. . . 4
β’ ((((π΄ β
No β§ π΄ β
V) β§ (π΅ β No β§ π΅ β V)) β§ π β π΄) β (Β¬ π <s (π βΎ dom π) β π <s π)) |
181 | 7, 180 | sylbid 239 |
. . 3
β’ ((((π΄ β
No β§ π΄ β
V) β§ (π΅ β No β§ π΅ β V)) β§ π β π΄) β (βπ β π΅ π <s π β π <s π)) |
182 | 181 | ralimdva 3161 |
. 2
β’ (((π΄ β
No β§ π΄ β
V) β§ (π΅ β No β§ π΅ β V)) β (βπ β π΄ βπ β π΅ π <s π β βπ β π΄ π <s π)) |
183 | 182 | 3impia 1118 |
1
β’ (((π΄ β
No β§ π΄ β
V) β§ (π΅ β No β§ π΅ β V) β§ βπ β π΄ βπ β π΅ π <s π) β βπ β π΄ π <s π) |