Step | Hyp | Ref
| Expression |
1 | | ssltex1 33981 |
. . 3
⊢ (𝐴 <<s 𝐵 → 𝐴 ∈ V) |
2 | 1 | adantr 481 |
. 2
⊢ ((𝐴 <<s 𝐵 ∧ 𝐴 <<s 𝐶) → 𝐴 ∈ V) |
3 | | ssltex2 33982 |
. . . 4
⊢ (𝐴 <<s 𝐵 → 𝐵 ∈ V) |
4 | 3 | adantr 481 |
. . 3
⊢ ((𝐴 <<s 𝐵 ∧ 𝐴 <<s 𝐶) → 𝐵 ∈ V) |
5 | | ssltex2 33982 |
. . . 4
⊢ (𝐴 <<s 𝐶 → 𝐶 ∈ V) |
6 | 5 | adantl 482 |
. . 3
⊢ ((𝐴 <<s 𝐵 ∧ 𝐴 <<s 𝐶) → 𝐶 ∈ V) |
7 | 4, 6 | unexd 7604 |
. 2
⊢ ((𝐴 <<s 𝐵 ∧ 𝐴 <<s 𝐶) → (𝐵 ∪ 𝐶) ∈ V) |
8 | | ssltss1 33983 |
. . 3
⊢ (𝐴 <<s 𝐵 → 𝐴 ⊆ No
) |
9 | 8 | adantr 481 |
. 2
⊢ ((𝐴 <<s 𝐵 ∧ 𝐴 <<s 𝐶) → 𝐴 ⊆ No
) |
10 | | ssltss2 33984 |
. . . 4
⊢ (𝐴 <<s 𝐵 → 𝐵 ⊆ No
) |
11 | 10 | adantr 481 |
. . 3
⊢ ((𝐴 <<s 𝐵 ∧ 𝐴 <<s 𝐶) → 𝐵 ⊆ No
) |
12 | | ssltss2 33984 |
. . . 4
⊢ (𝐴 <<s 𝐶 → 𝐶 ⊆ No
) |
13 | 12 | adantl 482 |
. . 3
⊢ ((𝐴 <<s 𝐵 ∧ 𝐴 <<s 𝐶) → 𝐶 ⊆ No
) |
14 | 11, 13 | unssd 4120 |
. 2
⊢ ((𝐴 <<s 𝐵 ∧ 𝐴 <<s 𝐶) → (𝐵 ∪ 𝐶) ⊆ No
) |
15 | | elun 4083 |
. . . 4
⊢ (𝑦 ∈ (𝐵 ∪ 𝐶) ↔ (𝑦 ∈ 𝐵 ∨ 𝑦 ∈ 𝐶)) |
16 | | ssltsepc 33987 |
. . . . . . . 8
⊢ ((𝐴 <<s 𝐵 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝑥 <s 𝑦) |
17 | 16 | 3exp 1118 |
. . . . . . 7
⊢ (𝐴 <<s 𝐵 → (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐵 → 𝑥 <s 𝑦))) |
18 | 17 | adantr 481 |
. . . . . 6
⊢ ((𝐴 <<s 𝐵 ∧ 𝐴 <<s 𝐶) → (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐵 → 𝑥 <s 𝑦))) |
19 | 18 | com3r 87 |
. . . . 5
⊢ (𝑦 ∈ 𝐵 → ((𝐴 <<s 𝐵 ∧ 𝐴 <<s 𝐶) → (𝑥 ∈ 𝐴 → 𝑥 <s 𝑦))) |
20 | | ssltsepc 33987 |
. . . . . . . 8
⊢ ((𝐴 <<s 𝐶 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) → 𝑥 <s 𝑦) |
21 | 20 | 3exp 1118 |
. . . . . . 7
⊢ (𝐴 <<s 𝐶 → (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → 𝑥 <s 𝑦))) |
22 | 21 | adantl 482 |
. . . . . 6
⊢ ((𝐴 <<s 𝐵 ∧ 𝐴 <<s 𝐶) → (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → 𝑥 <s 𝑦))) |
23 | 22 | com3r 87 |
. . . . 5
⊢ (𝑦 ∈ 𝐶 → ((𝐴 <<s 𝐵 ∧ 𝐴 <<s 𝐶) → (𝑥 ∈ 𝐴 → 𝑥 <s 𝑦))) |
24 | 19, 23 | jaoi 854 |
. . . 4
⊢ ((𝑦 ∈ 𝐵 ∨ 𝑦 ∈ 𝐶) → ((𝐴 <<s 𝐵 ∧ 𝐴 <<s 𝐶) → (𝑥 ∈ 𝐴 → 𝑥 <s 𝑦))) |
25 | 15, 24 | sylbi 216 |
. . 3
⊢ (𝑦 ∈ (𝐵 ∪ 𝐶) → ((𝐴 <<s 𝐵 ∧ 𝐴 <<s 𝐶) → (𝑥 ∈ 𝐴 → 𝑥 <s 𝑦))) |
26 | 25 | 3imp231 1112 |
. 2
⊢ (((𝐴 <<s 𝐵 ∧ 𝐴 <<s 𝐶) ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐵 ∪ 𝐶)) → 𝑥 <s 𝑦) |
27 | 2, 7, 9, 14, 26 | ssltd 33986 |
1
⊢ ((𝐴 <<s 𝐵 ∧ 𝐴 <<s 𝐶) → 𝐴 <<s (𝐵 ∪ 𝐶)) |