| Step |
Hyp |
Ref |
Expression |
| 1 |
|
scutf |
⊢ |s : <<s ⟶ No |
| 2 |
|
lltropt |
⊢ ( 𝑥 ∈ No → ( L ‘ 𝑥 ) <<s ( R ‘ 𝑥 ) ) |
| 3 |
|
df-br |
⊢ ( ( L ‘ 𝑥 ) <<s ( R ‘ 𝑥 ) ↔ ⟨ ( L ‘ 𝑥 ) , ( R ‘ 𝑥 ) ⟩ ∈ <<s ) |
| 4 |
2 3
|
sylib |
⊢ ( 𝑥 ∈ No → ⟨ ( L ‘ 𝑥 ) , ( R ‘ 𝑥 ) ⟩ ∈ <<s ) |
| 5 |
|
lrcut |
⊢ ( 𝑥 ∈ No → ( ( L ‘ 𝑥 ) |s ( R ‘ 𝑥 ) ) = 𝑥 ) |
| 6 |
5
|
eqcomd |
⊢ ( 𝑥 ∈ No → 𝑥 = ( ( L ‘ 𝑥 ) |s ( R ‘ 𝑥 ) ) ) |
| 7 |
|
fveq2 |
⊢ ( 𝑦 = ⟨ ( L ‘ 𝑥 ) , ( R ‘ 𝑥 ) ⟩ → ( |s ‘ 𝑦 ) = ( |s ‘ ⟨ ( L ‘ 𝑥 ) , ( R ‘ 𝑥 ) ⟩ ) ) |
| 8 |
|
df-ov |
⊢ ( ( L ‘ 𝑥 ) |s ( R ‘ 𝑥 ) ) = ( |s ‘ ⟨ ( L ‘ 𝑥 ) , ( R ‘ 𝑥 ) ⟩ ) |
| 9 |
7 8
|
eqtr4di |
⊢ ( 𝑦 = ⟨ ( L ‘ 𝑥 ) , ( R ‘ 𝑥 ) ⟩ → ( |s ‘ 𝑦 ) = ( ( L ‘ 𝑥 ) |s ( R ‘ 𝑥 ) ) ) |
| 10 |
9
|
rspceeqv |
⊢ ( ( ⟨ ( L ‘ 𝑥 ) , ( R ‘ 𝑥 ) ⟩ ∈ <<s ∧ 𝑥 = ( ( L ‘ 𝑥 ) |s ( R ‘ 𝑥 ) ) ) → ∃ 𝑦 ∈ <<s 𝑥 = ( |s ‘ 𝑦 ) ) |
| 11 |
4 6 10
|
syl2anc |
⊢ ( 𝑥 ∈ No → ∃ 𝑦 ∈ <<s 𝑥 = ( |s ‘ 𝑦 ) ) |
| 12 |
11
|
rgen |
⊢ ∀ 𝑥 ∈ No ∃ 𝑦 ∈ <<s 𝑥 = ( |s ‘ 𝑦 ) |
| 13 |
|
dffo3 |
⊢ ( |s : <<s –onto→ No ↔ ( |s : <<s ⟶ No ∧ ∀ 𝑥 ∈ No ∃ 𝑦 ∈ <<s 𝑥 = ( |s ‘ 𝑦 ) ) ) |
| 14 |
1 12 13
|
mpbir2an |
⊢ |s : <<s –onto→ No |