| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | 2fveq3 6910 | . . 3
⊢ (𝑥 = 𝑥𝑂 → ( bday ‘( -us ‘𝑥)) = ( bday
‘( -us ‘𝑥𝑂))) | 
| 2 |  | fveq2 6905 | . . 3
⊢ (𝑥 = 𝑥𝑂 → ( bday ‘𝑥) = ( bday
‘𝑥𝑂)) | 
| 3 | 1, 2 | sseq12d 4016 | . 2
⊢ (𝑥 = 𝑥𝑂 → (( bday ‘( -us ‘𝑥)) ⊆ ( bday
‘𝑥) ↔
( bday ‘( -us ‘𝑥𝑂)) ⊆
( bday ‘𝑥𝑂))) | 
| 4 |  | 2fveq3 6910 | . . 3
⊢ (𝑥 = 𝐴 → ( bday
‘( -us ‘𝑥)) = ( bday
‘( -us ‘𝐴))) | 
| 5 |  | fveq2 6905 | . . 3
⊢ (𝑥 = 𝐴 → ( bday
‘𝑥) = ( bday ‘𝐴)) | 
| 6 | 4, 5 | sseq12d 4016 | . 2
⊢ (𝑥 = 𝐴 → (( bday
‘( -us ‘𝑥)) ⊆ ( bday
‘𝑥) ↔
( bday ‘( -us ‘𝐴)) ⊆ ( bday ‘𝐴))) | 
| 7 |  | negsval 28058 | . . . . . 6
⊢ (𝑥 ∈ 
No  → ( -us ‘𝑥) = (( -us “ ( R
‘𝑥)) |s (
-us “ ( L ‘𝑥)))) | 
| 8 | 7 | fveq2d 6909 | . . . . 5
⊢ (𝑥 ∈ 
No  → ( bday ‘( -us
‘𝑥)) = ( bday ‘(( -us “ ( R ‘𝑥)) |s ( -us “ (
L ‘𝑥))))) | 
| 9 | 8 | adantr 480 | . . . 4
⊢ ((𝑥 ∈ 
No  ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))( bday
‘( -us ‘𝑥𝑂)) ⊆ ( bday ‘𝑥𝑂)) → ( bday ‘( -us ‘𝑥)) = ( bday
‘(( -us “ ( R ‘𝑥)) |s ( -us “ ( L
‘𝑥))))) | 
| 10 |  | negscut2 28073 | . . . . 5
⊢ (𝑥 ∈ 
No  → ( -us “ ( R ‘𝑥)) <<s ( -us “ ( L
‘𝑥))) | 
| 11 |  | lrold 27936 | . . . . . . . . . 10
⊢ (( L
‘𝑥) ∪ ( R
‘𝑥)) = ( O
‘( bday ‘𝑥)) | 
| 12 |  | uncom 4157 | . . . . . . . . . 10
⊢ (( L
‘𝑥) ∪ ( R
‘𝑥)) = (( R
‘𝑥) ∪ ( L
‘𝑥)) | 
| 13 | 11, 12 | eqtr3i 2766 | . . . . . . . . 9
⊢ ( O
‘( bday ‘𝑥)) = (( R ‘𝑥) ∪ ( L ‘𝑥)) | 
| 14 | 13 | imaeq2i 6075 | . . . . . . . 8
⊢ (
-us “ ( O ‘( bday
‘𝑥))) = (
-us “ (( R ‘𝑥) ∪ ( L ‘𝑥))) | 
| 15 |  | imaundi 6168 | . . . . . . . 8
⊢ (
-us “ (( R ‘𝑥) ∪ ( L ‘𝑥))) = (( -us “ ( R
‘𝑥)) ∪ (
-us “ ( L ‘𝑥))) | 
| 16 | 14, 15 | eqtri 2764 | . . . . . . 7
⊢ (
-us “ ( O ‘( bday
‘𝑥))) = ((
-us “ ( R ‘𝑥)) ∪ ( -us “ ( L
‘𝑥))) | 
| 17 | 16 | imaeq2i 6075 | . . . . . 6
⊢ ( bday  “ ( -us “ ( O
‘( bday ‘𝑥)))) = ( bday 
“ (( -us “ ( R ‘𝑥)) ∪ ( -us “ ( L
‘𝑥)))) | 
| 18 | 11 | raleqi 3323 | . . . . . . 7
⊢
(∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))( bday
‘( -us ‘𝑥𝑂)) ⊆ ( bday ‘𝑥𝑂) ↔ ∀𝑥𝑂 ∈ ( O
‘( bday ‘𝑥))( bday
‘( -us ‘𝑥𝑂)) ⊆ ( bday ‘𝑥𝑂)) | 
| 19 |  | oldbdayim 27928 | . . . . . . . . . . . 12
⊢ (𝑥𝑂 ∈ ( O
‘( bday ‘𝑥)) → ( bday
‘𝑥𝑂) ∈ ( bday ‘𝑥)) | 
| 20 | 19 | adantl 481 | . . . . . . . . . . 11
⊢ ((𝑥 ∈ 
No  ∧ 𝑥𝑂 ∈ ( O ‘( bday ‘𝑥))) → ( bday
‘𝑥𝑂) ∈ ( bday ‘𝑥)) | 
| 21 |  | bdayelon 27822 | . . . . . . . . . . . . 13
⊢ ( bday ‘( -us ‘𝑥𝑂)) ∈
On | 
| 22 |  | bdayelon 27822 | . . . . . . . . . . . . 13
⊢ ( bday ‘𝑥) ∈ On | 
| 23 |  | ontr2 6430 | . . . . . . . . . . . . 13
⊢ ((( bday ‘( -us ‘𝑥𝑂)) ∈ On ∧ ( bday ‘𝑥) ∈ On) → (((
bday ‘( -us ‘𝑥𝑂)) ⊆ ( bday ‘𝑥𝑂) ∧ ( bday ‘𝑥𝑂) ∈ ( bday ‘𝑥)) → ( bday
‘( -us ‘𝑥𝑂)) ∈ ( bday ‘𝑥))) | 
| 24 | 21, 22, 23 | mp2an 692 | . . . . . . . . . . . 12
⊢ ((( bday ‘( -us ‘𝑥𝑂)) ⊆ ( bday ‘𝑥𝑂) ∧ ( bday ‘𝑥𝑂) ∈ ( bday ‘𝑥)) → ( bday
‘( -us ‘𝑥𝑂)) ∈ ( bday ‘𝑥)) | 
| 25 | 24 | a1i 11 | . . . . . . . . . . 11
⊢ ((𝑥 ∈ 
No  ∧ 𝑥𝑂 ∈ ( O ‘( bday ‘𝑥))) → ((( bday
‘( -us ‘𝑥𝑂)) ⊆ ( bday ‘𝑥𝑂) ∧ ( bday ‘𝑥𝑂) ∈ ( bday ‘𝑥)) → ( bday
‘( -us ‘𝑥𝑂)) ∈ ( bday ‘𝑥))) | 
| 26 | 20, 25 | mpan2d 694 | . . . . . . . . . 10
⊢ ((𝑥 ∈ 
No  ∧ 𝑥𝑂 ∈ ( O ‘( bday ‘𝑥))) → (( bday
‘( -us ‘𝑥𝑂)) ⊆ ( bday ‘𝑥𝑂) → ( bday ‘( -us ‘𝑥𝑂)) ∈ ( bday ‘𝑥))) | 
| 27 | 26 | ralimdva 3166 | . . . . . . . . 9
⊢ (𝑥 ∈ 
No  → (∀𝑥𝑂 ∈ ( O ‘( bday ‘𝑥))( bday
‘( -us ‘𝑥𝑂)) ⊆ ( bday ‘𝑥𝑂) → ∀𝑥𝑂 ∈ ( O
‘( bday ‘𝑥))( bday
‘( -us ‘𝑥𝑂)) ∈ ( bday ‘𝑥))) | 
| 28 | 27 | imp 406 | . . . . . . . 8
⊢ ((𝑥 ∈ 
No  ∧ ∀𝑥𝑂 ∈ ( O ‘( bday ‘𝑥))( bday
‘( -us ‘𝑥𝑂)) ⊆ ( bday ‘𝑥𝑂)) → ∀𝑥𝑂 ∈ ( O
‘( bday ‘𝑥))( bday
‘( -us ‘𝑥𝑂)) ∈ ( bday ‘𝑥)) | 
| 29 |  | bdayfun 27818 | . . . . . . . . . 10
⊢ Fun  bday | 
| 30 |  | imassrn 6088 | . . . . . . . . . . 11
⊢ (
-us “ ( O ‘( bday
‘𝑥))) ⊆
ran -us | 
| 31 |  | bdaydm 27820 | . . . . . . . . . . . 12
⊢ dom  bday  =  No | 
| 32 |  | negsfo 28086 | . . . . . . . . . . . . 13
⊢ 
-us : No –onto→ No | 
| 33 |  | forn 6822 | . . . . . . . . . . . . 13
⊢ (
-us : No –onto→ No  → ran
-us =  No ) | 
| 34 | 32, 33 | ax-mp 5 | . . . . . . . . . . . 12
⊢ ran
-us =  No | 
| 35 | 31, 34 | eqtr4i 2767 | . . . . . . . . . . 11
⊢ dom  bday  = ran -us | 
| 36 | 30, 35 | sseqtrri 4032 | . . . . . . . . . 10
⊢ (
-us “ ( O ‘( bday
‘𝑥))) ⊆
dom  bday | 
| 37 |  | funimass4 6972 | . . . . . . . . . 10
⊢ ((Fun
 bday  ∧ ( -us “ ( O
‘( bday ‘𝑥))) ⊆ dom  bday
) → (( bday  “ ( -us
“ ( O ‘( bday ‘𝑥)))) ⊆ ( bday ‘𝑥) ↔ ∀𝑦 ∈ ( -us “ ( O
‘( bday ‘𝑥)))( bday
‘𝑦) ∈
( bday ‘𝑥))) | 
| 38 | 29, 36, 37 | mp2an 692 | . . . . . . . . 9
⊢ (( bday  “ ( -us “ ( O
‘( bday ‘𝑥)))) ⊆ ( bday
‘𝑥) ↔
∀𝑦 ∈ (
-us “ ( O ‘( bday
‘𝑥)))( bday ‘𝑦) ∈ ( bday
‘𝑥)) | 
| 39 |  | negsfn 28056 | . . . . . . . . . 10
⊢ 
-us Fn  No | 
| 40 |  | oldssno 27901 | . . . . . . . . . 10
⊢ ( O
‘( bday ‘𝑥)) ⊆  No | 
| 41 |  | fveq2 6905 | . . . . . . . . . . . 12
⊢ (𝑦 = ( -us ‘𝑥𝑂) →
( bday ‘𝑦) = ( bday
‘( -us ‘𝑥𝑂))) | 
| 42 | 41 | eleq1d 2825 | . . . . . . . . . . 11
⊢ (𝑦 = ( -us ‘𝑥𝑂) →
(( bday ‘𝑦) ∈ ( bday
‘𝑥) ↔
( bday ‘( -us ‘𝑥𝑂)) ∈
( bday ‘𝑥))) | 
| 43 | 42 | ralima 7258 | . . . . . . . . . 10
⊢ ((
-us Fn  No  ∧ ( O ‘( bday ‘𝑥)) ⊆  No )
→ (∀𝑦 ∈ (
-us “ ( O ‘( bday
‘𝑥)))( bday ‘𝑦) ∈ ( bday
‘𝑥) ↔
∀𝑥𝑂 ∈ ( O ‘( bday ‘𝑥))( bday
‘( -us ‘𝑥𝑂)) ∈ ( bday ‘𝑥))) | 
| 44 | 39, 40, 43 | mp2an 692 | . . . . . . . . 9
⊢
(∀𝑦 ∈ (
-us “ ( O ‘( bday
‘𝑥)))( bday ‘𝑦) ∈ ( bday
‘𝑥) ↔
∀𝑥𝑂 ∈ ( O ‘( bday ‘𝑥))( bday
‘( -us ‘𝑥𝑂)) ∈ ( bday ‘𝑥)) | 
| 45 | 38, 44 | bitri 275 | . . . . . . . 8
⊢ (( bday  “ ( -us “ ( O
‘( bday ‘𝑥)))) ⊆ ( bday
‘𝑥) ↔
∀𝑥𝑂 ∈ ( O ‘( bday ‘𝑥))( bday
‘( -us ‘𝑥𝑂)) ∈ ( bday ‘𝑥)) | 
| 46 | 28, 45 | sylibr 234 | . . . . . . 7
⊢ ((𝑥 ∈ 
No  ∧ ∀𝑥𝑂 ∈ ( O ‘( bday ‘𝑥))( bday
‘( -us ‘𝑥𝑂)) ⊆ ( bday ‘𝑥𝑂)) → ( bday  “ ( -us “ ( O
‘( bday ‘𝑥)))) ⊆ ( bday
‘𝑥)) | 
| 47 | 18, 46 | sylan2b 594 | . . . . . 6
⊢ ((𝑥 ∈ 
No  ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))( bday
‘( -us ‘𝑥𝑂)) ⊆ ( bday ‘𝑥𝑂)) → ( bday  “ ( -us “ ( O
‘( bday ‘𝑥)))) ⊆ ( bday
‘𝑥)) | 
| 48 | 17, 47 | eqsstrrid 4022 | . . . . 5
⊢ ((𝑥 ∈ 
No  ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))( bday
‘( -us ‘𝑥𝑂)) ⊆ ( bday ‘𝑥𝑂)) → ( bday  “ (( -us “ ( R
‘𝑥)) ∪ (
-us “ ( L ‘𝑥)))) ⊆ ( bday
‘𝑥)) | 
| 49 |  | scutbdaybnd 27861 | . . . . . 6
⊢ (((
-us “ ( R ‘𝑥)) <<s ( -us “ ( L
‘𝑥)) ∧ ( bday ‘𝑥) ∈ On ∧ (
bday  “ (( -us “ ( R ‘𝑥)) ∪ ( -us “ ( L
‘𝑥)))) ⊆ ( bday ‘𝑥)) → ( bday
‘(( -us “ ( R ‘𝑥)) |s ( -us “ ( L
‘𝑥)))) ⊆ ( bday ‘𝑥)) | 
| 50 | 22, 49 | mp3an2 1450 | . . . . 5
⊢ (((
-us “ ( R ‘𝑥)) <<s ( -us “ ( L
‘𝑥)) ∧ ( bday  “ (( -us “ ( R
‘𝑥)) ∪ (
-us “ ( L ‘𝑥)))) ⊆ ( bday
‘𝑥)) →
( bday ‘(( -us “ ( R
‘𝑥)) |s (
-us “ ( L ‘𝑥)))) ⊆ ( bday
‘𝑥)) | 
| 51 | 10, 48, 50 | syl2an2r 685 | . . . 4
⊢ ((𝑥 ∈ 
No  ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))( bday
‘( -us ‘𝑥𝑂)) ⊆ ( bday ‘𝑥𝑂)) → ( bday ‘(( -us “ ( R ‘𝑥)) |s ( -us “ (
L ‘𝑥)))) ⊆
( bday ‘𝑥)) | 
| 52 | 9, 51 | eqsstrd 4017 | . . 3
⊢ ((𝑥 ∈ 
No  ∧ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))( bday
‘( -us ‘𝑥𝑂)) ⊆ ( bday ‘𝑥𝑂)) → ( bday ‘( -us ‘𝑥)) ⊆ ( bday
‘𝑥)) | 
| 53 | 52 | ex 412 | . 2
⊢ (𝑥 ∈ 
No  → (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))( bday
‘( -us ‘𝑥𝑂)) ⊆ ( bday ‘𝑥𝑂) → ( bday ‘( -us ‘𝑥)) ⊆ ( bday
‘𝑥))) | 
| 54 | 3, 6, 53 | noinds 27979 | 1
⊢ (𝐴 ∈ 
No  → ( bday ‘( -us
‘𝐴)) ⊆ ( bday ‘𝐴)) |