Step | Hyp | Ref
| Expression |
1 | | ssltex1 33255 |
. . . 4
⊢ (𝐴 <<s 𝐶 → 𝐴 ∈ V) |
2 | | ssltex1 33255 |
. . . 4
⊢ (𝐵 <<s 𝐶 → 𝐵 ∈ V) |
3 | | unexg 7472 |
. . . 4
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴 ∪ 𝐵) ∈ V) |
4 | 1, 2, 3 | syl2an 597 |
. . 3
⊢ ((𝐴 <<s 𝐶 ∧ 𝐵 <<s 𝐶) → (𝐴 ∪ 𝐵) ∈ V) |
5 | | ssltex2 33256 |
. . . 4
⊢ (𝐴 <<s 𝐶 → 𝐶 ∈ V) |
6 | 5 | adantr 483 |
. . 3
⊢ ((𝐴 <<s 𝐶 ∧ 𝐵 <<s 𝐶) → 𝐶 ∈ V) |
7 | 4, 6 | jca 514 |
. 2
⊢ ((𝐴 <<s 𝐶 ∧ 𝐵 <<s 𝐶) → ((𝐴 ∪ 𝐵) ∈ V ∧ 𝐶 ∈ V)) |
8 | | ssltss1 33257 |
. . . . 5
⊢ (𝐴 <<s 𝐶 → 𝐴 ⊆ No
) |
9 | 8 | adantr 483 |
. . . 4
⊢ ((𝐴 <<s 𝐶 ∧ 𝐵 <<s 𝐶) → 𝐴 ⊆ No
) |
10 | | ssltss1 33257 |
. . . . 5
⊢ (𝐵 <<s 𝐶 → 𝐵 ⊆ No
) |
11 | 10 | adantl 484 |
. . . 4
⊢ ((𝐴 <<s 𝐶 ∧ 𝐵 <<s 𝐶) → 𝐵 ⊆ No
) |
12 | 9, 11 | unssd 4162 |
. . 3
⊢ ((𝐴 <<s 𝐶 ∧ 𝐵 <<s 𝐶) → (𝐴 ∪ 𝐵) ⊆ No
) |
13 | | ssltss2 33258 |
. . . 4
⊢ (𝐵 <<s 𝐶 → 𝐶 ⊆ No
) |
14 | 13 | adantl 484 |
. . 3
⊢ ((𝐴 <<s 𝐶 ∧ 𝐵 <<s 𝐶) → 𝐶 ⊆ No
) |
15 | | ssltsep 33259 |
. . . . 5
⊢ (𝐴 <<s 𝐶 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐶 𝑥 <s 𝑦) |
16 | 15 | adantr 483 |
. . . 4
⊢ ((𝐴 <<s 𝐶 ∧ 𝐵 <<s 𝐶) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐶 𝑥 <s 𝑦) |
17 | | ssltsep 33259 |
. . . . 5
⊢ (𝐵 <<s 𝐶 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐶 𝑥 <s 𝑦) |
18 | 17 | adantl 484 |
. . . 4
⊢ ((𝐴 <<s 𝐶 ∧ 𝐵 <<s 𝐶) → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐶 𝑥 <s 𝑦) |
19 | | ralunb 4167 |
. . . 4
⊢
(∀𝑥 ∈
(𝐴 ∪ 𝐵)∀𝑦 ∈ 𝐶 𝑥 <s 𝑦 ↔ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐶 𝑥 <s 𝑦 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐶 𝑥 <s 𝑦)) |
20 | 16, 18, 19 | sylanbrc 585 |
. . 3
⊢ ((𝐴 <<s 𝐶 ∧ 𝐵 <<s 𝐶) → ∀𝑥 ∈ (𝐴 ∪ 𝐵)∀𝑦 ∈ 𝐶 𝑥 <s 𝑦) |
21 | 12, 14, 20 | 3jca 1124 |
. 2
⊢ ((𝐴 <<s 𝐶 ∧ 𝐵 <<s 𝐶) → ((𝐴 ∪ 𝐵) ⊆ No
∧ 𝐶 ⊆ No ∧ ∀𝑥 ∈ (𝐴 ∪ 𝐵)∀𝑦 ∈ 𝐶 𝑥 <s 𝑦)) |
22 | | brsslt 33254 |
. 2
⊢ ((𝐴 ∪ 𝐵) <<s 𝐶 ↔ (((𝐴 ∪ 𝐵) ∈ V ∧ 𝐶 ∈ V) ∧ ((𝐴 ∪ 𝐵) ⊆ No
∧ 𝐶 ⊆ No ∧ ∀𝑥 ∈ (𝐴 ∪ 𝐵)∀𝑦 ∈ 𝐶 𝑥 <s 𝑦))) |
23 | 7, 21, 22 | sylanbrc 585 |
1
⊢ ((𝐴 <<s 𝐶 ∧ 𝐵 <<s 𝐶) → (𝐴 ∪ 𝐵) <<s 𝐶) |