| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | n0 4353 | . . 3
⊢ (𝐴 ≠ ∅ ↔
∃𝑢 𝑢 ∈ 𝐴) | 
| 2 |  | ltrelsr 11108 | . . . . . . . . . . . . 13
⊢ 
<R ⊆ (R ×
R) | 
| 3 | 2 | brel 5750 | . . . . . . . . . . . 12
⊢ (𝑦 <R
𝑥 → (𝑦 ∈ R ∧
𝑥 ∈
R)) | 
| 4 | 3 | simpld 494 | . . . . . . . . . . 11
⊢ (𝑦 <R
𝑥 → 𝑦 ∈ R) | 
| 5 | 4 | ralimi 3083 | . . . . . . . . . 10
⊢
(∀𝑦 ∈
𝐴 𝑦 <R 𝑥 → ∀𝑦 ∈ 𝐴 𝑦 ∈ R) | 
| 6 |  | dfss3 3972 | . . . . . . . . . 10
⊢ (𝐴 ⊆ R ↔
∀𝑦 ∈ 𝐴 𝑦 ∈ R) | 
| 7 | 5, 6 | sylibr 234 | . . . . . . . . 9
⊢
(∀𝑦 ∈
𝐴 𝑦 <R 𝑥 → 𝐴 ⊆ R) | 
| 8 | 7 | sseld 3982 | . . . . . . . 8
⊢
(∀𝑦 ∈
𝐴 𝑦 <R 𝑥 → (𝑢 ∈ 𝐴 → 𝑢 ∈ R)) | 
| 9 | 8 | rexlimivw 3151 | . . . . . . 7
⊢
(∃𝑥 ∈
R ∀𝑦
∈ 𝐴 𝑦 <R 𝑥 → (𝑢 ∈ 𝐴 → 𝑢 ∈ R)) | 
| 10 | 9 | impcom 407 | . . . . . 6
⊢ ((𝑢 ∈ 𝐴 ∧ ∃𝑥 ∈ R ∀𝑦 ∈ 𝐴 𝑦 <R 𝑥) → 𝑢 ∈ R) | 
| 11 |  | eleq1 2829 | . . . . . . . . 9
⊢ (𝑢 = if(𝑢 ∈ R, 𝑢, 1R) → (𝑢 ∈ 𝐴 ↔ if(𝑢 ∈ R, 𝑢, 1R) ∈ 𝐴)) | 
| 12 | 11 | anbi1d 631 | . . . . . . . 8
⊢ (𝑢 = if(𝑢 ∈ R, 𝑢, 1R) → ((𝑢 ∈ 𝐴 ∧ ∃𝑥 ∈ R ∀𝑦 ∈ 𝐴 𝑦 <R 𝑥) ↔ (if(𝑢 ∈ R, 𝑢, 1R) ∈ 𝐴 ∧ ∃𝑥 ∈ R ∀𝑦 ∈ 𝐴 𝑦 <R 𝑥))) | 
| 13 | 12 | imbi1d 341 | . . . . . . 7
⊢ (𝑢 = if(𝑢 ∈ R, 𝑢, 1R) →
(((𝑢 ∈ 𝐴 ∧ ∃𝑥 ∈ R ∀𝑦 ∈ 𝐴 𝑦 <R 𝑥) → ∃𝑥 ∈ R
(∀𝑦 ∈ 𝐴 ¬ 𝑥 <R 𝑦 ∧ ∀𝑦 ∈ R (𝑦 <R
𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧))) ↔ ((if(𝑢 ∈ R, 𝑢, 1R)
∈ 𝐴 ∧ ∃𝑥 ∈ R
∀𝑦 ∈ 𝐴 𝑦 <R 𝑥) → ∃𝑥 ∈ R
(∀𝑦 ∈ 𝐴 ¬ 𝑥 <R 𝑦 ∧ ∀𝑦 ∈ R (𝑦 <R
𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧))))) | 
| 14 |  | opeq1 4873 | . . . . . . . . . . . 12
⊢ (𝑣 = 𝑤 → 〈𝑣, 1P〉 =
〈𝑤,
1P〉) | 
| 15 | 14 | eceq1d 8785 | . . . . . . . . . . 11
⊢ (𝑣 = 𝑤 → [〈𝑣, 1P〉]
~R = [〈𝑤, 1P〉]
~R ) | 
| 16 | 15 | oveq2d 7447 | . . . . . . . . . 10
⊢ (𝑣 = 𝑤 → (if(𝑢 ∈ R, 𝑢, 1R)
+R [〈𝑣, 1P〉]
~R ) = (if(𝑢 ∈ R, 𝑢, 1R)
+R [〈𝑤, 1P〉]
~R )) | 
| 17 | 16 | eleq1d 2826 | . . . . . . . . 9
⊢ (𝑣 = 𝑤 → ((if(𝑢 ∈ R, 𝑢, 1R)
+R [〈𝑣, 1P〉]
~R ) ∈ 𝐴 ↔ (if(𝑢 ∈ R, 𝑢, 1R)
+R [〈𝑤, 1P〉]
~R ) ∈ 𝐴)) | 
| 18 | 17 | cbvabv 2812 | . . . . . . . 8
⊢ {𝑣 ∣ (if(𝑢 ∈ R, 𝑢, 1R)
+R [〈𝑣, 1P〉]
~R ) ∈ 𝐴} = {𝑤 ∣ (if(𝑢 ∈ R, 𝑢, 1R)
+R [〈𝑤, 1P〉]
~R ) ∈ 𝐴} | 
| 19 |  | 1sr 11121 | . . . . . . . . 9
⊢
1R ∈ R | 
| 20 | 19 | elimel 4595 | . . . . . . . 8
⊢ if(𝑢 ∈ R, 𝑢, 1R)
∈ R | 
| 21 | 18, 20 | supsrlem 11151 | . . . . . . 7
⊢
((if(𝑢 ∈
R, 𝑢,
1R) ∈ 𝐴 ∧ ∃𝑥 ∈ R ∀𝑦 ∈ 𝐴 𝑦 <R 𝑥) → ∃𝑥 ∈ R
(∀𝑦 ∈ 𝐴 ¬ 𝑥 <R 𝑦 ∧ ∀𝑦 ∈ R (𝑦 <R
𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧))) | 
| 22 | 13, 21 | dedth 4584 | . . . . . 6
⊢ (𝑢 ∈ R →
((𝑢 ∈ 𝐴 ∧ ∃𝑥 ∈ R ∀𝑦 ∈ 𝐴 𝑦 <R 𝑥) → ∃𝑥 ∈ R
(∀𝑦 ∈ 𝐴 ¬ 𝑥 <R 𝑦 ∧ ∀𝑦 ∈ R (𝑦 <R
𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧)))) | 
| 23 | 10, 22 | mpcom 38 | . . . . 5
⊢ ((𝑢 ∈ 𝐴 ∧ ∃𝑥 ∈ R ∀𝑦 ∈ 𝐴 𝑦 <R 𝑥) → ∃𝑥 ∈ R
(∀𝑦 ∈ 𝐴 ¬ 𝑥 <R 𝑦 ∧ ∀𝑦 ∈ R (𝑦 <R
𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧))) | 
| 24 | 23 | ex 412 | . . . 4
⊢ (𝑢 ∈ 𝐴 → (∃𝑥 ∈ R ∀𝑦 ∈ 𝐴 𝑦 <R 𝑥 → ∃𝑥 ∈ R
(∀𝑦 ∈ 𝐴 ¬ 𝑥 <R 𝑦 ∧ ∀𝑦 ∈ R (𝑦 <R
𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧)))) | 
| 25 | 24 | exlimiv 1930 | . . 3
⊢
(∃𝑢 𝑢 ∈ 𝐴 → (∃𝑥 ∈ R ∀𝑦 ∈ 𝐴 𝑦 <R 𝑥 → ∃𝑥 ∈ R
(∀𝑦 ∈ 𝐴 ¬ 𝑥 <R 𝑦 ∧ ∀𝑦 ∈ R (𝑦 <R
𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧)))) | 
| 26 | 1, 25 | sylbi 217 | . 2
⊢ (𝐴 ≠ ∅ →
(∃𝑥 ∈
R ∀𝑦
∈ 𝐴 𝑦 <R 𝑥 → ∃𝑥 ∈ R
(∀𝑦 ∈ 𝐴 ¬ 𝑥 <R 𝑦 ∧ ∀𝑦 ∈ R (𝑦 <R
𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧)))) | 
| 27 | 26 | imp 406 | 1
⊢ ((𝐴 ≠ ∅ ∧ ∃𝑥 ∈ R
∀𝑦 ∈ 𝐴 𝑦 <R 𝑥) → ∃𝑥 ∈ R
(∀𝑦 ∈ 𝐴 ¬ 𝑥 <R 𝑦 ∧ ∀𝑦 ∈ R (𝑦 <R
𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧))) |