| Step | Hyp | Ref
| Expression |
|---|
| 1 | | sltsex1 27780 |
. . 3
⊢ (𝐴 <<s 𝐶 → 𝐴 ∈ V) |
| 2 | 1 | 3ad2ant3 1141 |
. 2
⊢ ((𝐵 ∈ 𝒫 No ∧ ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 𝑦 ≤s 𝑥 ∧ 𝐴 <<s 𝐶) → 𝐴 ∈ V) |
| 3 | | simp1 1142 |
. 2
⊢ ((𝐵 ∈ 𝒫 No ∧ ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 𝑦 ≤s 𝑥 ∧ 𝐴 <<s 𝐶) → 𝐵 ∈ 𝒫 No
) |
| 4 | | sltsss1 27782 |
. . 3
⊢ (𝐴 <<s 𝐶 → 𝐴 ⊆ No
) |
| 5 | 4 | 3ad2ant3 1141 |
. 2
⊢ ((𝐵 ∈ 𝒫 No ∧ ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 𝑦 ≤s 𝑥 ∧ 𝐴 <<s 𝐶) → 𝐴 ⊆ No
) |
| 6 | 3 | elpwid 4545 |
. 2
⊢ ((𝐵 ∈ 𝒫 No ∧ ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 𝑦 ≤s 𝑥 ∧ 𝐴 <<s 𝐶) → 𝐵 ⊆ No
) |
| 7 | | breq2 5083 |
. . . . . 6
⊢ (𝑥 = 𝑏 → (𝑦 ≤s 𝑥 ↔ 𝑦 ≤s 𝑏)) |
| 8 | 7 | rexbidv 3164 |
. . . . 5
⊢ (𝑥 = 𝑏 → (∃𝑦 ∈ 𝐶 𝑦 ≤s 𝑥 ↔ ∃𝑦 ∈ 𝐶 𝑦 ≤s 𝑏)) |
| 9 | | simp12 1211 |
. . . . 5
⊢ (((𝐵 ∈ 𝒫 No ∧ ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 𝑦 ≤s 𝑥 ∧ 𝐴 <<s 𝐶) ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 𝑦 ≤s 𝑥) |
| 10 | | simp3 1144 |
. . . . 5
⊢ (((𝐵 ∈ 𝒫 No ∧ ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 𝑦 ≤s 𝑥 ∧ 𝐴 <<s 𝐶) ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ 𝐵) |
| 11 | 8, 9, 10 | rspcdva 3568 |
. . . 4
⊢ (((𝐵 ∈ 𝒫 No ∧ ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 𝑦 ≤s 𝑥 ∧ 𝐴 <<s 𝐶) ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → ∃𝑦 ∈ 𝐶 𝑦 ≤s 𝑏) |
| 12 | | breq1 5082 |
. . . . 5
⊢ (𝑦 = 𝑐 → (𝑦 ≤s 𝑏 ↔ 𝑐 ≤s 𝑏)) |
| 13 | 12 | cbvrexvw 3219 |
. . . 4
⊢
(∃𝑦 ∈
𝐶 𝑦 ≤s 𝑏 ↔ ∃𝑐 ∈ 𝐶 𝑐 ≤s 𝑏) |
| 14 | 11, 13 | sylib 219 |
. . 3
⊢ (((𝐵 ∈ 𝒫 No ∧ ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 𝑦 ≤s 𝑥 ∧ 𝐴 <<s 𝐶) ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → ∃𝑐 ∈ 𝐶 𝑐 ≤s 𝑏) |
| 15 | | simpl13 1257 |
. . . . . 6
⊢ ((((𝐵 ∈ 𝒫 No ∧ ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 𝑦 ≤s 𝑥 ∧ 𝐴 <<s 𝐶) ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐶 ∧ 𝑐 ≤s 𝑏)) → 𝐴 <<s 𝐶) |
| 16 | 15, 4 | syl 17 |
. . . . 5
⊢ ((((𝐵 ∈ 𝒫 No ∧ ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 𝑦 ≤s 𝑥 ∧ 𝐴 <<s 𝐶) ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐶 ∧ 𝑐 ≤s 𝑏)) → 𝐴 ⊆ No
) |
| 17 | | simpl2 1199 |
. . . . 5
⊢ ((((𝐵 ∈ 𝒫 No ∧ ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 𝑦 ≤s 𝑥 ∧ 𝐴 <<s 𝐶) ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐶 ∧ 𝑐 ≤s 𝑏)) → 𝑎 ∈ 𝐴) |
| 18 | 16, 17 | sseldd 3923 |
. . . 4
⊢ ((((𝐵 ∈ 𝒫 No ∧ ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 𝑦 ≤s 𝑥 ∧ 𝐴 <<s 𝐶) ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐶 ∧ 𝑐 ≤s 𝑏)) → 𝑎 ∈ No
) |
| 19 | | sltsss2 27783 |
. . . . . 6
⊢ (𝐴 <<s 𝐶 → 𝐶 ⊆ No
) |
| 20 | 15, 19 | syl 17 |
. . . . 5
⊢ ((((𝐵 ∈ 𝒫 No ∧ ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 𝑦 ≤s 𝑥 ∧ 𝐴 <<s 𝐶) ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐶 ∧ 𝑐 ≤s 𝑏)) → 𝐶 ⊆ No
) |
| 21 | | simprl 776 |
. . . . 5
⊢ ((((𝐵 ∈ 𝒫 No ∧ ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 𝑦 ≤s 𝑥 ∧ 𝐴 <<s 𝐶) ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐶 ∧ 𝑐 ≤s 𝑏)) → 𝑐 ∈ 𝐶) |
| 22 | 20, 21 | sseldd 3923 |
. . . 4
⊢ ((((𝐵 ∈ 𝒫 No ∧ ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 𝑦 ≤s 𝑥 ∧ 𝐴 <<s 𝐶) ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐶 ∧ 𝑐 ≤s 𝑏)) → 𝑐 ∈ No
) |
| 23 | | simpl1 1198 |
. . . . . 6
⊢ ((((𝐵 ∈ 𝒫 No ∧ ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 𝑦 ≤s 𝑥 ∧ 𝐴 <<s 𝐶) ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐶 ∧ 𝑐 ≤s 𝑏)) → (𝐵 ∈ 𝒫 No
∧ ∀𝑥
∈ 𝐵 ∃𝑦 ∈ 𝐶 𝑦 ≤s 𝑥 ∧ 𝐴 <<s 𝐶)) |
| 24 | 23, 6 | syl 17 |
. . . . 5
⊢ ((((𝐵 ∈ 𝒫 No ∧ ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 𝑦 ≤s 𝑥 ∧ 𝐴 <<s 𝐶) ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐶 ∧ 𝑐 ≤s 𝑏)) → 𝐵 ⊆ No
) |
| 25 | | simpl3 1200 |
. . . . 5
⊢ ((((𝐵 ∈ 𝒫 No ∧ ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 𝑦 ≤s 𝑥 ∧ 𝐴 <<s 𝐶) ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐶 ∧ 𝑐 ≤s 𝑏)) → 𝑏 ∈ 𝐵) |
| 26 | 24, 25 | sseldd 3923 |
. . . 4
⊢ ((((𝐵 ∈ 𝒫 No ∧ ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 𝑦 ≤s 𝑥 ∧ 𝐴 <<s 𝐶) ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐶 ∧ 𝑐 ≤s 𝑏)) → 𝑏 ∈ No
) |
| 27 | 15, 17, 21 | sltssepcd 27789 |
. . . 4
⊢ ((((𝐵 ∈ 𝒫 No ∧ ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 𝑦 ≤s 𝑥 ∧ 𝐴 <<s 𝐶) ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐶 ∧ 𝑐 ≤s 𝑏)) → 𝑎 <s 𝑐) |
| 28 | | simprr 778 |
. . . 4
⊢ ((((𝐵 ∈ 𝒫 No ∧ ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 𝑦 ≤s 𝑥 ∧ 𝐴 <<s 𝐶) ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐶 ∧ 𝑐 ≤s 𝑏)) → 𝑐 ≤s 𝑏) |
| 29 | 18, 22, 26, 27, 28 | ltlestrd 27753 |
. . 3
⊢ ((((𝐵 ∈ 𝒫 No ∧ ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 𝑦 ≤s 𝑥 ∧ 𝐴 <<s 𝐶) ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐶 ∧ 𝑐 ≤s 𝑏)) → 𝑎 <s 𝑏) |
| 30 | 14, 29 | rexlimddv 3147 |
. 2
⊢ (((𝐵 ∈ 𝒫 No ∧ ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 𝑦 ≤s 𝑥 ∧ 𝐴 <<s 𝐶) ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → 𝑎 <s 𝑏) |
| 31 | 2, 3, 5, 6, 30 | sltsd 27785 |
1
⊢ ((𝐵 ∈ 𝒫 No ∧ ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 𝑦 ≤s 𝑥 ∧ 𝐴 <<s 𝐶) → 𝐴 <<s 𝐵) |
