Step | Hyp | Ref
| Expression |
1 | | ssltex1 31901 |
. . . 4
⊢ (𝐴 <<s 𝐵 → 𝐴 ∈ V) |
2 | 1 | adantr 481 |
. . 3
⊢ ((𝐴 <<s 𝐵 ∧ 𝐶 ⊆ 𝐵) → 𝐴 ∈ V) |
3 | | ssltex2 31902 |
. . . . 5
⊢ (𝐴 <<s 𝐵 → 𝐵 ∈ V) |
4 | 3 | adantr 481 |
. . . 4
⊢ ((𝐴 <<s 𝐵 ∧ 𝐶 ⊆ 𝐵) → 𝐵 ∈ V) |
5 | | simpr 477 |
. . . 4
⊢ ((𝐴 <<s 𝐵 ∧ 𝐶 ⊆ 𝐵) → 𝐶 ⊆ 𝐵) |
6 | 4, 5 | ssexd 4805 |
. . 3
⊢ ((𝐴 <<s 𝐵 ∧ 𝐶 ⊆ 𝐵) → 𝐶 ∈ V) |
7 | 2, 6 | jca 554 |
. 2
⊢ ((𝐴 <<s 𝐵 ∧ 𝐶 ⊆ 𝐵) → (𝐴 ∈ V ∧ 𝐶 ∈ V)) |
8 | | ssltss1 31903 |
. . . 4
⊢ (𝐴 <<s 𝐵 → 𝐴 ⊆ No
) |
9 | 8 | adantr 481 |
. . 3
⊢ ((𝐴 <<s 𝐵 ∧ 𝐶 ⊆ 𝐵) → 𝐴 ⊆ No
) |
10 | | ssltss2 31904 |
. . . . 5
⊢ (𝐴 <<s 𝐵 → 𝐵 ⊆ No
) |
11 | 10 | adantr 481 |
. . . 4
⊢ ((𝐴 <<s 𝐵 ∧ 𝐶 ⊆ 𝐵) → 𝐵 ⊆ No
) |
12 | 5, 11 | sstrd 3613 |
. . 3
⊢ ((𝐴 <<s 𝐵 ∧ 𝐶 ⊆ 𝐵) → 𝐶 ⊆ No
) |
13 | | ssltsep 31905 |
. . . . 5
⊢ (𝐴 <<s 𝐵 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 <s 𝑦) |
14 | 13 | adantr 481 |
. . . 4
⊢ ((𝐴 <<s 𝐵 ∧ 𝐶 ⊆ 𝐵) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 <s 𝑦) |
15 | | ssralv 3666 |
. . . . . 6
⊢ (𝐶 ⊆ 𝐵 → (∀𝑦 ∈ 𝐵 𝑥 <s 𝑦 → ∀𝑦 ∈ 𝐶 𝑥 <s 𝑦)) |
16 | 5, 15 | syl 17 |
. . . . 5
⊢ ((𝐴 <<s 𝐵 ∧ 𝐶 ⊆ 𝐵) → (∀𝑦 ∈ 𝐵 𝑥 <s 𝑦 → ∀𝑦 ∈ 𝐶 𝑥 <s 𝑦)) |
17 | 16 | ralimdv 2963 |
. . . 4
⊢ ((𝐴 <<s 𝐵 ∧ 𝐶 ⊆ 𝐵) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 <s 𝑦 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐶 𝑥 <s 𝑦)) |
18 | 14, 17 | mpd 15 |
. . 3
⊢ ((𝐴 <<s 𝐵 ∧ 𝐶 ⊆ 𝐵) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐶 𝑥 <s 𝑦) |
19 | 9, 12, 18 | 3jca 1242 |
. 2
⊢ ((𝐴 <<s 𝐵 ∧ 𝐶 ⊆ 𝐵) → (𝐴 ⊆ No
∧ 𝐶 ⊆ No ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐶 𝑥 <s 𝑦)) |
20 | | brsslt 31900 |
. 2
⊢ (𝐴 <<s 𝐶 ↔ ((𝐴 ∈ V ∧ 𝐶 ∈ V) ∧ (𝐴 ⊆ No
∧ 𝐶 ⊆ No ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐶 𝑥 <s 𝑦))) |
21 | 7, 19, 20 | sylanbrc 698 |
1
⊢ ((𝐴 <<s 𝐵 ∧ 𝐶 ⊆ 𝐵) → 𝐴 <<s 𝐶) |