Step | Hyp | Ref
| Expression |
1 | | cutlt.2 |
. 2
⊢ (𝜑 → 𝐴 = (𝐿 |s 𝑅)) |
2 | | cutlt.1 |
. . 3
⊢ (𝜑 → 𝐿 <<s 𝑅) |
3 | | ssltss1 27635 |
. . . . . . 7
⊢ (𝐿 <<s 𝑅 → 𝐿 ⊆ No
) |
4 | 2, 3 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐿 ⊆ No
) |
5 | | cutlt.3 |
. . . . . 6
⊢ (𝜑 → 𝑋 ∈ 𝐿) |
6 | 4, 5 | sseldd 3983 |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ No
) |
7 | | snelpwi 5443 |
. . . . 5
⊢ (𝑋 ∈
No → {𝑋}
∈ 𝒫 No ) |
8 | 6, 7 | syl 17 |
. . . 4
⊢ (𝜑 → {𝑋} ∈ 𝒫 No
) |
9 | | ssltex1 27633 |
. . . . . 6
⊢ (𝐿 <<s 𝑅 → 𝐿 ∈ V) |
10 | | rabexg 5331 |
. . . . . 6
⊢ (𝐿 ∈ V → {𝑦 ∈ 𝐿 ∣ 𝑋 <s 𝑦} ∈ V) |
11 | 2, 9, 10 | 3syl 18 |
. . . . 5
⊢ (𝜑 → {𝑦 ∈ 𝐿 ∣ 𝑋 <s 𝑦} ∈ V) |
12 | | ssrab2 4077 |
. . . . . 6
⊢ {𝑦 ∈ 𝐿 ∣ 𝑋 <s 𝑦} ⊆ 𝐿 |
13 | 12, 4 | sstrid 3993 |
. . . . 5
⊢ (𝜑 → {𝑦 ∈ 𝐿 ∣ 𝑋 <s 𝑦} ⊆ No
) |
14 | 11, 13 | elpwd 4608 |
. . . 4
⊢ (𝜑 → {𝑦 ∈ 𝐿 ∣ 𝑋 <s 𝑦} ∈ 𝒫 No
) |
15 | | pwuncl 7761 |
. . . 4
⊢ (({𝑋} ∈ 𝒫 No ∧ {𝑦 ∈ 𝐿 ∣ 𝑋 <s 𝑦} ∈ 𝒫 No
) → ({𝑋} ∪
{𝑦 ∈ 𝐿 ∣ 𝑋 <s 𝑦}) ∈ 𝒫 No
) |
16 | 8, 14, 15 | syl2anc 583 |
. . 3
⊢ (𝜑 → ({𝑋} ∪ {𝑦 ∈ 𝐿 ∣ 𝑋 <s 𝑦}) ∈ 𝒫 No
) |
17 | | ssltex2 27634 |
. . . . 5
⊢ (𝐿 <<s 𝑅 → 𝑅 ∈ V) |
18 | 2, 17 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑅 ∈ V) |
19 | | ssltss2 27636 |
. . . . 5
⊢ (𝐿 <<s 𝑅 → 𝑅 ⊆ No
) |
20 | 2, 19 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑅 ⊆ No
) |
21 | 18, 20 | elpwd 4608 |
. . 3
⊢ (𝜑 → 𝑅 ∈ 𝒫 No
) |
22 | | snidg 4662 |
. . . . . . . . 9
⊢ (𝑋 ∈ 𝐿 → 𝑋 ∈ {𝑋}) |
23 | | elun1 4176 |
. . . . . . . . 9
⊢ (𝑋 ∈ {𝑋} → 𝑋 ∈ ({𝑋} ∪ {𝑦 ∈ 𝐿 ∣ 𝑋 <s 𝑦})) |
24 | 5, 22, 23 | 3syl 18 |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ∈ ({𝑋} ∪ {𝑦 ∈ 𝐿 ∣ 𝑋 <s 𝑦})) |
25 | 24 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐿) → 𝑋 ∈ ({𝑋} ∪ {𝑦 ∈ 𝐿 ∣ 𝑋 <s 𝑦})) |
26 | | breq2 5152 |
. . . . . . . 8
⊢ (𝑏 = 𝑋 → (𝑎 ≤s 𝑏 ↔ 𝑎 ≤s 𝑋)) |
27 | 26 | rspcev 3612 |
. . . . . . 7
⊢ ((𝑋 ∈ ({𝑋} ∪ {𝑦 ∈ 𝐿 ∣ 𝑋 <s 𝑦}) ∧ 𝑎 ≤s 𝑋) → ∃𝑏 ∈ ({𝑋} ∪ {𝑦 ∈ 𝐿 ∣ 𝑋 <s 𝑦})𝑎 ≤s 𝑏) |
28 | 25, 27 | sylan 579 |
. . . . . 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 27600 |
. . . . . . 7
⊢ ((𝑋 ∈
No ∧ 𝑎 ∈
No ) → (𝑋 <s 𝑎 ↔ ¬ 𝑎 ≤s 𝑋)) |
33 | 30, 31, 32 | syl2anc 583 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐿) → (𝑋 <s 𝑎 ↔ ¬ 𝑎 ≤s 𝑋)) |
34 | | breq2 5152 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑎 → (𝑋 <s 𝑦 ↔ 𝑋 <s 𝑎)) |
35 | 34 | elrab 3683 |
. . . . . . . . 9
⊢ (𝑎 ∈ {𝑦 ∈ 𝐿 ∣ 𝑋 <s 𝑦} ↔ (𝑎 ∈ 𝐿 ∧ 𝑋 <s 𝑎)) |
36 | | elun2 4177 |
. . . . . . . . 9
⊢ (𝑎 ∈ {𝑦 ∈ 𝐿 ∣ 𝑋 <s 𝑦} → 𝑎 ∈ ({𝑋} ∪ {𝑦 ∈ 𝐿 ∣ 𝑋 <s 𝑦})) |
37 | 35, 36 | sylbir 234 |
. . . . . . . 8
⊢ ((𝑎 ∈ 𝐿 ∧ 𝑋 <s 𝑎) → 𝑎 ∈ ({𝑋} ∪ {𝑦 ∈ 𝐿 ∣ 𝑋 <s 𝑦})) |
38 | | slerflex 27610 |
. . . . . . . . . 10
⊢ (𝑎 ∈
No → 𝑎 ≤s
𝑎) |
39 | 31, 38 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐿) → 𝑎 ≤s 𝑎) |
40 | 39 | adantrr 714 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐿 ∧ 𝑋 <s 𝑎)) → 𝑎 ≤s 𝑎) |
41 | | breq2 5152 |
. . . . . . . . 9
⊢ (𝑏 = 𝑎 → (𝑎 ≤s 𝑏 ↔ 𝑎 ≤s 𝑎)) |
42 | 41 | rspcev 3612 |
. . . . . . . 8
⊢ ((𝑎 ∈ ({𝑋} ∪ {𝑦 ∈ 𝐿 ∣ 𝑋 <s 𝑦}) ∧ 𝑎 ≤s 𝑎) → ∃𝑏 ∈ ({𝑋} ∪ {𝑦 ∈ 𝐿 ∣ 𝑋 <s 𝑦})𝑎 ≤s 𝑏) |
43 | 37, 40, 42 | syl2an2 683 |
. . . . . . 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 4005 |
. . . 4
⊢ (𝜑 → 𝑅 ⊆ 𝑅) |
49 | 20, 48 | coiniss 27765 |
. . 3
⊢ (𝜑 → ∀𝑎 ∈ 𝑅 ∃𝑏 ∈ 𝑅 𝑏 ≤s 𝑎) |
50 | 5 | snssd 4812 |
. . . . 5
⊢ (𝜑 → {𝑋} ⊆ 𝐿) |
51 | 12 | a1i 11 |
. . . . 5
⊢ (𝜑 → {𝑦 ∈ 𝐿 ∣ 𝑋 <s 𝑦} ⊆ 𝐿) |
52 | 50, 51 | unssd 4186 |
. . . 4
⊢ (𝜑 → ({𝑋} ∪ {𝑦 ∈ 𝐿 ∣ 𝑋 <s 𝑦}) ⊆ 𝐿) |
53 | 4, 52 | cofss 27764 |
. . 3
⊢ (𝜑 → ∀𝑎 ∈ ({𝑋} ∪ {𝑦 ∈ 𝐿 ∣ 𝑋 <s 𝑦})∃𝑏 ∈ 𝐿 𝑎 ≤s 𝑏) |
54 | 2, 16, 21, 47, 49, 53, 49 | cofcut2d 27757 |
. 2
⊢ (𝜑 → (𝐿 |s 𝑅) = (({𝑋} ∪ {𝑦 ∈ 𝐿 ∣ 𝑋 <s 𝑦}) |s 𝑅)) |
55 | 1, 54 | eqtrd 2771 |
1
⊢ (𝜑 → 𝐴 = (({𝑋} ∪ {𝑦 ∈ 𝐿 ∣ 𝑋 <s 𝑦}) |s 𝑅)) |