Step |
Hyp |
Ref |
Expression |
1 |
|
leftval |
⊢ ( L ‘ 𝐴 ) = { 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ∣ 𝑥 <s 𝐴 } |
2 |
|
rightval |
⊢ ( R ‘ 𝐴 ) = { 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ∣ 𝐴 <s 𝑥 } |
3 |
1 2
|
uneq12i |
⊢ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) = ( { 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ∣ 𝑥 <s 𝐴 } ∪ { 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ∣ 𝐴 <s 𝑥 } ) |
4 |
|
unrab |
⊢ ( { 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ∣ 𝑥 <s 𝐴 } ∪ { 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ∣ 𝐴 <s 𝑥 } ) = { 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ∣ ( 𝑥 <s 𝐴 ∨ 𝐴 <s 𝑥 ) } |
5 |
3 4
|
eqtri |
⊢ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) = { 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ∣ ( 𝑥 <s 𝐴 ∨ 𝐴 <s 𝑥 ) } |
6 |
|
oldirr |
⊢ ¬ 𝐴 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) |
7 |
|
eleq1 |
⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ↔ 𝐴 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ) ) |
8 |
6 7
|
mtbiri |
⊢ ( 𝑥 = 𝐴 → ¬ 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ) |
9 |
8
|
necon2ai |
⊢ ( 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) → 𝑥 ≠ 𝐴 ) |
10 |
9
|
adantl |
⊢ ( ( 𝐴 ∈ No ∧ 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ) → 𝑥 ≠ 𝐴 ) |
11 |
|
oldssno |
⊢ ( O ‘ ( bday ‘ 𝐴 ) ) ⊆ No |
12 |
11
|
sseli |
⊢ ( 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) → 𝑥 ∈ No ) |
13 |
|
slttrine |
⊢ ( ( 𝑥 ∈ No ∧ 𝐴 ∈ No ) → ( 𝑥 ≠ 𝐴 ↔ ( 𝑥 <s 𝐴 ∨ 𝐴 <s 𝑥 ) ) ) |
14 |
13
|
ancoms |
⊢ ( ( 𝐴 ∈ No ∧ 𝑥 ∈ No ) → ( 𝑥 ≠ 𝐴 ↔ ( 𝑥 <s 𝐴 ∨ 𝐴 <s 𝑥 ) ) ) |
15 |
12 14
|
sylan2 |
⊢ ( ( 𝐴 ∈ No ∧ 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ) → ( 𝑥 ≠ 𝐴 ↔ ( 𝑥 <s 𝐴 ∨ 𝐴 <s 𝑥 ) ) ) |
16 |
10 15
|
mpbid |
⊢ ( ( 𝐴 ∈ No ∧ 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ) → ( 𝑥 <s 𝐴 ∨ 𝐴 <s 𝑥 ) ) |
17 |
16
|
rabeqcda |
⊢ ( 𝐴 ∈ No → { 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ∣ ( 𝑥 <s 𝐴 ∨ 𝐴 <s 𝑥 ) } = ( O ‘ ( bday ‘ 𝐴 ) ) ) |
18 |
5 17
|
eqtrid |
⊢ ( 𝐴 ∈ No → ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) = ( O ‘ ( bday ‘ 𝐴 ) ) ) |
19 |
|
un0 |
⊢ ( ∅ ∪ ∅ ) = ∅ |
20 |
|
leftf |
⊢ L : No ⟶ 𝒫 No |
21 |
20
|
fdmi |
⊢ dom L = No |
22 |
21
|
eleq2i |
⊢ ( 𝐴 ∈ dom L ↔ 𝐴 ∈ No ) |
23 |
|
ndmfv |
⊢ ( ¬ 𝐴 ∈ dom L → ( L ‘ 𝐴 ) = ∅ ) |
24 |
22 23
|
sylnbir |
⊢ ( ¬ 𝐴 ∈ No → ( L ‘ 𝐴 ) = ∅ ) |
25 |
|
rightf |
⊢ R : No ⟶ 𝒫 No |
26 |
25
|
fdmi |
⊢ dom R = No |
27 |
26
|
eleq2i |
⊢ ( 𝐴 ∈ dom R ↔ 𝐴 ∈ No ) |
28 |
|
ndmfv |
⊢ ( ¬ 𝐴 ∈ dom R → ( R ‘ 𝐴 ) = ∅ ) |
29 |
27 28
|
sylnbir |
⊢ ( ¬ 𝐴 ∈ No → ( R ‘ 𝐴 ) = ∅ ) |
30 |
24 29
|
uneq12d |
⊢ ( ¬ 𝐴 ∈ No → ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) = ( ∅ ∪ ∅ ) ) |
31 |
|
bdaydm |
⊢ dom bday = No |
32 |
31
|
eleq2i |
⊢ ( 𝐴 ∈ dom bday ↔ 𝐴 ∈ No ) |
33 |
|
ndmfv |
⊢ ( ¬ 𝐴 ∈ dom bday → ( bday ‘ 𝐴 ) = ∅ ) |
34 |
32 33
|
sylnbir |
⊢ ( ¬ 𝐴 ∈ No → ( bday ‘ 𝐴 ) = ∅ ) |
35 |
34
|
fveq2d |
⊢ ( ¬ 𝐴 ∈ No → ( O ‘ ( bday ‘ 𝐴 ) ) = ( O ‘ ∅ ) ) |
36 |
|
old0 |
⊢ ( O ‘ ∅ ) = ∅ |
37 |
35 36
|
eqtrdi |
⊢ ( ¬ 𝐴 ∈ No → ( O ‘ ( bday ‘ 𝐴 ) ) = ∅ ) |
38 |
19 30 37
|
3eqtr4a |
⊢ ( ¬ 𝐴 ∈ No → ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) = ( O ‘ ( bday ‘ 𝐴 ) ) ) |
39 |
18 38
|
pm2.61i |
⊢ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) = ( O ‘ ( bday ‘ 𝐴 ) ) |