Step | Hyp | Ref
| Expression |
1 | | ssltex1 32782 |
. . . 4
⊢ (𝐴 <<s 𝐵 → 𝐴 ∈ V) |
2 | 1 | adantr 473 |
. . 3
⊢ ((𝐴 <<s 𝐵 ∧ 𝐴 <<s 𝐶) → 𝐴 ∈ V) |
3 | | ssltex2 32783 |
. . . 4
⊢ (𝐴 <<s 𝐵 → 𝐵 ∈ V) |
4 | | ssltex2 32783 |
. . . 4
⊢ (𝐴 <<s 𝐶 → 𝐶 ∈ V) |
5 | | unexg 7289 |
. . . 4
⊢ ((𝐵 ∈ V ∧ 𝐶 ∈ V) → (𝐵 ∪ 𝐶) ∈ V) |
6 | 3, 4, 5 | syl2an 586 |
. . 3
⊢ ((𝐴 <<s 𝐵 ∧ 𝐴 <<s 𝐶) → (𝐵 ∪ 𝐶) ∈ V) |
7 | 2, 6 | jca 504 |
. 2
⊢ ((𝐴 <<s 𝐵 ∧ 𝐴 <<s 𝐶) → (𝐴 ∈ V ∧ (𝐵 ∪ 𝐶) ∈ V)) |
8 | | ssltss1 32784 |
. . . 4
⊢ (𝐴 <<s 𝐵 → 𝐴 ⊆ No
) |
9 | 8 | adantr 473 |
. . 3
⊢ ((𝐴 <<s 𝐵 ∧ 𝐴 <<s 𝐶) → 𝐴 ⊆ No
) |
10 | | ssltss2 32785 |
. . . . 5
⊢ (𝐴 <<s 𝐵 → 𝐵 ⊆ No
) |
11 | 10 | adantr 473 |
. . . 4
⊢ ((𝐴 <<s 𝐵 ∧ 𝐴 <<s 𝐶) → 𝐵 ⊆ No
) |
12 | | ssltss2 32785 |
. . . . 5
⊢ (𝐴 <<s 𝐶 → 𝐶 ⊆ No
) |
13 | 12 | adantl 474 |
. . . 4
⊢ ((𝐴 <<s 𝐵 ∧ 𝐴 <<s 𝐶) → 𝐶 ⊆ No
) |
14 | 11, 13 | unssd 4050 |
. . 3
⊢ ((𝐴 <<s 𝐵 ∧ 𝐴 <<s 𝐶) → (𝐵 ∪ 𝐶) ⊆ No
) |
15 | | ssltsep 32786 |
. . . . 5
⊢ (𝐴 <<s 𝐵 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 <s 𝑦) |
16 | 15 | adantr 473 |
. . . 4
⊢ ((𝐴 <<s 𝐵 ∧ 𝐴 <<s 𝐶) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 <s 𝑦) |
17 | | ssltsep 32786 |
. . . . 5
⊢ (𝐴 <<s 𝐶 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐶 𝑥 <s 𝑦) |
18 | 17 | adantl 474 |
. . . 4
⊢ ((𝐴 <<s 𝐵 ∧ 𝐴 <<s 𝐶) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐶 𝑥 <s 𝑦) |
19 | | ralunb 4055 |
. . . . . 6
⊢
(∀𝑦 ∈
(𝐵 ∪ 𝐶)𝑥 <s 𝑦 ↔ (∀𝑦 ∈ 𝐵 𝑥 <s 𝑦 ∧ ∀𝑦 ∈ 𝐶 𝑥 <s 𝑦)) |
20 | 19 | ralbii 3115 |
. . . . 5
⊢
(∀𝑥 ∈
𝐴 ∀𝑦 ∈ (𝐵 ∪ 𝐶)𝑥 <s 𝑦 ↔ ∀𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 𝑥 <s 𝑦 ∧ ∀𝑦 ∈ 𝐶 𝑥 <s 𝑦)) |
21 | | r19.26 3120 |
. . . . 5
⊢
(∀𝑥 ∈
𝐴 (∀𝑦 ∈ 𝐵 𝑥 <s 𝑦 ∧ ∀𝑦 ∈ 𝐶 𝑥 <s 𝑦) ↔ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 <s 𝑦 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐶 𝑥 <s 𝑦)) |
22 | 20, 21 | bitri 267 |
. . . 4
⊢
(∀𝑥 ∈
𝐴 ∀𝑦 ∈ (𝐵 ∪ 𝐶)𝑥 <s 𝑦 ↔ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 <s 𝑦 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐶 𝑥 <s 𝑦)) |
23 | 16, 18, 22 | sylanbrc 575 |
. . 3
⊢ ((𝐴 <<s 𝐵 ∧ 𝐴 <<s 𝐶) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ (𝐵 ∪ 𝐶)𝑥 <s 𝑦) |
24 | 9, 14, 23 | 3jca 1108 |
. 2
⊢ ((𝐴 <<s 𝐵 ∧ 𝐴 <<s 𝐶) → (𝐴 ⊆ No
∧ (𝐵 ∪ 𝐶) ⊆
No ∧ ∀𝑥
∈ 𝐴 ∀𝑦 ∈ (𝐵 ∪ 𝐶)𝑥 <s 𝑦)) |
25 | | brsslt 32781 |
. 2
⊢ (𝐴 <<s (𝐵 ∪ 𝐶) ↔ ((𝐴 ∈ V ∧ (𝐵 ∪ 𝐶) ∈ V) ∧ (𝐴 ⊆ No
∧ (𝐵 ∪ 𝐶) ⊆
No ∧ ∀𝑥
∈ 𝐴 ∀𝑦 ∈ (𝐵 ∪ 𝐶)𝑥 <s 𝑦))) |
26 | 7, 24, 25 | sylanbrc 575 |
1
⊢ ((𝐴 <<s 𝐵 ∧ 𝐴 <<s 𝐶) → 𝐴 <<s (𝐵 ∪ 𝐶)) |