Step | Hyp | Ref
| Expression |
1 | | id 22 |
. 2
β’ (((π΄ β
No β§ π΄ β
π) β§ (π΅ β No
β§ π΅ β π) β§ βπ₯ β π΄ βπ¦ β π΅ π₯ <s π¦) β ((π΄ β No
β§ π΄ β π) β§ (π΅ β No
β§ π΅ β π) β§ βπ₯ β π΄ βπ¦ β π΅ π₯ <s π¦)) |
2 | | bdayfo 27041 |
. . . . . . 7
β’ bday : No βontoβOn |
3 | | fofun 6758 |
. . . . . . 7
β’ ( bday : No βontoβOn β Fun
bday ) |
4 | 2, 3 | ax-mp 5 |
. . . . . 6
β’ Fun bday |
5 | | simp1r 1199 |
. . . . . . 7
β’ (((π΄ β
No β§ π΄ β
π) β§ (π΅ β No
β§ π΅ β π) β§ βπ₯ β π΄ βπ¦ β π΅ π₯ <s π¦) β π΄ β π) |
6 | | simp2r 1201 |
. . . . . . 7
β’ (((π΄ β
No β§ π΄ β
π) β§ (π΅ β No
β§ π΅ β π) β§ βπ₯ β π΄ βπ¦ β π΅ π₯ <s π¦) β π΅ β π) |
7 | | unexg 7684 |
. . . . . . 7
β’ ((π΄ β π β§ π΅ β π) β (π΄ βͺ π΅) β V) |
8 | 5, 6, 7 | syl2anc 585 |
. . . . . 6
β’ (((π΄ β
No β§ π΄ β
π) β§ (π΅ β No
β§ π΅ β π) β§ βπ₯ β π΄ βπ¦ β π΅ π₯ <s π¦) β (π΄ βͺ π΅) β V) |
9 | | funimaexg 6588 |
. . . . . 6
β’ ((Fun
bday β§ (π΄ βͺ π΅) β V) β (
bday β (π΄
βͺ π΅)) β
V) |
10 | 4, 8, 9 | sylancr 588 |
. . . . 5
β’ (((π΄ β
No β§ π΄ β
π) β§ (π΅ β No
β§ π΅ β π) β§ βπ₯ β π΄ βπ¦ β π΅ π₯ <s π¦) β ( bday
β (π΄ βͺ π΅)) β V) |
11 | 10 | uniexd 7680 |
. . . 4
β’ (((π΄ β
No β§ π΄ β
π) β§ (π΅ β No
β§ π΅ β π) β§ βπ₯ β π΄ βπ¦ β π΅ π₯ <s π¦) β βͺ ( bday β (π΄ βͺ π΅)) β V) |
12 | | imassrn 6025 |
. . . . . . 7
β’ ( bday β (π΄ βͺ π΅)) β ran bday
|
13 | | forn 6760 |
. . . . . . . 8
β’ ( bday : No βontoβOn β ran
bday = On) |
14 | 2, 13 | ax-mp 5 |
. . . . . . 7
β’ ran bday = On |
15 | 12, 14 | sseqtri 3981 |
. . . . . 6
β’ ( bday β (π΄ βͺ π΅)) β On |
16 | | ssorduni 7714 |
. . . . . 6
β’ (( bday β (π΄ βͺ π΅)) β On β Ord βͺ ( bday β (π΄ βͺ π΅))) |
17 | 15, 16 | ax-mp 5 |
. . . . 5
β’ Ord βͺ ( bday β (π΄ βͺ π΅)) |
18 | | elon2 6329 |
. . . . 5
β’ (βͺ ( bday β (π΄ βͺ π΅)) β On β (Ord βͺ ( bday β (π΄ βͺ π΅)) β§ βͺ ( bday β (π΄ βͺ π΅)) β V)) |
19 | 17, 18 | mpbiran 708 |
. . . 4
β’ (βͺ ( bday β (π΄ βͺ π΅)) β On β βͺ ( bday β (π΄ βͺ π΅)) β V) |
20 | 11, 19 | sylibr 233 |
. . 3
β’ (((π΄ β
No β§ π΄ β
π) β§ (π΅ β No
β§ π΅ β π) β§ βπ₯ β π΄ βπ¦ β π΅ π₯ <s π¦) β βͺ ( bday β (π΄ βͺ π΅)) β On) |
21 | | onsucb 7753 |
. . 3
β’ (βͺ ( bday β (π΄ βͺ π΅)) β On β suc βͺ ( bday β (π΄ βͺ π΅)) β On) |
22 | 20, 21 | sylib 217 |
. 2
β’ (((π΄ β
No β§ π΄ β
π) β§ (π΅ β No
β§ π΅ β π) β§ βπ₯ β π΄ βπ¦ β π΅ π₯ <s π¦) β suc βͺ
( bday β (π΄ βͺ π΅)) β On) |
23 | | onsucuni 7764 |
. . 3
β’ (( bday β (π΄ βͺ π΅)) β On β (
bday β (π΄
βͺ π΅)) β suc βͺ ( bday β (π΄ βͺ π΅))) |
24 | 15, 23 | mp1i 13 |
. 2
β’ (((π΄ β
No β§ π΄ β
π) β§ (π΅ β No
β§ π΅ β π) β§ βπ₯ β π΄ βπ¦ β π΅ π₯ <s π¦) β ( bday
β (π΄ βͺ π΅)) β suc βͺ ( bday β (π΄ βͺ π΅))) |
25 | | noeta 27107 |
. 2
β’ ((((π΄ β
No β§ π΄ β
π) β§ (π΅ β No
β§ π΅ β π) β§ βπ₯ β π΄ βπ¦ β π΅ π₯ <s π¦) β§ (suc βͺ
( bday β (π΄ βͺ π΅)) β On β§ (
bday β (π΄
βͺ π΅)) β suc βͺ ( bday β (π΄ βͺ π΅)))) β βπ§ β No
(βπ₯ β π΄ π₯ <s π§ β§ βπ¦ β π΅ π§ <s π¦ β§ ( bday
βπ§) β
suc βͺ ( bday β
(π΄ βͺ π΅)))) |
26 | 1, 22, 24, 25 | syl12anc 836 |
1
β’ (((π΄ β
No β§ π΄ β
π) β§ (π΅ β No
β§ π΅ β π) β§ βπ₯ β π΄ βπ¦ β π΅ π₯ <s π¦) β βπ§ β No
(βπ₯ β π΄ π₯ <s π§ β§ βπ¦ β π΅ π§ <s π¦ β§ ( bday
βπ§) β
suc βͺ ( bday β
(π΄ βͺ π΅)))) |