Proof of Theorem scutbdaybnd2lim
Step | Hyp | Ref
| Expression |
1 | | scutbdaybnd2 33655 |
. . . 4
⊢ (𝐴 <<s 𝐵 → ( bday
‘(𝐴 |s 𝐵)) ⊆ suc ∪ ( bday “ (𝐴 ∪ 𝐵))) |
2 | 1 | adantr 484 |
. . 3
⊢ ((𝐴 <<s 𝐵 ∧ Lim ( bday
‘(𝐴 |s 𝐵))) → ( bday ‘(𝐴 |s 𝐵)) ⊆ suc ∪
( bday “ (𝐴 ∪ 𝐵))) |
3 | | bdayfun 33612 |
. . . . . . . . 9
⊢ Fun bday |
4 | | ssltex1 33626 |
. . . . . . . . . 10
⊢ (𝐴 <<s 𝐵 → 𝐴 ∈ V) |
5 | | ssltex2 33627 |
. . . . . . . . . 10
⊢ (𝐴 <<s 𝐵 → 𝐵 ∈ V) |
6 | | unexg 7492 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴 ∪ 𝐵) ∈ V) |
7 | 4, 5, 6 | syl2anc 587 |
. . . . . . . . 9
⊢ (𝐴 <<s 𝐵 → (𝐴 ∪ 𝐵) ∈ V) |
8 | | funimaexg 6425 |
. . . . . . . . 9
⊢ ((Fun
bday ∧ (𝐴 ∪ 𝐵) ∈ V) → (
bday “ (𝐴
∪ 𝐵)) ∈
V) |
9 | 3, 7, 8 | sylancr 590 |
. . . . . . . 8
⊢ (𝐴 <<s 𝐵 → ( bday
“ (𝐴 ∪ 𝐵)) ∈ V) |
10 | 9 | uniexd 7488 |
. . . . . . 7
⊢ (𝐴 <<s 𝐵 → ∪ ( bday “ (𝐴 ∪ 𝐵)) ∈ V) |
11 | 10 | adantr 484 |
. . . . . 6
⊢ ((𝐴 <<s 𝐵 ∧ Lim ( bday
‘(𝐴 |s 𝐵))) → ∪ ( bday “ (𝐴 ∪ 𝐵)) ∈ V) |
12 | | nlimsucg 7578 |
. . . . . 6
⊢ (∪ ( bday “ (𝐴 ∪ 𝐵)) ∈ V → ¬ Lim suc ∪ ( bday “ (𝐴 ∪ 𝐵))) |
13 | 11, 12 | syl 17 |
. . . . 5
⊢ ((𝐴 <<s 𝐵 ∧ Lim ( bday
‘(𝐴 |s 𝐵))) → ¬ Lim suc ∪ ( bday “ (𝐴 ∪ 𝐵))) |
14 | | limeq 6184 |
. . . . . . 7
⊢ (( bday ‘(𝐴 |s 𝐵)) = suc ∪ ( bday “ (𝐴 ∪ 𝐵)) → (Lim ( bday
‘(𝐴 |s 𝐵)) ↔ Lim suc ∪ ( bday “ (𝐴 ∪ 𝐵)))) |
15 | 14 | biimpcd 252 |
. . . . . 6
⊢ (Lim
( bday ‘(𝐴 |s 𝐵)) → (( bday
‘(𝐴 |s 𝐵)) = suc ∪ ( bday “ (𝐴 ∪ 𝐵)) → Lim suc ∪ ( bday “ (𝐴 ∪ 𝐵)))) |
16 | 15 | adantl 485 |
. . . . 5
⊢ ((𝐴 <<s 𝐵 ∧ Lim ( bday
‘(𝐴 |s 𝐵))) → (( bday ‘(𝐴 |s 𝐵)) = suc ∪ ( bday “ (𝐴 ∪ 𝐵)) → Lim suc ∪ ( bday “ (𝐴 ∪ 𝐵)))) |
17 | 13, 16 | mtod 201 |
. . . 4
⊢ ((𝐴 <<s 𝐵 ∧ Lim ( bday
‘(𝐴 |s 𝐵))) → ¬ ( bday ‘(𝐴 |s 𝐵)) = suc ∪ ( bday “ (𝐴 ∪ 𝐵))) |
18 | 17 | neqned 2941 |
. . 3
⊢ ((𝐴 <<s 𝐵 ∧ Lim ( bday
‘(𝐴 |s 𝐵))) → ( bday ‘(𝐴 |s 𝐵)) ≠ suc ∪
( bday “ (𝐴 ∪ 𝐵))) |
19 | | bdayelon 33616 |
. . . . 5
⊢ ( bday ‘(𝐴 |s 𝐵)) ∈ On |
20 | 19 | onordi 6277 |
. . . 4
⊢ Ord
( bday ‘(𝐴 |s 𝐵)) |
21 | | imassrn 5914 |
. . . . . . 7
⊢ ( bday “ (𝐴 ∪ 𝐵)) ⊆ ran bday
|
22 | | bdayrn 33615 |
. . . . . . 7
⊢ ran bday = On |
23 | 21, 22 | sseqtri 3913 |
. . . . . 6
⊢ ( bday “ (𝐴 ∪ 𝐵)) ⊆ On |
24 | | ssorduni 7521 |
. . . . . 6
⊢ (( bday “ (𝐴 ∪ 𝐵)) ⊆ On → Ord ∪ ( bday “ (𝐴 ∪ 𝐵))) |
25 | 23, 24 | ax-mp 5 |
. . . . 5
⊢ Ord ∪ ( bday “ (𝐴 ∪ 𝐵)) |
26 | | ordsuc 7550 |
. . . . 5
⊢ (Ord
∪ ( bday “
(𝐴 ∪ 𝐵)) ↔ Ord suc ∪ ( bday “ (𝐴 ∪ 𝐵))) |
27 | 25, 26 | mpbi 233 |
. . . 4
⊢ Ord suc
∪ ( bday “
(𝐴 ∪ 𝐵)) |
28 | | ordelssne 6199 |
. . . 4
⊢ ((Ord
( bday ‘(𝐴 |s 𝐵)) ∧ Ord suc ∪ ( bday “ (𝐴 ∪ 𝐵))) → (( bday
‘(𝐴 |s 𝐵)) ∈ suc ∪ ( bday “ (𝐴 ∪ 𝐵)) ↔ (( bday
‘(𝐴 |s 𝐵)) ⊆ suc ∪ ( bday “ (𝐴 ∪ 𝐵)) ∧ ( bday
‘(𝐴 |s 𝐵)) ≠ suc ∪ ( bday “ (𝐴 ∪ 𝐵))))) |
29 | 20, 27, 28 | mp2an 692 |
. . 3
⊢ (( bday ‘(𝐴 |s 𝐵)) ∈ suc ∪
( bday “ (𝐴 ∪ 𝐵)) ↔ (( bday
‘(𝐴 |s 𝐵)) ⊆ suc ∪ ( bday “ (𝐴 ∪ 𝐵)) ∧ ( bday
‘(𝐴 |s 𝐵)) ≠ suc ∪ ( bday “ (𝐴 ∪ 𝐵)))) |
30 | 2, 18, 29 | sylanbrc 586 |
. 2
⊢ ((𝐴 <<s 𝐵 ∧ Lim ( bday
‘(𝐴 |s 𝐵))) → ( bday ‘(𝐴 |s 𝐵)) ∈ suc ∪
( bday “ (𝐴 ∪ 𝐵))) |
31 | 19 | a1i 11 |
. . 3
⊢ ((𝐴 <<s 𝐵 ∧ Lim ( bday
‘(𝐴 |s 𝐵))) → ( bday ‘(𝐴 |s 𝐵)) ∈ On) |
32 | | ordsssuc 6258 |
. . 3
⊢ ((( bday ‘(𝐴 |s 𝐵)) ∈ On ∧ Ord ∪ ( bday “ (𝐴 ∪ 𝐵))) → (( bday
‘(𝐴 |s 𝐵)) ⊆ ∪ ( bday “ (𝐴 ∪ 𝐵)) ↔ ( bday
‘(𝐴 |s 𝐵)) ∈ suc ∪ ( bday “ (𝐴 ∪ 𝐵)))) |
33 | 31, 25, 32 | sylancl 589 |
. 2
⊢ ((𝐴 <<s 𝐵 ∧ Lim ( bday
‘(𝐴 |s 𝐵))) → (( bday ‘(𝐴 |s 𝐵)) ⊆ ∪
( bday “ (𝐴 ∪ 𝐵)) ↔ ( bday
‘(𝐴 |s 𝐵)) ∈ suc ∪ ( bday “ (𝐴 ∪ 𝐵)))) |
34 | 30, 33 | mpbird 260 |
1
⊢ ((𝐴 <<s 𝐵 ∧ Lim ( bday
‘(𝐴 |s 𝐵))) → ( bday ‘(𝐴 |s 𝐵)) ⊆ ∪
( bday “ (𝐴 ∪ 𝐵))) |