| Step | Hyp | Ref
| Expression |
|---|
| 1 | | ssltex1 27767 |
. . 3
⊢ (𝐴 <<s 𝐶 → 𝐴 ∈ V) |
| 2 | 1 | 3ad2ant3 1135 |
. 2
⊢ ((𝐵 ∈ 𝒫 No ∧ ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 𝑦 ≤s 𝑥 ∧ 𝐴 <<s 𝐶) → 𝐴 ∈ V) |
| 3 | | simp1 1136 |
. 2
⊢ ((𝐵 ∈ 𝒫 No ∧ ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 𝑦 ≤s 𝑥 ∧ 𝐴 <<s 𝐶) → 𝐵 ∈ 𝒫 No
) |
| 4 | | ssltss1 27769 |
. . 3
⊢ (𝐴 <<s 𝐶 → 𝐴 ⊆ No
) |
| 5 | 4 | 3ad2ant3 1135 |
. 2
⊢ ((𝐵 ∈ 𝒫 No ∧ ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 𝑦 ≤s 𝑥 ∧ 𝐴 <<s 𝐶) → 𝐴 ⊆ No
) |
| 6 | 3 | elpwid 4589 |
. 2
⊢ ((𝐵 ∈ 𝒫 No ∧ ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 𝑦 ≤s 𝑥 ∧ 𝐴 <<s 𝐶) → 𝐵 ⊆ No
) |
| 7 | | breq2 5127 |
. . . . . 6
⊢ (𝑥 = 𝑏 → (𝑦 ≤s 𝑥 ↔ 𝑦 ≤s 𝑏)) |
| 8 | 7 | rexbidv 3166 |
. . . . 5
⊢ (𝑥 = 𝑏 → (∃𝑦 ∈ 𝐶 𝑦 ≤s 𝑥 ↔ ∃𝑦 ∈ 𝐶 𝑦 ≤s 𝑏)) |
| 9 | | simp12 1204 |
. . . . 5
⊢ (((𝐵 ∈ 𝒫 No ∧ ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 𝑦 ≤s 𝑥 ∧ 𝐴 <<s 𝐶) ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 𝑦 ≤s 𝑥) |
| 10 | | simp3 1138 |
. . . . 5
⊢ (((𝐵 ∈ 𝒫 No ∧ ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 𝑦 ≤s 𝑥 ∧ 𝐴 <<s 𝐶) ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ 𝐵) |
| 11 | 8, 9, 10 | rspcdva 3606 |
. . . 4
⊢ (((𝐵 ∈ 𝒫 No ∧ ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 𝑦 ≤s 𝑥 ∧ 𝐴 <<s 𝐶) ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → ∃𝑦 ∈ 𝐶 𝑦 ≤s 𝑏) |
| 12 | | breq1 5126 |
. . . . 5
⊢ (𝑦 = 𝑐 → (𝑦 ≤s 𝑏 ↔ 𝑐 ≤s 𝑏)) |
| 13 | 12 | cbvrexvw 3224 |
. . . 4
⊢
(∃𝑦 ∈
𝐶 𝑦 ≤s 𝑏 ↔ ∃𝑐 ∈ 𝐶 𝑐 ≤s 𝑏) |
| 14 | 11, 13 | sylib 218 |
. . 3
⊢ (((𝐵 ∈ 𝒫 No ∧ ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 𝑦 ≤s 𝑥 ∧ 𝐴 <<s 𝐶) ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → ∃𝑐 ∈ 𝐶 𝑐 ≤s 𝑏) |
| 15 | | simpl13 1250 |
. . . . . 6
⊢ ((((𝐵 ∈ 𝒫 No ∧ ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 𝑦 ≤s 𝑥 ∧ 𝐴 <<s 𝐶) ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐶 ∧ 𝑐 ≤s 𝑏)) → 𝐴 <<s 𝐶) |
| 16 | 15, 4 | syl 17 |
. . . . 5
⊢ ((((𝐵 ∈ 𝒫 No ∧ ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 𝑦 ≤s 𝑥 ∧ 𝐴 <<s 𝐶) ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐶 ∧ 𝑐 ≤s 𝑏)) → 𝐴 ⊆ No
) |
| 17 | | simpl2 1192 |
. . . . 5
⊢ ((((𝐵 ∈ 𝒫 No ∧ ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 𝑦 ≤s 𝑥 ∧ 𝐴 <<s 𝐶) ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐶 ∧ 𝑐 ≤s 𝑏)) → 𝑎 ∈ 𝐴) |
| 18 | 16, 17 | sseldd 3964 |
. . . 4
⊢ ((((𝐵 ∈ 𝒫 No ∧ ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 𝑦 ≤s 𝑥 ∧ 𝐴 <<s 𝐶) ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐶 ∧ 𝑐 ≤s 𝑏)) → 𝑎 ∈ No
) |
| 19 | | ssltss2 27770 |
. . . . . 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 3964 |
. . . 4
⊢ ((((𝐵 ∈ 𝒫 No ∧ ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 𝑦 ≤s 𝑥 ∧ 𝐴 <<s 𝐶) ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐶 ∧ 𝑐 ≤s 𝑏)) → 𝑐 ∈ No
) |
| 23 | | simpl1 1191 |
. . . . . 6
⊢ ((((𝐵 ∈ 𝒫 No ∧ ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 𝑦 ≤s 𝑥 ∧ 𝐴 <<s 𝐶) ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐶 ∧ 𝑐 ≤s 𝑏)) → (𝐵 ∈ 𝒫 No
∧ ∀𝑥
∈ 𝐵 ∃𝑦 ∈ 𝐶 𝑦 ≤s 𝑥 ∧ 𝐴 <<s 𝐶)) |
| 24 | 23, 6 | syl 17 |
. . . . 5
⊢ ((((𝐵 ∈ 𝒫 No ∧ ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 𝑦 ≤s 𝑥 ∧ 𝐴 <<s 𝐶) ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐶 ∧ 𝑐 ≤s 𝑏)) → 𝐵 ⊆ No
) |
| 25 | | simpl3 1193 |
. . . . 5
⊢ ((((𝐵 ∈ 𝒫 No ∧ ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 𝑦 ≤s 𝑥 ∧ 𝐴 <<s 𝐶) ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐶 ∧ 𝑐 ≤s 𝑏)) → 𝑏 ∈ 𝐵) |
| 26 | 24, 25 | sseldd 3964 |
. . . 4
⊢ ((((𝐵 ∈ 𝒫 No ∧ ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 𝑦 ≤s 𝑥 ∧ 𝐴 <<s 𝐶) ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐶 ∧ 𝑐 ≤s 𝑏)) → 𝑏 ∈ No
) |
| 27 | 15, 17, 21 | ssltsepcd 27775 |
. . . 4
⊢ ((((𝐵 ∈ 𝒫 No ∧ ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 𝑦 ≤s 𝑥 ∧ 𝐴 <<s 𝐶) ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐶 ∧ 𝑐 ≤s 𝑏)) → 𝑎 <s 𝑐) |
| 28 | | simprr 772 |
. . . 4
⊢ ((((𝐵 ∈ 𝒫 No ∧ ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 𝑦 ≤s 𝑥 ∧ 𝐴 <<s 𝐶) ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐶 ∧ 𝑐 ≤s 𝑏)) → 𝑐 ≤s 𝑏) |
| 29 | 18, 22, 26, 27, 28 | sltletrd 27741 |
. . 3
⊢ ((((𝐵 ∈ 𝒫 No ∧ ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 𝑦 ≤s 𝑥 ∧ 𝐴 <<s 𝐶) ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐶 ∧ 𝑐 ≤s 𝑏)) → 𝑎 <s 𝑏) |
| 30 | 14, 29 | rexlimddv 3148 |
. 2
⊢ (((𝐵 ∈ 𝒫 No ∧ ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 𝑦 ≤s 𝑥 ∧ 𝐴 <<s 𝐶) ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → 𝑎 <s 𝑏) |
| 31 | 2, 3, 5, 6, 30 | ssltd 27772 |
1
⊢ ((𝐵 ∈ 𝒫 No ∧ ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 𝑦 ≤s 𝑥 ∧ 𝐴 <<s 𝐶) → 𝐴 <<s 𝐵) |
