Step | Hyp | Ref
| Expression |
1 | | n0 3931 |
. . . 4
⊢ (𝐵 ≠ ∅ ↔
∃𝑦 𝑦 ∈ 𝐵) |
2 | | ssltex1 31901 |
. . . . . . . . 9
⊢ (𝐴 <<s 𝐵 → 𝐴 ∈ V) |
3 | | ssltex2 31902 |
. . . . . . . . 9
⊢ (𝐵 <<s 𝐶 → 𝐶 ∈ V) |
4 | 2, 3 | anim12i 590 |
. . . . . . . 8
⊢ ((𝐴 <<s 𝐵 ∧ 𝐵 <<s 𝐶) → (𝐴 ∈ V ∧ 𝐶 ∈ V)) |
5 | 4 | adantl 482 |
. . . . . . 7
⊢ ((𝑦 ∈ 𝐵 ∧ (𝐴 <<s 𝐵 ∧ 𝐵 <<s 𝐶)) → (𝐴 ∈ V ∧ 𝐶 ∈ V)) |
6 | | ssltss1 31903 |
. . . . . . . . 9
⊢ (𝐴 <<s 𝐵 → 𝐴 ⊆ No
) |
7 | 6 | ad2antrl 764 |
. . . . . . . 8
⊢ ((𝑦 ∈ 𝐵 ∧ (𝐴 <<s 𝐵 ∧ 𝐵 <<s 𝐶)) → 𝐴 ⊆ No
) |
8 | | ssltss2 31904 |
. . . . . . . . 9
⊢ (𝐵 <<s 𝐶 → 𝐶 ⊆ No
) |
9 | 8 | ad2antll 765 |
. . . . . . . 8
⊢ ((𝑦 ∈ 𝐵 ∧ (𝐴 <<s 𝐵 ∧ 𝐵 <<s 𝐶)) → 𝐶 ⊆ No
) |
10 | 7 | adantr 481 |
. . . . . . . . . . 11
⊢ (((𝑦 ∈ 𝐵 ∧ (𝐴 <<s 𝐵 ∧ 𝐵 <<s 𝐶)) ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶)) → 𝐴 ⊆ No
) |
11 | | simprl 794 |
. . . . . . . . . . 11
⊢ (((𝑦 ∈ 𝐵 ∧ (𝐴 <<s 𝐵 ∧ 𝐵 <<s 𝐶)) ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶)) → 𝑥 ∈ 𝐴) |
12 | 10, 11 | sseldd 3604 |
. . . . . . . . . 10
⊢ (((𝑦 ∈ 𝐵 ∧ (𝐴 <<s 𝐵 ∧ 𝐵 <<s 𝐶)) ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶)) → 𝑥 ∈ No
) |
13 | | ssltss1 31903 |
. . . . . . . . . . . . 13
⊢ (𝐵 <<s 𝐶 → 𝐵 ⊆ No
) |
14 | 13 | ad2antll 765 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ 𝐵 ∧ (𝐴 <<s 𝐵 ∧ 𝐵 <<s 𝐶)) → 𝐵 ⊆ No
) |
15 | 14 | adantr 481 |
. . . . . . . . . . 11
⊢ (((𝑦 ∈ 𝐵 ∧ (𝐴 <<s 𝐵 ∧ 𝐵 <<s 𝐶)) ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶)) → 𝐵 ⊆ No
) |
16 | | simpll 790 |
. . . . . . . . . . 11
⊢ (((𝑦 ∈ 𝐵 ∧ (𝐴 <<s 𝐵 ∧ 𝐵 <<s 𝐶)) ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶)) → 𝑦 ∈ 𝐵) |
17 | 15, 16 | sseldd 3604 |
. . . . . . . . . 10
⊢ (((𝑦 ∈ 𝐵 ∧ (𝐴 <<s 𝐵 ∧ 𝐵 <<s 𝐶)) ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶)) → 𝑦 ∈ No
) |
18 | 9 | adantr 481 |
. . . . . . . . . . 11
⊢ (((𝑦 ∈ 𝐵 ∧ (𝐴 <<s 𝐵 ∧ 𝐵 <<s 𝐶)) ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶)) → 𝐶 ⊆ No
) |
19 | | simprr 796 |
. . . . . . . . . . 11
⊢ (((𝑦 ∈ 𝐵 ∧ (𝐴 <<s 𝐵 ∧ 𝐵 <<s 𝐶)) ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶)) → 𝑧 ∈ 𝐶) |
20 | 18, 19 | sseldd 3604 |
. . . . . . . . . 10
⊢ (((𝑦 ∈ 𝐵 ∧ (𝐴 <<s 𝐵 ∧ 𝐵 <<s 𝐶)) ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶)) → 𝑧 ∈ No
) |
21 | | ssltsep 31905 |
. . . . . . . . . . . . . 14
⊢ (𝐴 <<s 𝐵 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 <s 𝑦) |
22 | 21 | ad2antrl 764 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ 𝐵 ∧ (𝐴 <<s 𝐵 ∧ 𝐵 <<s 𝐶)) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 <s 𝑦) |
23 | 22 | adantr 481 |
. . . . . . . . . . . 12
⊢ (((𝑦 ∈ 𝐵 ∧ (𝐴 <<s 𝐵 ∧ 𝐵 <<s 𝐶)) ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶)) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 <s 𝑦) |
24 | | rsp 2929 |
. . . . . . . . . . . 12
⊢
(∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐵 𝑥 <s 𝑦 → (𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐵 𝑥 <s 𝑦)) |
25 | 23, 11, 24 | sylc 65 |
. . . . . . . . . . 11
⊢ (((𝑦 ∈ 𝐵 ∧ (𝐴 <<s 𝐵 ∧ 𝐵 <<s 𝐶)) ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶)) → ∀𝑦 ∈ 𝐵 𝑥 <s 𝑦) |
26 | | rsp 2929 |
. . . . . . . . . . 11
⊢
(∀𝑦 ∈
𝐵 𝑥 <s 𝑦 → (𝑦 ∈ 𝐵 → 𝑥 <s 𝑦)) |
27 | 25, 16, 26 | sylc 65 |
. . . . . . . . . 10
⊢ (((𝑦 ∈ 𝐵 ∧ (𝐴 <<s 𝐵 ∧ 𝐵 <<s 𝐶)) ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶)) → 𝑥 <s 𝑦) |
28 | | ssltsep 31905 |
. . . . . . . . . . . . . 14
⊢ (𝐵 <<s 𝐶 → ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝑦 <s 𝑧) |
29 | 28 | ad2antll 765 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ 𝐵 ∧ (𝐴 <<s 𝐵 ∧ 𝐵 <<s 𝐶)) → ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝑦 <s 𝑧) |
30 | 29 | adantr 481 |
. . . . . . . . . . . 12
⊢ (((𝑦 ∈ 𝐵 ∧ (𝐴 <<s 𝐵 ∧ 𝐵 <<s 𝐶)) ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶)) → ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝑦 <s 𝑧) |
31 | | rsp 2929 |
. . . . . . . . . . . 12
⊢
(∀𝑦 ∈
𝐵 ∀𝑧 ∈ 𝐶 𝑦 <s 𝑧 → (𝑦 ∈ 𝐵 → ∀𝑧 ∈ 𝐶 𝑦 <s 𝑧)) |
32 | 30, 16, 31 | sylc 65 |
. . . . . . . . . . 11
⊢ (((𝑦 ∈ 𝐵 ∧ (𝐴 <<s 𝐵 ∧ 𝐵 <<s 𝐶)) ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶)) → ∀𝑧 ∈ 𝐶 𝑦 <s 𝑧) |
33 | | rsp 2929 |
. . . . . . . . . . 11
⊢
(∀𝑧 ∈
𝐶 𝑦 <s 𝑧 → (𝑧 ∈ 𝐶 → 𝑦 <s 𝑧)) |
34 | 32, 19, 33 | sylc 65 |
. . . . . . . . . 10
⊢ (((𝑦 ∈ 𝐵 ∧ (𝐴 <<s 𝐵 ∧ 𝐵 <<s 𝐶)) ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶)) → 𝑦 <s 𝑧) |
35 | 12, 17, 20, 27, 34 | slttrd 31884 |
. . . . . . . . 9
⊢ (((𝑦 ∈ 𝐵 ∧ (𝐴 <<s 𝐵 ∧ 𝐵 <<s 𝐶)) ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶)) → 𝑥 <s 𝑧) |
36 | 35 | ralrimivva 2971 |
. . . . . . . 8
⊢ ((𝑦 ∈ 𝐵 ∧ (𝐴 <<s 𝐵 ∧ 𝐵 <<s 𝐶)) → ∀𝑥 ∈ 𝐴 ∀𝑧 ∈ 𝐶 𝑥 <s 𝑧) |
37 | 7, 9, 36 | 3jca 1242 |
. . . . . . 7
⊢ ((𝑦 ∈ 𝐵 ∧ (𝐴 <<s 𝐵 ∧ 𝐵 <<s 𝐶)) → (𝐴 ⊆ No
∧ 𝐶 ⊆ No ∧ ∀𝑥 ∈ 𝐴 ∀𝑧 ∈ 𝐶 𝑥 <s 𝑧)) |
38 | | brsslt 31900 |
. . . . . . 7
⊢ (𝐴 <<s 𝐶 ↔ ((𝐴 ∈ V ∧ 𝐶 ∈ V) ∧ (𝐴 ⊆ No
∧ 𝐶 ⊆ No ∧ ∀𝑥 ∈ 𝐴 ∀𝑧 ∈ 𝐶 𝑥 <s 𝑧))) |
39 | 5, 37, 38 | sylanbrc 698 |
. . . . . 6
⊢ ((𝑦 ∈ 𝐵 ∧ (𝐴 <<s 𝐵 ∧ 𝐵 <<s 𝐶)) → 𝐴 <<s 𝐶) |
40 | 39 | ex 450 |
. . . . 5
⊢ (𝑦 ∈ 𝐵 → ((𝐴 <<s 𝐵 ∧ 𝐵 <<s 𝐶) → 𝐴 <<s 𝐶)) |
41 | 40 | exlimiv 1858 |
. . . 4
⊢
(∃𝑦 𝑦 ∈ 𝐵 → ((𝐴 <<s 𝐵 ∧ 𝐵 <<s 𝐶) → 𝐴 <<s 𝐶)) |
42 | 1, 41 | sylbi 207 |
. . 3
⊢ (𝐵 ≠ ∅ → ((𝐴 <<s 𝐵 ∧ 𝐵 <<s 𝐶) → 𝐴 <<s 𝐶)) |
43 | 42 | com12 32 |
. 2
⊢ ((𝐴 <<s 𝐵 ∧ 𝐵 <<s 𝐶) → (𝐵 ≠ ∅ → 𝐴 <<s 𝐶)) |
44 | 43 | 3impia 1261 |
1
⊢ ((𝐴 <<s 𝐵 ∧ 𝐵 <<s 𝐶 ∧ 𝐵 ≠ ∅) → 𝐴 <<s 𝐶) |