| Step | Hyp | Ref
| Expression |
|---|
| 1 | | n0 4349 |
. . 3
⊢ (𝐵 ≠ ∅ ↔
∃𝑦 𝑦 ∈ 𝐵) |
| 2 | | ssltex1 27816 |
. . . . . . 7
⊢ (𝐴 <<s 𝐵 → 𝐴 ∈ V) |
| 3 | 2 | 3ad2ant2 1131 |
. . . . . 6
⊢ ((𝑦 ∈ 𝐵 ∧ 𝐴 <<s 𝐵 ∧ 𝐵 <<s 𝐶) → 𝐴 ∈ V) |
| 4 | | ssltex2 27817 |
. . . . . . 7
⊢ (𝐵 <<s 𝐶 → 𝐶 ∈ V) |
| 5 | 4 | 3ad2ant3 1132 |
. . . . . 6
⊢ ((𝑦 ∈ 𝐵 ∧ 𝐴 <<s 𝐵 ∧ 𝐵 <<s 𝐶) → 𝐶 ∈ V) |
| 6 | | ssltss1 27818 |
. . . . . . 7
⊢ (𝐴 <<s 𝐵 → 𝐴 ⊆ No
) |
| 7 | 6 | 3ad2ant2 1131 |
. . . . . 6
⊢ ((𝑦 ∈ 𝐵 ∧ 𝐴 <<s 𝐵 ∧ 𝐵 <<s 𝐶) → 𝐴 ⊆ No
) |
| 8 | | ssltss2 27819 |
. . . . . . 7
⊢ (𝐵 <<s 𝐶 → 𝐶 ⊆ No
) |
| 9 | 8 | 3ad2ant3 1132 |
. . . . . 6
⊢ ((𝑦 ∈ 𝐵 ∧ 𝐴 <<s 𝐵 ∧ 𝐵 <<s 𝐶) → 𝐶 ⊆ No
) |
| 10 | 7 | 3ad2ant1 1130 |
. . . . . . . 8
⊢ (((𝑦 ∈ 𝐵 ∧ 𝐴 <<s 𝐵 ∧ 𝐵 <<s 𝐶) ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶) → 𝐴 ⊆ No
) |
| 11 | | simp2 1134 |
. . . . . . . 8
⊢ (((𝑦 ∈ 𝐵 ∧ 𝐴 <<s 𝐵 ∧ 𝐵 <<s 𝐶) ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶) → 𝑥 ∈ 𝐴) |
| 12 | 10, 11 | sseldd 3980 |
. . . . . . 7
⊢ (((𝑦 ∈ 𝐵 ∧ 𝐴 <<s 𝐵 ∧ 𝐵 <<s 𝐶) ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶) → 𝑥 ∈ No
) |
| 13 | | ssltss2 27819 |
. . . . . . . . . 10
⊢ (𝐴 <<s 𝐵 → 𝐵 ⊆ No
) |
| 14 | 13 | 3ad2ant2 1131 |
. . . . . . . . 9
⊢ ((𝑦 ∈ 𝐵 ∧ 𝐴 <<s 𝐵 ∧ 𝐵 <<s 𝐶) → 𝐵 ⊆ No
) |
| 15 | 14 | 3ad2ant1 1130 |
. . . . . . . 8
⊢ (((𝑦 ∈ 𝐵 ∧ 𝐴 <<s 𝐵 ∧ 𝐵 <<s 𝐶) ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶) → 𝐵 ⊆ No
) |
| 16 | | simp11 1200 |
. . . . . . . 8
⊢ (((𝑦 ∈ 𝐵 ∧ 𝐴 <<s 𝐵 ∧ 𝐵 <<s 𝐶) ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶) → 𝑦 ∈ 𝐵) |
| 17 | 15, 16 | sseldd 3980 |
. . . . . . 7
⊢ (((𝑦 ∈ 𝐵 ∧ 𝐴 <<s 𝐵 ∧ 𝐵 <<s 𝐶) ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶) → 𝑦 ∈ No
) |
| 18 | 9 | 3ad2ant1 1130 |
. . . . . . . 8
⊢ (((𝑦 ∈ 𝐵 ∧ 𝐴 <<s 𝐵 ∧ 𝐵 <<s 𝐶) ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶) → 𝐶 ⊆ No
) |
| 19 | | simp3 1135 |
. . . . . . . 8
⊢ (((𝑦 ∈ 𝐵 ∧ 𝐴 <<s 𝐵 ∧ 𝐵 <<s 𝐶) ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶) → 𝑧 ∈ 𝐶) |
| 20 | 18, 19 | sseldd 3980 |
. . . . . . 7
⊢ (((𝑦 ∈ 𝐵 ∧ 𝐴 <<s 𝐵 ∧ 𝐵 <<s 𝐶) ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶) → 𝑧 ∈ No
) |
| 21 | | simp12 1201 |
. . . . . . . 8
⊢ (((𝑦 ∈ 𝐵 ∧ 𝐴 <<s 𝐵 ∧ 𝐵 <<s 𝐶) ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶) → 𝐴 <<s 𝐵) |
| 22 | 21, 11, 16 | ssltsepcd 27824 |
. . . . . . 7
⊢ (((𝑦 ∈ 𝐵 ∧ 𝐴 <<s 𝐵 ∧ 𝐵 <<s 𝐶) ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶) → 𝑥 <s 𝑦) |
| 23 | | simp13 1202 |
. . . . . . . 8
⊢ (((𝑦 ∈ 𝐵 ∧ 𝐴 <<s 𝐵 ∧ 𝐵 <<s 𝐶) ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶) → 𝐵 <<s 𝐶) |
| 24 | 23, 16, 19 | ssltsepcd 27824 |
. . . . . . 7
⊢ (((𝑦 ∈ 𝐵 ∧ 𝐴 <<s 𝐵 ∧ 𝐵 <<s 𝐶) ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶) → 𝑦 <s 𝑧) |
| 25 | 12, 17, 20, 22, 24 | slttrd 27789 |
. . . . . 6
⊢ (((𝑦 ∈ 𝐵 ∧ 𝐴 <<s 𝐵 ∧ 𝐵 <<s 𝐶) ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶) → 𝑥 <s 𝑧) |
| 26 | 3, 5, 7, 9, 25 | ssltd 27821 |
. . . . 5
⊢ ((𝑦 ∈ 𝐵 ∧ 𝐴 <<s 𝐵 ∧ 𝐵 <<s 𝐶) → 𝐴 <<s 𝐶) |
| 27 | 26 | 3exp 1116 |
. . . 4
⊢ (𝑦 ∈ 𝐵 → (𝐴 <<s 𝐵 → (𝐵 <<s 𝐶 → 𝐴 <<s 𝐶))) |
| 28 | 27 | exlimiv 1926 |
. . 3
⊢
(∃𝑦 𝑦 ∈ 𝐵 → (𝐴 <<s 𝐵 → (𝐵 <<s 𝐶 → 𝐴 <<s 𝐶))) |
| 29 | 1, 28 | sylbi 216 |
. 2
⊢ (𝐵 ≠ ∅ → (𝐴 <<s 𝐵 → (𝐵 <<s 𝐶 → 𝐴 <<s 𝐶))) |
| 30 | 29 | 3imp231 1110 |
1
⊢ ((𝐴 <<s 𝐵 ∧ 𝐵 <<s 𝐶 ∧ 𝐵 ≠ ∅) → 𝐴 <<s 𝐶) |
