Proof of Theorem scutbdaybnd2lim
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | scutbdaybnd2 27861 | . . . 4
⊢ (𝐴 <<s 𝐵 → ( bday
‘(𝐴 |s 𝐵)) ⊆ suc ∪ ( bday  “ (𝐴 ∪ 𝐵))) | 
| 2 | 1 | adantr 480 | . . 3
⊢ ((𝐴 <<s 𝐵 ∧ Lim ( bday
‘(𝐴 |s 𝐵))) → ( bday ‘(𝐴 |s 𝐵)) ⊆ suc ∪
( bday  “ (𝐴 ∪ 𝐵))) | 
| 3 |  | bdayfun 27817 | . . . . . . . . 9
⊢ Fun  bday | 
| 4 |  | ssltex1 27831 | . . . . . . . . . 10
⊢ (𝐴 <<s 𝐵 → 𝐴 ∈ V) | 
| 5 |  | ssltex2 27832 | . . . . . . . . . 10
⊢ (𝐴 <<s 𝐵 → 𝐵 ∈ V) | 
| 6 |  | unexg 7763 | . . . . . . . . . 10
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴 ∪ 𝐵) ∈ V) | 
| 7 | 4, 5, 6 | syl2anc 584 | . . . . . . . . 9
⊢ (𝐴 <<s 𝐵 → (𝐴 ∪ 𝐵) ∈ V) | 
| 8 |  | funimaexg 6653 | . . . . . . . . 9
⊢ ((Fun
 bday  ∧ (𝐴 ∪ 𝐵) ∈ V) → (
bday  “ (𝐴
∪ 𝐵)) ∈
V) | 
| 9 | 3, 7, 8 | sylancr 587 | . . . . . . . 8
⊢ (𝐴 <<s 𝐵 → ( bday 
“ (𝐴 ∪ 𝐵)) ∈ V) | 
| 10 | 9 | uniexd 7762 | . . . . . . 7
⊢ (𝐴 <<s 𝐵 → ∪ ( bday  “ (𝐴 ∪ 𝐵)) ∈ V) | 
| 11 | 10 | adantr 480 | . . . . . 6
⊢ ((𝐴 <<s 𝐵 ∧ Lim ( bday
‘(𝐴 |s 𝐵))) → ∪ ( bday  “ (𝐴 ∪ 𝐵)) ∈ V) | 
| 12 |  | nlimsucg 7863 | . . . . . 6
⊢ (∪ ( bday  “ (𝐴 ∪ 𝐵)) ∈ V → ¬ Lim suc ∪ ( bday  “ (𝐴 ∪ 𝐵))) | 
| 13 | 11, 12 | syl 17 | . . . . 5
⊢ ((𝐴 <<s 𝐵 ∧ Lim ( bday
‘(𝐴 |s 𝐵))) → ¬ Lim suc ∪ ( bday  “ (𝐴 ∪ 𝐵))) | 
| 14 |  | limeq 6396 | . . . . . . 7
⊢ (( bday ‘(𝐴 |s 𝐵)) = suc ∪ ( bday  “ (𝐴 ∪ 𝐵)) → (Lim ( bday
‘(𝐴 |s 𝐵)) ↔ Lim suc ∪ ( bday  “ (𝐴 ∪ 𝐵)))) | 
| 15 | 14 | biimpcd 249 | . . . . . 6
⊢ (Lim
( bday ‘(𝐴 |s 𝐵)) → (( bday
‘(𝐴 |s 𝐵)) = suc ∪ ( bday  “ (𝐴 ∪ 𝐵)) → Lim suc ∪ ( bday  “ (𝐴 ∪ 𝐵)))) | 
| 16 | 15 | adantl 481 | . . . . 5
⊢ ((𝐴 <<s 𝐵 ∧ Lim ( bday
‘(𝐴 |s 𝐵))) → (( bday ‘(𝐴 |s 𝐵)) = suc ∪ ( bday  “ (𝐴 ∪ 𝐵)) → Lim suc ∪ ( bday  “ (𝐴 ∪ 𝐵)))) | 
| 17 | 13, 16 | mtod 198 | . . . 4
⊢ ((𝐴 <<s 𝐵 ∧ Lim ( bday
‘(𝐴 |s 𝐵))) → ¬ ( bday ‘(𝐴 |s 𝐵)) = suc ∪ ( bday  “ (𝐴 ∪ 𝐵))) | 
| 18 | 17 | neqned 2947 | . . 3
⊢ ((𝐴 <<s 𝐵 ∧ Lim ( bday
‘(𝐴 |s 𝐵))) → ( bday ‘(𝐴 |s 𝐵)) ≠ suc ∪
( bday  “ (𝐴 ∪ 𝐵))) | 
| 19 |  | bdayelon 27821 | . . . . 5
⊢ ( bday ‘(𝐴 |s 𝐵)) ∈ On | 
| 20 | 19 | onordi 6495 | . . . 4
⊢ Ord
( bday ‘(𝐴 |s 𝐵)) | 
| 21 |  | imassrn 6089 | . . . . . . 7
⊢ ( bday  “ (𝐴 ∪ 𝐵)) ⊆ ran  bday | 
| 22 |  | bdayrn 27820 | . . . . . . 7
⊢ ran  bday  = On | 
| 23 | 21, 22 | sseqtri 4032 | . . . . . 6
⊢ ( bday  “ (𝐴 ∪ 𝐵)) ⊆ On | 
| 24 |  | ssorduni 7799 | . . . . . 6
⊢ (( bday  “ (𝐴 ∪ 𝐵)) ⊆ On → Ord ∪ ( bday  “ (𝐴 ∪ 𝐵))) | 
| 25 | 23, 24 | ax-mp 5 | . . . . 5
⊢ Ord ∪ ( bday  “ (𝐴 ∪ 𝐵)) | 
| 26 |  | ordsuc 7833 | . . . . 5
⊢ (Ord
∪ ( bday  “
(𝐴 ∪ 𝐵)) ↔ Ord suc ∪ ( bday  “ (𝐴 ∪ 𝐵))) | 
| 27 | 25, 26 | mpbi 230 | . . . 4
⊢ Ord suc
∪ ( bday  “
(𝐴 ∪ 𝐵)) | 
| 28 |  | ordelssne 6411 | . . . 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 583 | . 2
⊢ ((𝐴 <<s 𝐵 ∧ Lim ( bday
‘(𝐴 |s 𝐵))) → ( bday ‘(𝐴 |s 𝐵)) ∈ suc ∪
( bday  “ (𝐴 ∪ 𝐵))) | 
| 31 | 19 | a1i 11 | . . 3
⊢ ((𝐴 <<s 𝐵 ∧ Lim ( bday
‘(𝐴 |s 𝐵))) → ( bday ‘(𝐴 |s 𝐵)) ∈ On) | 
| 32 |  | ordsssuc 6473 | . . 3
⊢ ((( bday ‘(𝐴 |s 𝐵)) ∈ On ∧ Ord ∪ ( bday  “ (𝐴 ∪ 𝐵))) → (( bday
‘(𝐴 |s 𝐵)) ⊆ ∪ ( bday  “ (𝐴 ∪ 𝐵)) ↔ ( bday
‘(𝐴 |s 𝐵)) ∈ suc ∪ ( bday  “ (𝐴 ∪ 𝐵)))) | 
| 33 | 31, 25, 32 | sylancl 586 | . 2
⊢ ((𝐴 <<s 𝐵 ∧ Lim ( bday
‘(𝐴 |s 𝐵))) → (( bday ‘(𝐴 |s 𝐵)) ⊆ ∪
( bday  “ (𝐴 ∪ 𝐵)) ↔ ( bday
‘(𝐴 |s 𝐵)) ∈ suc ∪ ( bday  “ (𝐴 ∪ 𝐵)))) | 
| 34 | 30, 33 | mpbird 257 | 1
⊢ ((𝐴 <<s 𝐵 ∧ Lim ( bday
‘(𝐴 |s 𝐵))) → ( bday ‘(𝐴 |s 𝐵)) ⊆ ∪
( bday  “ (𝐴 ∪ 𝐵))) |