| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | cutlt.2 | . 2
⊢ (𝜑 → 𝐴 = (𝐿 |s 𝑅)) | 
| 2 |  | cutlt.1 | . . 3
⊢ (𝜑 → 𝐿 <<s 𝑅) | 
| 3 |  | ssltss1 27834 | . . . . . . 7
⊢ (𝐿 <<s 𝑅 → 𝐿 ⊆  No
) | 
| 4 | 2, 3 | syl 17 | . . . . . 6
⊢ (𝜑 → 𝐿 ⊆  No
) | 
| 5 |  | cutlt.3 | . . . . . 6
⊢ (𝜑 → 𝑋 ∈ 𝐿) | 
| 6 | 4, 5 | sseldd 3983 | . . . . 5
⊢ (𝜑 → 𝑋 ∈  No
) | 
| 7 |  | snelpwi 5447 | . . . . 5
⊢ (𝑋 ∈ 
No  → {𝑋}
∈ 𝒫  No ) | 
| 8 | 6, 7 | syl 17 | . . . 4
⊢ (𝜑 → {𝑋} ∈ 𝒫  No
) | 
| 9 |  | ssltex1 27832 | . . . . . 6
⊢ (𝐿 <<s 𝑅 → 𝐿 ∈ V) | 
| 10 |  | rabexg 5336 | . . . . . 6
⊢ (𝐿 ∈ V → {𝑦 ∈ 𝐿 ∣ 𝑋 <s 𝑦} ∈ V) | 
| 11 | 2, 9, 10 | 3syl 18 | . . . . 5
⊢ (𝜑 → {𝑦 ∈ 𝐿 ∣ 𝑋 <s 𝑦} ∈ V) | 
| 12 |  | ssrab2 4079 | . . . . . 6
⊢ {𝑦 ∈ 𝐿 ∣ 𝑋 <s 𝑦} ⊆ 𝐿 | 
| 13 | 12, 4 | sstrid 3994 | . . . . 5
⊢ (𝜑 → {𝑦 ∈ 𝐿 ∣ 𝑋 <s 𝑦} ⊆  No
) | 
| 14 | 11, 13 | elpwd 4605 | . . . 4
⊢ (𝜑 → {𝑦 ∈ 𝐿 ∣ 𝑋 <s 𝑦} ∈ 𝒫  No
) | 
| 15 |  | pwuncl 7791 | . . . 4
⊢ (({𝑋} ∈ 𝒫  No  ∧ {𝑦 ∈ 𝐿 ∣ 𝑋 <s 𝑦} ∈ 𝒫  No
) → ({𝑋} ∪
{𝑦 ∈ 𝐿 ∣ 𝑋 <s 𝑦}) ∈ 𝒫  No
) | 
| 16 | 8, 14, 15 | syl2anc 584 | . . 3
⊢ (𝜑 → ({𝑋} ∪ {𝑦 ∈ 𝐿 ∣ 𝑋 <s 𝑦}) ∈ 𝒫  No
) | 
| 17 |  | ssltex2 27833 | . . . . 5
⊢ (𝐿 <<s 𝑅 → 𝑅 ∈ V) | 
| 18 | 2, 17 | syl 17 | . . . 4
⊢ (𝜑 → 𝑅 ∈ V) | 
| 19 |  | ssltss2 27835 | . . . . 5
⊢ (𝐿 <<s 𝑅 → 𝑅 ⊆  No
) | 
| 20 | 2, 19 | syl 17 | . . . 4
⊢ (𝜑 → 𝑅 ⊆  No
) | 
| 21 | 18, 20 | elpwd 4605 | . . 3
⊢ (𝜑 → 𝑅 ∈ 𝒫  No
) | 
| 22 |  | snidg 4659 | . . . . . . . . 9
⊢ (𝑋 ∈ 𝐿 → 𝑋 ∈ {𝑋}) | 
| 23 |  | elun1 4181 | . . . . . . . . 9
⊢ (𝑋 ∈ {𝑋} → 𝑋 ∈ ({𝑋} ∪ {𝑦 ∈ 𝐿 ∣ 𝑋 <s 𝑦})) | 
| 24 | 5, 22, 23 | 3syl 18 | . . . . . . . 8
⊢ (𝜑 → 𝑋 ∈ ({𝑋} ∪ {𝑦 ∈ 𝐿 ∣ 𝑋 <s 𝑦})) | 
| 25 | 24 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐿) → 𝑋 ∈ ({𝑋} ∪ {𝑦 ∈ 𝐿 ∣ 𝑋 <s 𝑦})) | 
| 26 |  | breq2 5146 | . . . . . . . 8
⊢ (𝑏 = 𝑋 → (𝑎 ≤s 𝑏 ↔ 𝑎 ≤s 𝑋)) | 
| 27 | 26 | rspcev 3621 | . . . . . . 7
⊢ ((𝑋 ∈ ({𝑋} ∪ {𝑦 ∈ 𝐿 ∣ 𝑋 <s 𝑦}) ∧ 𝑎 ≤s 𝑋) → ∃𝑏 ∈ ({𝑋} ∪ {𝑦 ∈ 𝐿 ∣ 𝑋 <s 𝑦})𝑎 ≤s 𝑏) | 
| 28 | 25, 27 | sylan 580 | . . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐿) ∧ 𝑎 ≤s 𝑋) → ∃𝑏 ∈ ({𝑋} ∪ {𝑦 ∈ 𝐿 ∣ 𝑋 <s 𝑦})𝑎 ≤s 𝑏) | 
| 29 | 28 | ex 412 | . . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐿) → (𝑎 ≤s 𝑋 → ∃𝑏 ∈ ({𝑋} ∪ {𝑦 ∈ 𝐿 ∣ 𝑋 <s 𝑦})𝑎 ≤s 𝑏)) | 
| 30 | 6 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐿) → 𝑋 ∈  No
) | 
| 31 | 4 | sselda 3982 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐿) → 𝑎 ∈  No
) | 
| 32 |  | sltnle 27799 | . . . . . . 7
⊢ ((𝑋 ∈ 
No  ∧ 𝑎 ∈
 No ) → (𝑋 <s 𝑎 ↔ ¬ 𝑎 ≤s 𝑋)) | 
