| Step | Hyp | Ref
| Expression |
|---|
| 1 | | ssltex1 27719 |
. . 3
⊢ (𝐴 <<s 𝐶 → 𝐴 ∈ V) |
| 2 | 1 | 3ad2ant3 1135 |
. 2
⊢ ((𝐵 ∈ 𝒫 No ∧ ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 𝑦 ≤s 𝑥 ∧ 𝐴 <<s 𝐶) → 𝐴 ∈ V) |
| 3 | | simp1 1136 |
. 2
⊢ ((𝐵 ∈ 𝒫 No ∧ ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 𝑦 ≤s 𝑥 ∧ 𝐴 <<s 𝐶) → 𝐵 ∈ 𝒫 No
) |
| 4 | | ssltss1 27721 |
. . 3
⊢ (𝐴 <<s 𝐶 → 𝐴 ⊆ No
) |
| 5 | 4 | 3ad2ant3 1135 |
. 2
⊢ ((𝐵 ∈ 𝒫 No ∧ ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 𝑦 ≤s 𝑥 ∧ 𝐴 <<s 𝐶) → 𝐴 ⊆ No
) |
| 6 | 3 | elpwid 4557 |
. 2
⊢ ((𝐵 ∈ 𝒫 No ∧ ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 𝑦 ≤s 𝑥 ∧ 𝐴 <<s 𝐶) → 𝐵 ⊆ No
) |
| 7 | | breq2 5093 |
. . . . . 6
⊢ (𝑥 = 𝑏 → (𝑦 ≤s 𝑥 ↔ 𝑦 ≤s 𝑏)) |
| 8 | 7 | rexbidv 3154 |
. . . . 5
⊢ (𝑥 = 𝑏 → (∃𝑦 ∈ 𝐶 𝑦 ≤s 𝑥 ↔ ∃𝑦 ∈ 𝐶 𝑦 ≤s 𝑏)) |
| 9 | | simp12 1205 |
. . . . 5
⊢ (((𝐵 ∈ 𝒫 No ∧ ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 𝑦 ≤s 𝑥 ∧ 𝐴 <<s 𝐶) ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 𝑦 ≤s 𝑥) |
| 10 | | simp3 1138 |
. . . . 5
⊢ (((𝐵 ∈ 𝒫 No ∧ ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 𝑦 ≤s 𝑥 ∧ 𝐴 <<s 𝐶) ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ 𝐵) |
| 11 | 8, 9, 10 | rspcdva 3576 |
. . . 4
⊢ (((𝐵 ∈ 𝒫 No ∧ ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 𝑦 ≤s 𝑥 ∧ 𝐴 <<s 𝐶) ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → ∃𝑦 ∈ 𝐶 𝑦 ≤s 𝑏) |
| 12 | | breq1 5092 |
. . . . 5
⊢ (𝑦 = 𝑐 → (𝑦 ≤s 𝑏 ↔ 𝑐 ≤s 𝑏)) |
| 13 | 12 | cbvrexvw 3209 |
. . . 4
⊢
(∃𝑦 ∈
𝐶 𝑦 ≤s 𝑏 ↔ ∃𝑐 ∈ 𝐶 𝑐 ≤s 𝑏) |
| 14 | 11, 13 | sylib 218 |
. . 3
⊢ (((𝐵 ∈ 𝒫 No ∧ ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 𝑦 ≤s 𝑥 ∧ 𝐴 <<s 𝐶) ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → ∃𝑐 ∈ 𝐶 𝑐 ≤s 𝑏) |
| 15 | | simpl13 1251 |
. . . . . 6
⊢ ((((𝐵 ∈ 𝒫 No ∧ ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 𝑦 ≤s 𝑥 ∧ 𝐴 <<s 𝐶) ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐶 ∧ 𝑐 ≤s 𝑏)) → 𝐴 <<s 𝐶) |
| 16 | 15, 4 | syl 17 |
. . . . 5
⊢ ((((𝐵 ∈ 𝒫 No ∧ ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 𝑦 ≤s 𝑥 ∧ 𝐴 <<s 𝐶) ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐶 ∧ 𝑐 ≤s 𝑏)) → 𝐴 ⊆ No
) |
| 17 | | simpl2 1193 |
. . . . 5
⊢ ((((𝐵 ∈ 𝒫 No ∧ ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 𝑦 ≤s 𝑥 ∧ 𝐴 <<s 𝐶) ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐶 ∧ 𝑐 ≤s 𝑏)) → 𝑎 ∈ 𝐴) |
| 18 | 16, 17 | sseldd 3933 |
. . . 4
⊢ ((((𝐵 ∈ 𝒫 No ∧ ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 𝑦 ≤s 𝑥 ∧ 𝐴 <<s 𝐶) ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐶 ∧ 𝑐 ≤s 𝑏)) → 𝑎 ∈ No
) |
| 19 | | ssltss2 27722 |
. . . . . 6
⊢ (𝐴 <<s 𝐶 → 𝐶 ⊆ No
) |
| 20 | 15, 19 | syl 17 |
. . . . 5
⊢ ((((𝐵 ∈ 𝒫 No ∧ ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 𝑦 ≤s 𝑥 ∧ 𝐴 <<s 𝐶) ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐶 ∧ 𝑐 ≤s 𝑏)) → 𝐶 ⊆ No
) |
| 21 | | simprl 770 |
. . . . 5
⊢ ((((𝐵 ∈ 𝒫 No ∧ ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 𝑦 ≤s 𝑥 ∧ 𝐴 <<s 𝐶) ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐶 ∧ 𝑐 ≤s 𝑏)) → 𝑐 ∈ 𝐶) |
| 22 | 20, 21 | sseldd 3933 |
. . . 4
⊢ ((((𝐵 ∈ 𝒫 No ∧ ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 𝑦 ≤s 𝑥 ∧ 𝐴 <<s 𝐶) ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐶 ∧ 𝑐 ≤s 𝑏)) → 𝑐 ∈ No
) |
| 23 | | simpl1 1192 |
. . . . . 6
⊢ ((((𝐵 ∈ 𝒫 No ∧ ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 𝑦 ≤s 𝑥 ∧ 𝐴 <<s 𝐶) ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐶 ∧ 𝑐 ≤s 𝑏)) → (𝐵 ∈ 𝒫 No
∧ ∀𝑥
∈ 𝐵 ∃𝑦 ∈ 𝐶 𝑦 ≤s 𝑥 ∧ 𝐴 <<s 𝐶)) |
| 24 | 23, 6 | syl 17 |
. . . . 5
⊢ ((((𝐵 ∈ 𝒫 No ∧ ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 𝑦 ≤s 𝑥 ∧ 𝐴 <<s 𝐶) ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐶 ∧ 𝑐 ≤s 𝑏)) → 𝐵 ⊆ No
) |
| 25 | | simpl3 1194 |
. . . . 5
⊢ ((((𝐵 ∈ 𝒫 No ∧ ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 𝑦 ≤s 𝑥 ∧ 𝐴 <<s 𝐶) ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐶 ∧ 𝑐 ≤s 𝑏)) → 𝑏 ∈ 𝐵) |
| 26 | 24, 25 | sseldd 3933 |
. . . 4
⊢ ((((𝐵 ∈ 𝒫 No ∧ ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 𝑦 ≤s 𝑥 ∧ 𝐴 <<s 𝐶) ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐶 ∧ 𝑐 ≤s 𝑏)) → 𝑏 ∈ No
) |
| 27 | 15, 17, 21 | ssltsepcd 27728 |
. . . 4
⊢ ((((𝐵 ∈ 𝒫 No ∧ ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 𝑦 ≤s 𝑥 ∧ 𝐴 <<s 𝐶) ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐶 ∧ 𝑐 ≤s 𝑏)) → 𝑎 <s 𝑐) |
| 28 | | simprr 772 |
. . . 4
⊢ ((((𝐵 ∈ 𝒫 No ∧ ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 𝑦 ≤s 𝑥 ∧ 𝐴 <<s 𝐶) ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐶 ∧ 𝑐 ≤s 𝑏)) → 𝑐 ≤s 𝑏) |
| 29 | 18, 22, 26, 27, 28 | sltletrd 27692 |
. . 3
⊢ ((((𝐵 ∈ 𝒫 No ∧ ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 𝑦 ≤s 𝑥 ∧ 𝐴 <<s 𝐶) ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐶 ∧ 𝑐 ≤s 𝑏)) → 𝑎 <s 𝑏) |
| 30 | 14, 29 | rexlimddv 3137 |
. 2
⊢ (((𝐵 ∈ 𝒫 No ∧ ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 𝑦 ≤s 𝑥 ∧ 𝐴 <<s 𝐶) ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → 𝑎 <s 𝑏) |
| 31 | 2, 3, 5, 6, 30 | ssltd 27724 |
1
⊢ ((𝐵 ∈ 𝒫 No ∧ ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 𝑦 ≤s 𝑥 ∧ 𝐴 <<s 𝐶) → 𝐴 <<s 𝐵) |
