Proof of Theorem cofcutrtime
| Step | Hyp | Ref
| Expression |
| 1 | | ssun1 4178 |
. . . . . . . 8
⊢ 𝐴 ⊆ (𝐴 ∪ 𝐵) |
| 2 | | sstr 3992 |
. . . . . . . 8
⊢ ((𝐴 ⊆ (𝐴 ∪ 𝐵) ∧ (𝐴 ∪ 𝐵) ⊆ ( O ‘(
bday ‘𝑋)))
→ 𝐴 ⊆ ( O
‘( bday ‘𝑋))) |
| 3 | 1, 2 | mpan 690 |
. . . . . . 7
⊢ ((𝐴 ∪ 𝐵) ⊆ ( O ‘(
bday ‘𝑋))
→ 𝐴 ⊆ ( O
‘( bday ‘𝑋))) |
| 4 | 3 | 3ad2ant1 1134 |
. . . . . 6
⊢ (((𝐴 ∪ 𝐵) ⊆ ( O ‘(
bday ‘𝑋))
∧ 𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → 𝐴 ⊆ ( O ‘(
bday ‘𝑋))) |
| 5 | 4 | sselda 3983 |
. . . . 5
⊢ ((((𝐴 ∪ 𝐵) ⊆ ( O ‘(
bday ‘𝑋))
∧ 𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ ( O ‘(
bday ‘𝑋))) |
| 6 | | simpl2 1193 |
. . . . . . . . 9
⊢ ((((𝐴 ∪ 𝐵) ⊆ ( O ‘(
bday ‘𝑋))
∧ 𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ 𝐴) → 𝐴 <<s 𝐵) |
| 7 | | scutcut 27846 |
. . . . . . . . 9
⊢ (𝐴 <<s 𝐵 → ((𝐴 |s 𝐵) ∈ No
∧ 𝐴 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐵)) |
| 8 | 6, 7 | syl 17 |
. . . . . . . 8
⊢ ((((𝐴 ∪ 𝐵) ⊆ ( O ‘(
bday ‘𝑋))
∧ 𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ 𝐴) → ((𝐴 |s 𝐵) ∈ No
∧ 𝐴 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐵)) |
| 9 | 8 | simp2d 1144 |
. . . . . . 7
⊢ ((((𝐴 ∪ 𝐵) ⊆ ( O ‘(
bday ‘𝑋))
∧ 𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ 𝐴) → 𝐴 <<s {(𝐴 |s 𝐵)}) |
| 10 | | simpr 484 |
. . . . . . 7
⊢ ((((𝐴 ∪ 𝐵) ⊆ ( O ‘(
bday ‘𝑋))
∧ 𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴) |
| 11 | | ovex 7464 |
. . . . . . . . 9
⊢ (𝐴 |s 𝐵) ∈ V |
| 12 | 11 | snid 4662 |
. . . . . . . 8
⊢ (𝐴 |s 𝐵) ∈ {(𝐴 |s 𝐵)} |
| 13 | 12 | a1i 11 |
. . . . . . 7
⊢ ((((𝐴 ∪ 𝐵) ⊆ ( O ‘(
bday ‘𝑋))
∧ 𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ 𝐴) → (𝐴 |s 𝐵) ∈ {(𝐴 |s 𝐵)}) |
| 14 | 9, 10, 13 | ssltsepcd 27839 |
. . . . . 6
⊢ ((((𝐴 ∪ 𝐵) ⊆ ( O ‘(
bday ‘𝑋))
∧ 𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ 𝐴) → 𝑥 <s (𝐴 |s 𝐵)) |
| 15 | | simpl3 1194 |
. . . . . 6
⊢ ((((𝐴 ∪ 𝐵) ⊆ ( O ‘(
bday ‘𝑋))
∧ 𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ 𝐴) → 𝑋 = (𝐴 |s 𝐵)) |
| 16 | 14, 15 | breqtrrd 5171 |
. . . . 5
⊢ ((((𝐴 ∪ 𝐵) ⊆ ( O ‘(
bday ‘𝑋))
∧ 𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ 𝐴) → 𝑥 <s 𝑋) |
| 17 | | leftval 27902 |
. . . . . . . 8
⊢ ( L
‘𝑋) = {𝑥 ∈ ( O ‘( bday ‘𝑋)) ∣ 𝑥 <s 𝑋} |
| 18 | 17 | a1i 11 |
. . . . . . 7
⊢ ((((𝐴 ∪ 𝐵) ⊆ ( O ‘(
bday ‘𝑋))
∧ 𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ 𝐴) → ( L ‘𝑋) = {𝑥 ∈ ( O ‘(
bday ‘𝑋))
∣ 𝑥 <s 𝑋}) |
| 19 | 18 | eleq2d 2827 |
. . . . . 6
⊢ ((((𝐴 ∪ 𝐵) ⊆ ( O ‘(
bday ‘𝑋))
∧ 𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ 𝐴) → (𝑥 ∈ ( L ‘𝑋) ↔ 𝑥 ∈ {𝑥 ∈ ( O ‘(
bday ‘𝑋))
∣ 𝑥 <s 𝑋})) |
| 20 | | rabid 3458 |
. . . . . 6
⊢ (𝑥 ∈ {𝑥 ∈ ( O ‘(
bday ‘𝑋))
∣ 𝑥 <s 𝑋} ↔ (𝑥 ∈ ( O ‘(
bday ‘𝑋))
∧ 𝑥 <s 𝑋)) |
| 21 | 19, 20 | bitrdi 287 |
. . . . 5
⊢ ((((𝐴 ∪ 𝐵) ⊆ ( O ‘(
bday ‘𝑋))
∧ 𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ 𝐴) → (𝑥 ∈ ( L ‘𝑋) ↔ (𝑥 ∈ ( O ‘(
bday ‘𝑋))
∧ 𝑥 <s 𝑋))) |
| 22 | 5, 16, 21 | mpbir2and 713 |
. . . 4
⊢ ((((𝐴 ∪ 𝐵) ⊆ ( O ‘(
bday ‘𝑋))
∧ 𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ ( L ‘𝑋)) |
| 23 | | leftssno 27919 |
. . . . . 6
⊢ ( L
‘𝑋) ⊆ No |
| 24 | 23, 22 | sselid 3981 |
. . . . 5
⊢ ((((𝐴 ∪ 𝐵) ⊆ ( O ‘(
bday ‘𝑋))
∧ 𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ No
) |
| 25 | | slerflex 27808 |
. . . . 5
⊢ (𝑥 ∈
No → 𝑥 ≤s
𝑥) |
| 26 | 24, 25 | syl 17 |
. . . 4
⊢ ((((𝐴 ∪ 𝐵) ⊆ ( O ‘(
bday ‘𝑋))
∧ 𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ 𝐴) → 𝑥 ≤s 𝑥) |
| 27 | | breq2 5147 |
. . . . 5
⊢ (𝑦 = 𝑥 → (𝑥 ≤s 𝑦 ↔ 𝑥 ≤s 𝑥)) |
| 28 | 27 | rspcev 3622 |
. . . 4
⊢ ((𝑥 ∈ ( L ‘𝑋) ∧ 𝑥 ≤s 𝑥) → ∃𝑦 ∈ ( L ‘𝑋)𝑥 ≤s 𝑦) |
| 29 | 22, 26, 28 | syl2anc 584 |
. . 3
⊢ ((((𝐴 ∪ 𝐵) ⊆ ( O ‘(
bday ‘𝑋))
∧ 𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ 𝐴) → ∃𝑦 ∈ ( L ‘𝑋)𝑥 ≤s 𝑦) |
| 30 | 29 | ralrimiva 3146 |
. 2
⊢ (((𝐴 ∪ 𝐵) ⊆ ( O ‘(
bday ‘𝑋))
∧ 𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ ( L ‘𝑋)𝑥 ≤s 𝑦) |
| 31 | | ssun2 4179 |
. . . . . . . 8
⊢ 𝐵 ⊆ (𝐴 ∪ 𝐵) |
| 32 | | sstr 3992 |
. . . . . . . 8
⊢ ((𝐵 ⊆ (𝐴 ∪ 𝐵) ∧ (𝐴 ∪ 𝐵) ⊆ ( O ‘(
bday ‘𝑋)))
→ 𝐵 ⊆ ( O
‘( bday ‘𝑋))) |
| 33 | 31, 32 | mpan 690 |
. . . . . . 7
⊢ ((𝐴 ∪ 𝐵) ⊆ ( O ‘(
bday ‘𝑋))
→ 𝐵 ⊆ ( O
‘( bday ‘𝑋))) |
| 34 | 33 | 3ad2ant1 1134 |
. . . . . 6
⊢ (((𝐴 ∪ 𝐵) ⊆ ( O ‘(
bday ‘𝑋))
∧ 𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → 𝐵 ⊆ ( O ‘(
bday ‘𝑋))) |
| 35 | 34 | sselda 3983 |
. . . . 5
⊢ ((((𝐴 ∪ 𝐵) ⊆ ( O ‘(
bday ‘𝑋))
∧ 𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ 𝐵) → 𝑧 ∈ ( O ‘(
bday ‘𝑋))) |
| 36 | | simpl3 1194 |
. . . . . 6
⊢ ((((𝐴 ∪ 𝐵) ⊆ ( O ‘(
bday ‘𝑋))
∧ 𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ 𝐵) → 𝑋 = (𝐴 |s 𝐵)) |
| 37 | | simpl2 1193 |
. . . . . . . . 9
⊢ ((((𝐴 ∪ 𝐵) ⊆ ( O ‘(
bday ‘𝑋))
∧ 𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ 𝐵) → 𝐴 <<s 𝐵) |
| 38 | 37, 7 | syl 17 |
. . . . . . . 8
⊢ ((((𝐴 ∪ 𝐵) ⊆ ( O ‘(
bday ‘𝑋))
∧ 𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ 𝐵) → ((𝐴 |s 𝐵) ∈ No
∧ 𝐴 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐵)) |
| 39 | 38 | simp3d 1145 |
. . . . . . 7
⊢ ((((𝐴 ∪ 𝐵) ⊆ ( O ‘(
bday ‘𝑋))
∧ 𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ 𝐵) → {(𝐴 |s 𝐵)} <<s 𝐵) |
| 40 | 12 | a1i 11 |
. . . . . . 7
⊢ ((((𝐴 ∪ 𝐵) ⊆ ( O ‘(
bday ‘𝑋))
∧ 𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ 𝐵) → (𝐴 |s 𝐵) ∈ {(𝐴 |s 𝐵)}) |
| 41 | | simpr 484 |
. . . . . . 7
⊢ ((((𝐴 ∪ 𝐵) ⊆ ( O ‘(
bday ‘𝑋))
∧ 𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ 𝐵) → 𝑧 ∈ 𝐵) |
| 42 | 39, 40, 41 | ssltsepcd 27839 |
. . . . . 6
⊢ ((((𝐴 ∪ 𝐵) ⊆ ( O ‘(
bday ‘𝑋))
∧ 𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ 𝐵) → (𝐴 |s 𝐵) <s 𝑧) |
| 43 | 36, 42 | eqbrtrd 5165 |
. . . . 5
⊢ ((((𝐴 ∪ 𝐵) ⊆ ( O ‘(
bday ‘𝑋))
∧ 𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ 𝐵) → 𝑋 <s 𝑧) |
| 44 | | rightval 27903 |
. . . . . . . 8
⊢ ( R
‘𝑋) = {𝑧 ∈ ( O ‘( bday ‘𝑋)) ∣ 𝑋 <s 𝑧} |
| 45 | 44 | a1i 11 |
. . . . . . 7
⊢ ((((𝐴 ∪ 𝐵) ⊆ ( O ‘(
bday ‘𝑋))
∧ 𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ 𝐵) → ( R ‘𝑋) = {𝑧 ∈ ( O ‘(
bday ‘𝑋))
∣ 𝑋 <s 𝑧}) |
| 46 | 45 | eleq2d 2827 |
. . . . . 6
⊢ ((((𝐴 ∪ 𝐵) ⊆ ( O ‘(
bday ‘𝑋))
∧ 𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ 𝐵) → (𝑧 ∈ ( R ‘𝑋) ↔ 𝑧 ∈ {𝑧 ∈ ( O ‘(
bday ‘𝑋))
∣ 𝑋 <s 𝑧})) |
| 47 | | rabid 3458 |
. . . . . 6
⊢ (𝑧 ∈ {𝑧 ∈ ( O ‘(
bday ‘𝑋))
∣ 𝑋 <s 𝑧} ↔ (𝑧 ∈ ( O ‘(
bday ‘𝑋))
∧ 𝑋 <s 𝑧)) |
| 48 | 46, 47 | bitrdi 287 |
. . . . 5
⊢ ((((𝐴 ∪ 𝐵) ⊆ ( O ‘(
bday ‘𝑋))
∧ 𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ 𝐵) → (𝑧 ∈ ( R ‘𝑋) ↔ (𝑧 ∈ ( O ‘(
bday ‘𝑋))
∧ 𝑋 <s 𝑧))) |
| 49 | 35, 43, 48 | mpbir2and 713 |
. . . 4
⊢ ((((𝐴 ∪ 𝐵) ⊆ ( O ‘(
bday ‘𝑋))
∧ 𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ 𝐵) → 𝑧 ∈ ( R ‘𝑋)) |
| 50 | | rightssno 27920 |
. . . . . 6
⊢ ( R
‘𝑋) ⊆ No |
| 51 | 50, 49 | sselid 3981 |
. . . . 5
⊢ ((((𝐴 ∪ 𝐵) ⊆ ( O ‘(
bday ‘𝑋))
∧ 𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ 𝐵) → 𝑧 ∈ No
) |
| 52 | | slerflex 27808 |
. . . . 5
⊢ (𝑧 ∈
No → 𝑧 ≤s
𝑧) |
| 53 | 51, 52 | syl 17 |
. . . 4
⊢ ((((𝐴 ∪ 𝐵) ⊆ ( O ‘(
bday ‘𝑋))
∧ 𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ 𝐵) → 𝑧 ≤s 𝑧) |
| 54 | | breq1 5146 |
. . . . 5
⊢ (𝑤 = 𝑧 → (𝑤 ≤s 𝑧 ↔ 𝑧 ≤s 𝑧)) |
| 55 | 54 | rspcev 3622 |
. . . 4
⊢ ((𝑧 ∈ ( R ‘𝑋) ∧ 𝑧 ≤s 𝑧) → ∃𝑤 ∈ ( R ‘𝑋)𝑤 ≤s 𝑧) |
| 56 | 49, 53, 55 | syl2anc 584 |
. . 3
⊢ ((((𝐴 ∪ 𝐵) ⊆ ( O ‘(
bday ‘𝑋))
∧ 𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ 𝐵) → ∃𝑤 ∈ ( R ‘𝑋)𝑤 ≤s 𝑧) |
| 57 | 56 | ralrimiva 3146 |
. 2
⊢ (((𝐴 ∪ 𝐵) ⊆ ( O ‘(
bday ‘𝑋))
∧ 𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ ( R ‘𝑋)𝑤 ≤s 𝑧) |
| 58 | 30, 57 | jca 511 |
1
⊢ (((𝐴 ∪ 𝐵) ⊆ ( O ‘(
bday ‘𝑋))
∧ 𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ ( L ‘𝑋)𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ ( R ‘𝑋)𝑤 ≤s 𝑧)) |