Step | Hyp | Ref
| Expression |
1 | | ssltex1 33250 |
. . . 4
⊢ (𝐴 <<s 𝐵 → 𝐴 ∈ V) |
2 | 1 | adantr 483 |
. . 3
⊢ ((𝐴 <<s 𝐵 ∧ 𝐴 <<s 𝐶) → 𝐴 ∈ V) |
3 | | ssltex2 33251 |
. . . 4
⊢ (𝐴 <<s 𝐵 → 𝐵 ∈ V) |
4 | | ssltex2 33251 |
. . . 4
⊢ (𝐴 <<s 𝐶 → 𝐶 ∈ V) |
5 | | unexg 7466 |
. . . 4
⊢ ((𝐵 ∈ V ∧ 𝐶 ∈ V) → (𝐵 ∪ 𝐶) ∈ V) |
6 | 3, 4, 5 | syl2an 597 |
. . 3
⊢ ((𝐴 <<s 𝐵 ∧ 𝐴 <<s 𝐶) → (𝐵 ∪ 𝐶) ∈ V) |
7 | 2, 6 | jca 514 |
. 2
⊢ ((𝐴 <<s 𝐵 ∧ 𝐴 <<s 𝐶) → (𝐴 ∈ V ∧ (𝐵 ∪ 𝐶) ∈ V)) |
8 | | ssltss1 33252 |
. . . 4
⊢ (𝐴 <<s 𝐵 → 𝐴 ⊆ No
) |
9 | 8 | adantr 483 |
. . 3
⊢ ((𝐴 <<s 𝐵 ∧ 𝐴 <<s 𝐶) → 𝐴 ⊆ No
) |
10 | | ssltss2 33253 |
. . . . 5
⊢ (𝐴 <<s 𝐵 → 𝐵 ⊆ No
) |
11 | 10 | adantr 483 |
. . . 4
⊢ ((𝐴 <<s 𝐵 ∧ 𝐴 <<s 𝐶) → 𝐵 ⊆ No
) |
12 | | ssltss2 33253 |
. . . . 5
⊢ (𝐴 <<s 𝐶 → 𝐶 ⊆ No
) |
13 | 12 | adantl 484 |
. . . 4
⊢ ((𝐴 <<s 𝐵 ∧ 𝐴 <<s 𝐶) → 𝐶 ⊆ No
) |
14 | 11, 13 | unssd 4162 |
. . 3
⊢ ((𝐴 <<s 𝐵 ∧ 𝐴 <<s 𝐶) → (𝐵 ∪ 𝐶) ⊆ No
) |
15 | | ssltsep 33254 |
. . . . 5
⊢ (𝐴 <<s 𝐵 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 <s 𝑦) |
16 | 15 | adantr 483 |
. . . 4
⊢ ((𝐴 <<s 𝐵 ∧ 𝐴 <<s 𝐶) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 <s 𝑦) |
17 | | ssltsep 33254 |
. . . . 5
⊢ (𝐴 <<s 𝐶 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐶 𝑥 <s 𝑦) |
18 | 17 | adantl 484 |
. . . 4
⊢ ((𝐴 <<s 𝐵 ∧ 𝐴 <<s 𝐶) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐶 𝑥 <s 𝑦) |
19 | | ralunb 4167 |
. . . . . 6
⊢
(∀𝑦 ∈
(𝐵 ∪ 𝐶)𝑥 <s 𝑦 ↔ (∀𝑦 ∈ 𝐵 𝑥 <s 𝑦 ∧ ∀𝑦 ∈ 𝐶 𝑥 <s 𝑦)) |
20 | 19 | ralbii 3165 |
. . . . 5
⊢
(∀𝑥 ∈
𝐴 ∀𝑦 ∈ (𝐵 ∪ 𝐶)𝑥 <s 𝑦 ↔ ∀𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 𝑥 <s 𝑦 ∧ ∀𝑦 ∈ 𝐶 𝑥 <s 𝑦)) |
21 | | r19.26 3170 |
. . . . 5
⊢
(∀𝑥 ∈
𝐴 (∀𝑦 ∈ 𝐵 𝑥 <s 𝑦 ∧ ∀𝑦 ∈ 𝐶 𝑥 <s 𝑦) ↔ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 <s 𝑦 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐶 𝑥 <s 𝑦)) |
22 | 20, 21 | bitri 277 |
. . . 4
⊢
(∀𝑥 ∈
𝐴 ∀𝑦 ∈ (𝐵 ∪ 𝐶)𝑥 <s 𝑦 ↔ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 <s 𝑦 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐶 𝑥 <s 𝑦)) |
23 | 16, 18, 22 | sylanbrc 585 |
. . 3
⊢ ((𝐴 <<s 𝐵 ∧ 𝐴 <<s 𝐶) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ (𝐵 ∪ 𝐶)𝑥 <s 𝑦) |
24 | 9, 14, 23 | 3jca 1124 |
. 2
⊢ ((𝐴 <<s 𝐵 ∧ 𝐴 <<s 𝐶) → (𝐴 ⊆ No
∧ (𝐵 ∪ 𝐶) ⊆
No ∧ ∀𝑥
∈ 𝐴 ∀𝑦 ∈ (𝐵 ∪ 𝐶)𝑥 <s 𝑦)) |
25 | | brsslt 33249 |
. 2
⊢ (𝐴 <<s (𝐵 ∪ 𝐶) ↔ ((𝐴 ∈ V ∧ (𝐵 ∪ 𝐶) ∈ V) ∧ (𝐴 ⊆ No
∧ (𝐵 ∪ 𝐶) ⊆
No ∧ ∀𝑥
∈ 𝐴 ∀𝑦 ∈ (𝐵 ∪ 𝐶)𝑥 <s 𝑦))) |
26 | 7, 24, 25 | sylanbrc 585 |
1
⊢ ((𝐴 <<s 𝐵 ∧ 𝐴 <<s 𝐶) → 𝐴 <<s (𝐵 ∪ 𝐶)) |