Step |
Hyp |
Ref |
Expression |
1 |
|
fvexd |
⊢ ( 𝐴 ∈ No → ( L ‘ 𝐴 ) ∈ V ) |
2 |
|
snex |
⊢ { 𝐴 } ∈ V |
3 |
2
|
a1i |
⊢ ( 𝐴 ∈ No → { 𝐴 } ∈ V ) |
4 |
|
leftf |
⊢ L : No ⟶ 𝒫 No |
5 |
4
|
ffvelrni |
⊢ ( 𝐴 ∈ No → ( L ‘ 𝐴 ) ∈ 𝒫 No ) |
6 |
5
|
elpwid |
⊢ ( 𝐴 ∈ No → ( L ‘ 𝐴 ) ⊆ No ) |
7 |
|
snssi |
⊢ ( 𝐴 ∈ No → { 𝐴 } ⊆ No ) |
8 |
|
velsn |
⊢ ( 𝑦 ∈ { 𝐴 } ↔ 𝑦 = 𝐴 ) |
9 |
|
leftval |
⊢ ( L ‘ 𝐴 ) = { 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ∣ 𝑥 <s 𝐴 } |
10 |
9
|
a1i |
⊢ ( 𝐴 ∈ No → ( L ‘ 𝐴 ) = { 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ∣ 𝑥 <s 𝐴 } ) |
11 |
10
|
eleq2d |
⊢ ( 𝐴 ∈ No → ( 𝑥 ∈ ( L ‘ 𝐴 ) ↔ 𝑥 ∈ { 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ∣ 𝑥 <s 𝐴 } ) ) |
12 |
|
rabid |
⊢ ( 𝑥 ∈ { 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ∣ 𝑥 <s 𝐴 } ↔ ( 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ∧ 𝑥 <s 𝐴 ) ) |
13 |
11 12
|
bitrdi |
⊢ ( 𝐴 ∈ No → ( 𝑥 ∈ ( L ‘ 𝐴 ) ↔ ( 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ∧ 𝑥 <s 𝐴 ) ) ) |
14 |
13
|
simplbda |
⊢ ( ( 𝐴 ∈ No ∧ 𝑥 ∈ ( L ‘ 𝐴 ) ) → 𝑥 <s 𝐴 ) |
15 |
|
breq2 |
⊢ ( 𝑦 = 𝐴 → ( 𝑥 <s 𝑦 ↔ 𝑥 <s 𝐴 ) ) |
16 |
14 15
|
syl5ibr |
⊢ ( 𝑦 = 𝐴 → ( ( 𝐴 ∈ No ∧ 𝑥 ∈ ( L ‘ 𝐴 ) ) → 𝑥 <s 𝑦 ) ) |
17 |
16
|
expd |
⊢ ( 𝑦 = 𝐴 → ( 𝐴 ∈ No → ( 𝑥 ∈ ( L ‘ 𝐴 ) → 𝑥 <s 𝑦 ) ) ) |
18 |
8 17
|
sylbi |
⊢ ( 𝑦 ∈ { 𝐴 } → ( 𝐴 ∈ No → ( 𝑥 ∈ ( L ‘ 𝐴 ) → 𝑥 <s 𝑦 ) ) ) |
19 |
18
|
3imp231 |
⊢ ( ( 𝐴 ∈ No ∧ 𝑥 ∈ ( L ‘ 𝐴 ) ∧ 𝑦 ∈ { 𝐴 } ) → 𝑥 <s 𝑦 ) |
20 |
1 3 6 7 19
|
ssltd |
⊢ ( 𝐴 ∈ No → ( L ‘ 𝐴 ) <<s { 𝐴 } ) |