| 33 | 30, 31, 32 | syl2anc 584 | . . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐿) → (𝑋 <s 𝑎 ↔ ¬ 𝑎 ≤s 𝑋)) | 
| 34 |  | breq2 5146 | . . . . . . . . . 10
⊢ (𝑦 = 𝑎 → (𝑋 <s 𝑦 ↔ 𝑋 <s 𝑎)) | 
| 35 | 34 | elrab 3691 | . . . . . . . . 9
⊢ (𝑎 ∈ {𝑦 ∈ 𝐿 ∣ 𝑋 <s 𝑦} ↔ (𝑎 ∈ 𝐿 ∧ 𝑋 <s 𝑎)) | 
| 36 |  | elun2 4182 | . . . . . . . . 9
⊢ (𝑎 ∈ {𝑦 ∈ 𝐿 ∣ 𝑋 <s 𝑦} → 𝑎 ∈ ({𝑋} ∪ {𝑦 ∈ 𝐿 ∣ 𝑋 <s 𝑦})) | 
| 37 | 35, 36 | sylbir 235 | . . . . . . . 8
⊢ ((𝑎 ∈ 𝐿 ∧ 𝑋 <s 𝑎) → 𝑎 ∈ ({𝑋} ∪ {𝑦 ∈ 𝐿 ∣ 𝑋 <s 𝑦})) | 
| 38 |  | slerflex 27809 | . . . . . . . . . 10
⊢ (𝑎 ∈ 
No  → 𝑎 ≤s
𝑎) | 
| 39 | 31, 38 | syl 17 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐿) → 𝑎 ≤s 𝑎) | 
| 40 | 39 | adantrr 717 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐿 ∧ 𝑋 <s 𝑎)) → 𝑎 ≤s 𝑎) | 
| 41 |  | breq2 5146 | . . . . . . . . 9
⊢ (𝑏 = 𝑎 → (𝑎 ≤s 𝑏 ↔ 𝑎 ≤s 𝑎)) | 
| 42 | 41 | rspcev 3621 | . . . . . . . 8
⊢ ((𝑎 ∈ ({𝑋} ∪ {𝑦 ∈ 𝐿 ∣ 𝑋 <s 𝑦}) ∧ 𝑎 ≤s 𝑎) → ∃𝑏 ∈ ({𝑋} ∪ {𝑦 ∈ 𝐿 ∣ 𝑋 <s 𝑦})𝑎 ≤s 𝑏) | 
| 43 | 37, 40, 42 | syl2an2 686 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐿 ∧ 𝑋 <s 𝑎)) → ∃𝑏 ∈ ({𝑋} ∪ {𝑦 ∈ 𝐿 ∣ 𝑋 <s 𝑦})𝑎 ≤s 𝑏) | 
| 44 | 43 | expr 456 | . . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐿) → (𝑋 <s 𝑎 → ∃𝑏 ∈ ({𝑋} ∪ {𝑦 ∈ 𝐿 ∣ 𝑋 <s 𝑦})𝑎 ≤s 𝑏)) | 
| 45 | 33, 44 | sylbird 260 | . . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐿) → (¬ 𝑎 ≤s 𝑋 → ∃𝑏 ∈ ({𝑋} ∪ {𝑦 ∈ 𝐿 ∣ 𝑋 <s 𝑦})𝑎 ≤s 𝑏)) | 
| 46 | 29, 45 | pm2.61d 179 | . . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐿) → ∃𝑏 ∈ ({𝑋} ∪ {𝑦 ∈ 𝐿 ∣ 𝑋 <s 𝑦})𝑎 ≤s 𝑏) | 
| 47 | 46 | ralrimiva 3145 | . . 3
⊢ (𝜑 → ∀𝑎 ∈ 𝐿 ∃𝑏 ∈ ({𝑋} ∪ {𝑦 ∈ 𝐿 ∣ 𝑋 <s 𝑦})𝑎 ≤s 𝑏) | 
| 48 |  | ssidd 4006 | . . . 4
⊢ (𝜑 → 𝑅 ⊆ 𝑅) | 
| 49 | 20, 48 | coiniss 27966 | . . 3
⊢ (𝜑 → ∀𝑎 ∈ 𝑅 ∃𝑏 ∈ 𝑅 𝑏 ≤s 𝑎) | 
| 50 | 5 | snssd 4808 | . . . . 5
⊢ (𝜑 → {𝑋} ⊆ 𝐿) | 
| 51 | 12 | a1i 11 | . . . . 5
⊢ (𝜑 → {𝑦 ∈ 𝐿 ∣ 𝑋 <s 𝑦} ⊆ 𝐿) | 
| 52 | 50, 51 | unssd 4191 | . . . 4
⊢ (𝜑 → ({𝑋} ∪ {𝑦 ∈ 𝐿 ∣ 𝑋 <s 𝑦}) ⊆ 𝐿) | 
| 53 | 4, 52 | cofss 27965 | . . 3
⊢ (𝜑 → ∀𝑎 ∈ ({𝑋} ∪ {𝑦 ∈ 𝐿 ∣ 𝑋 <s 𝑦})∃𝑏 ∈ 𝐿 𝑎 ≤s 𝑏) | 
| 54 | 2, 16, 21, 47, 49, 53, 49 | cofcut2d 27958 | . 2
⊢ (𝜑 → (𝐿 |s 𝑅) = (({𝑋} ∪ {𝑦 ∈ 𝐿 ∣ 𝑋 <s 𝑦}) |s 𝑅)) | 
| 55 | 1, 54 | eqtrd 2776 | 1
⊢ (𝜑 → 𝐴 = (({𝑋} ∪ {𝑦 ∈ 𝐿 ∣ 𝑋 <s 𝑦}) |s 𝑅)) |