Proof of Theorem slelss
| Step | Hyp | Ref
| Expression |
| 1 | | sltlpss 27945 |
. . 3
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ ( bday
‘𝐴) = ( bday ‘𝐵)) → (𝐴 <s 𝐵 ↔ ( L ‘𝐴) ⊊ ( L ‘𝐵))) |
| 2 | | fveq2 6906 |
. . . 4
⊢ (𝐴 = 𝐵 → ( L ‘𝐴) = ( L ‘𝐵)) |
| 3 | | simpr 484 |
. . . . . . 7
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ ( bday
‘𝐴) = ( bday ‘𝐵)) ∧ ( L ‘𝐴) = ( L ‘𝐵)) → ( L ‘𝐴) = ( L ‘𝐵)) |
| 4 | | lruneq 27944 |
. . . . . . . . . 10
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ ( bday
‘𝐴) = ( bday ‘𝐵)) → (( L ‘𝐴) ∪ ( R ‘𝐴)) = (( L ‘𝐵) ∪ ( R ‘𝐵))) |
| 5 | 4 | adantr 480 |
. . . . . . . . 9
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ ( bday
‘𝐴) = ( bday ‘𝐵)) ∧ ( L ‘𝐴) = ( L ‘𝐵)) → (( L ‘𝐴) ∪ ( R ‘𝐴)) = (( L ‘𝐵) ∪ ( R ‘𝐵))) |
| 6 | 5, 3 | difeq12d 4127 |
. . . . . . . 8
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ ( bday
‘𝐴) = ( bday ‘𝐵)) ∧ ( L ‘𝐴) = ( L ‘𝐵)) → ((( L ‘𝐴) ∪ ( R ‘𝐴)) ∖ ( L ‘𝐴)) = ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∖ ( L ‘𝐵))) |
| 7 | | difundir 4291 |
. . . . . . . . . 10
⊢ ((( L
‘𝐴) ∪ ( R
‘𝐴)) ∖ ( L
‘𝐴)) = ((( L
‘𝐴) ∖ ( L
‘𝐴)) ∪ (( R
‘𝐴) ∖ ( L
‘𝐴))) |
| 8 | | difid 4376 |
. . . . . . . . . . 11
⊢ (( L
‘𝐴) ∖ ( L
‘𝐴)) =
∅ |
| 9 | 8 | uneq1i 4164 |
. . . . . . . . . 10
⊢ ((( L
‘𝐴) ∖ ( L
‘𝐴)) ∪ (( R
‘𝐴) ∖ ( L
‘𝐴))) = (∅
∪ (( R ‘𝐴)
∖ ( L ‘𝐴))) |
| 10 | | 0un 4396 |
. . . . . . . . . 10
⊢ (∅
∪ (( R ‘𝐴)
∖ ( L ‘𝐴))) =
(( R ‘𝐴) ∖ ( L
‘𝐴)) |
| 11 | 7, 9, 10 | 3eqtri 2769 |
. . . . . . . . 9
⊢ ((( L
‘𝐴) ∪ ( R
‘𝐴)) ∖ ( L
‘𝐴)) = (( R
‘𝐴) ∖ ( L
‘𝐴)) |
| 12 | | incom 4209 |
. . . . . . . . . . 11
⊢ (( L
‘𝐴) ∩ ( R
‘𝐴)) = (( R
‘𝐴) ∩ ( L
‘𝐴)) |
| 13 | | lltropt 27911 |
. . . . . . . . . . . 12
⊢ ( L
‘𝐴) <<s ( R
‘𝐴) |
| 14 | | ssltdisj 27866 |
. . . . . . . . . . . 12
⊢ (( L
‘𝐴) <<s ( R
‘𝐴) → (( L
‘𝐴) ∩ ( R
‘𝐴)) =
∅) |
| 15 | 13, 14 | mp1i 13 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ ( bday
‘𝐴) = ( bday ‘𝐵)) ∧ ( L ‘𝐴) = ( L ‘𝐵)) → (( L ‘𝐴) ∩ ( R ‘𝐴)) = ∅) |
| 16 | 12, 15 | eqtr3id 2791 |
. . . . . . . . . 10
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ ( bday
‘𝐴) = ( bday ‘𝐵)) ∧ ( L ‘𝐴) = ( L ‘𝐵)) → (( R ‘𝐴) ∩ ( L ‘𝐴)) = ∅) |
| 17 | | disjdif2 4480 |
. . . . . . . . . 10
⊢ ((( R
‘𝐴) ∩ ( L
‘𝐴)) = ∅ →
(( R ‘𝐴) ∖ ( L
‘𝐴)) = ( R
‘𝐴)) |
| 18 | 16, 17 | syl 17 |
. . . . . . . . 9
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ ( bday
‘𝐴) = ( bday ‘𝐵)) ∧ ( L ‘𝐴) = ( L ‘𝐵)) → (( R ‘𝐴) ∖ ( L ‘𝐴)) = ( R ‘𝐴)) |
| 19 | 11, 18 | eqtrid 2789 |
. . . . . . . 8
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ ( bday
‘𝐴) = ( bday ‘𝐵)) ∧ ( L ‘𝐴) = ( L ‘𝐵)) → ((( L ‘𝐴) ∪ ( R ‘𝐴)) ∖ ( L ‘𝐴)) = ( R ‘𝐴)) |
| 20 | | difundir 4291 |
. . . . . . . . . 10
⊢ ((( L
‘𝐵) ∪ ( R
‘𝐵)) ∖ ( L
‘𝐵)) = ((( L
‘𝐵) ∖ ( L
‘𝐵)) ∪ (( R
‘𝐵) ∖ ( L
‘𝐵))) |
| 21 | | difid 4376 |
. . . . . . . . . . 11
⊢ (( L
‘𝐵) ∖ ( L
‘𝐵)) =
∅ |
| 22 | 21 | uneq1i 4164 |
. . . . . . . . . 10
⊢ ((( L
‘𝐵) ∖ ( L
‘𝐵)) ∪ (( R
‘𝐵) ∖ ( L
‘𝐵))) = (∅
∪ (( R ‘𝐵)
∖ ( L ‘𝐵))) |
| 23 | | 0un 4396 |
. . . . . . . . . 10
⊢ (∅
∪ (( R ‘𝐵)
∖ ( L ‘𝐵))) =
(( R ‘𝐵) ∖ ( L
‘𝐵)) |
| 24 | 20, 22, 23 | 3eqtri 2769 |
. . . . . . . . 9
⊢ ((( L
‘𝐵) ∪ ( R
‘𝐵)) ∖ ( L
‘𝐵)) = (( R
‘𝐵) ∖ ( L
‘𝐵)) |
| 25 | | incom 4209 |
. . . . . . . . . . 11
⊢ (( L
‘𝐵) ∩ ( R
‘𝐵)) = (( R
‘𝐵) ∩ ( L
‘𝐵)) |
| 26 | | lltropt 27911 |
. . . . . . . . . . . 12
⊢ ( L
‘𝐵) <<s ( R
‘𝐵) |
| 27 | | ssltdisj 27866 |
. . . . . . . . . . . 12
⊢ (( L
‘𝐵) <<s ( R
‘𝐵) → (( L
‘𝐵) ∩ ( R
‘𝐵)) =
∅) |
| 28 | 26, 27 | mp1i 13 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ ( bday
‘𝐴) = ( bday ‘𝐵)) ∧ ( L ‘𝐴) = ( L ‘𝐵)) → (( L ‘𝐵) ∩ ( R ‘𝐵)) = ∅) |
| 29 | 25, 28 | eqtr3id 2791 |
. . . . . . . . . 10
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ ( bday
‘𝐴) = ( bday ‘𝐵)) ∧ ( L ‘𝐴) = ( L ‘𝐵)) → (( R ‘𝐵) ∩ ( L ‘𝐵)) = ∅) |
| 30 | | disjdif2 4480 |
. . . . . . . . . 10
⊢ ((( R
‘𝐵) ∩ ( L
‘𝐵)) = ∅ →
(( R ‘𝐵) ∖ ( L
‘𝐵)) = ( R
‘𝐵)) |
| 31 | 29, 30 | syl 17 |
. . . . . . . . 9
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ ( bday
‘𝐴) = ( bday ‘𝐵)) ∧ ( L ‘𝐴) = ( L ‘𝐵)) → (( R ‘𝐵) ∖ ( L ‘𝐵)) = ( R ‘𝐵)) |
| 32 | 24, 31 | eqtrid 2789 |
. . . . . . . 8
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ ( bday
‘𝐴) = ( bday ‘𝐵)) ∧ ( L ‘𝐴) = ( L ‘𝐵)) → ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∖ ( L ‘𝐵)) = ( R ‘𝐵)) |
| 33 | 6, 19, 32 | 3eqtr3d 2785 |
. . . . . . 7
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ ( bday
‘𝐴) = ( bday ‘𝐵)) ∧ ( L ‘𝐴) = ( L ‘𝐵)) → ( R ‘𝐴) = ( R ‘𝐵)) |
| 34 | 3, 33 | oveq12d 7449 |
. . . . . 6
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ ( bday
‘𝐴) = ( bday ‘𝐵)) ∧ ( L ‘𝐴) = ( L ‘𝐵)) → (( L ‘𝐴) |s ( R ‘𝐴)) = (( L ‘𝐵) |s ( R ‘𝐵))) |
| 35 | | simpl1 1192 |
. . . . . . 7
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ ( bday
‘𝐴) = ( bday ‘𝐵)) ∧ ( L ‘𝐴) = ( L ‘𝐵)) → 𝐴 ∈ No
) |
| 36 | | lrcut 27941 |
. . . . . . 7
⊢ (𝐴 ∈
No → (( L ‘𝐴) |s ( R ‘𝐴)) = 𝐴) |
| 37 | 35, 36 | syl 17 |
. . . . . 6
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ ( bday
‘𝐴) = ( bday ‘𝐵)) ∧ ( L ‘𝐴) = ( L ‘𝐵)) → (( L ‘𝐴) |s ( R ‘𝐴)) = 𝐴) |
| 38 | | simpl2 1193 |
. . . . . . 7
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ ( bday
‘𝐴) = ( bday ‘𝐵)) ∧ ( L ‘𝐴) = ( L ‘𝐵)) → 𝐵 ∈ No
) |
| 39 | | lrcut 27941 |
. . . . . . 7
⊢ (𝐵 ∈
No → (( L ‘𝐵) |s ( R ‘𝐵)) = 𝐵) |
| 40 | 38, 39 | syl 17 |
. . . . . 6
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ ( bday
‘𝐴) = ( bday ‘𝐵)) ∧ ( L ‘𝐴) = ( L ‘𝐵)) → (( L ‘𝐵) |s ( R ‘𝐵)) = 𝐵) |
| 41 | 34, 37, 40 | 3eqtr3d 2785 |
. . . . 5
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ ( bday
‘𝐴) = ( bday ‘𝐵)) ∧ ( L ‘𝐴) = ( L ‘𝐵)) → 𝐴 = 𝐵) |
| 42 | 41 | ex 412 |
. . . 4
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ ( bday
‘𝐴) = ( bday ‘𝐵)) → (( L ‘𝐴) = ( L ‘𝐵) → 𝐴 = 𝐵)) |
| 43 | 2, 42 | impbid2 226 |
. . 3
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ ( bday
‘𝐴) = ( bday ‘𝐵)) → (𝐴 = 𝐵 ↔ ( L ‘𝐴) = ( L ‘𝐵))) |
| 44 | 1, 43 | orbi12d 919 |
. 2
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ ( bday
‘𝐴) = ( bday ‘𝐵)) → ((𝐴 <s 𝐵 ∨ 𝐴 = 𝐵) ↔ (( L ‘𝐴) ⊊ ( L ‘𝐵) ∨ ( L ‘𝐴) = ( L ‘𝐵)))) |
| 45 | | sleloe 27799 |
. . 3
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (𝐴 ≤s 𝐵 ↔ (𝐴 <s 𝐵 ∨ 𝐴 = 𝐵))) |
| 46 | 45 | 3adant3 1133 |
. 2
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ ( bday
‘𝐴) = ( bday ‘𝐵)) → (𝐴 ≤s 𝐵 ↔ (𝐴 <s 𝐵 ∨ 𝐴 = 𝐵))) |
| 47 | | sspss 4102 |
. . 3
⊢ (( L
‘𝐴) ⊆ ( L
‘𝐵) ↔ (( L
‘𝐴) ⊊ ( L
‘𝐵) ∨ ( L
‘𝐴) = ( L
‘𝐵))) |
| 48 | 47 | a1i 11 |
. 2
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ ( bday
‘𝐴) = ( bday ‘𝐵)) → (( L ‘𝐴) ⊆ ( L ‘𝐵) ↔ (( L ‘𝐴) ⊊ ( L ‘𝐵) ∨ ( L ‘𝐴) = ( L ‘𝐵)))) |
| 49 | 44, 46, 48 | 3bitr4d 311 |
1
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ ( bday
‘𝐴) = ( bday ‘𝐵)) → (𝐴 ≤s 𝐵 ↔ ( L ‘𝐴) ⊆ ( L ‘𝐵))) |