| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | wfrlem10OLD.2 | . . . 4
⊢ 𝐹 = wrecs(𝑅, 𝐴, 𝐺) | 
| 2 | 1 | wfrlem8OLD 8357 | . . 3
⊢
(Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅ ↔ Pred(𝑅, 𝐴, 𝑧) = Pred(𝑅, dom 𝐹, 𝑧)) | 
| 3 | 2 | biimpi 216 | . 2
⊢
(Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅ → Pred(𝑅, 𝐴, 𝑧) = Pred(𝑅, dom 𝐹, 𝑧)) | 
| 4 |  | predss 6328 | . . . 4
⊢
Pred(𝑅, dom 𝐹, 𝑧) ⊆ dom 𝐹 | 
| 5 | 4 | a1i 11 | . . 3
⊢ (𝑧 ∈ (𝐴 ∖ dom 𝐹) → Pred(𝑅, dom 𝐹, 𝑧) ⊆ dom 𝐹) | 
| 6 |  | simpr 484 | . . . 4
⊢ ((𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ 𝑤 ∈ dom 𝐹) → 𝑤 ∈ dom 𝐹) | 
| 7 |  | eldifn 4131 | . . . . . . . 8
⊢ (𝑧 ∈ (𝐴 ∖ dom 𝐹) → ¬ 𝑧 ∈ dom 𝐹) | 
| 8 |  | eleq1w 2823 | . . . . . . . . 9
⊢ (𝑤 = 𝑧 → (𝑤 ∈ dom 𝐹 ↔ 𝑧 ∈ dom 𝐹)) | 
| 9 | 8 | notbid 318 | . . . . . . . 8
⊢ (𝑤 = 𝑧 → (¬ 𝑤 ∈ dom 𝐹 ↔ ¬ 𝑧 ∈ dom 𝐹)) | 
| 10 | 7, 9 | syl5ibrcom 247 | . . . . . . 7
⊢ (𝑧 ∈ (𝐴 ∖ dom 𝐹) → (𝑤 = 𝑧 → ¬ 𝑤 ∈ dom 𝐹)) | 
| 11 | 10 | con2d 134 | . . . . . 6
⊢ (𝑧 ∈ (𝐴 ∖ dom 𝐹) → (𝑤 ∈ dom 𝐹 → ¬ 𝑤 = 𝑧)) | 
| 12 | 11 | imp 406 | . . . . 5
⊢ ((𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ 𝑤 ∈ dom 𝐹) → ¬ 𝑤 = 𝑧) | 
| 13 |  | ssel 3976 | . . . . . . . . 9
⊢
(Pred(𝑅, 𝐴, 𝑤) ⊆ dom 𝐹 → (𝑧 ∈ Pred(𝑅, 𝐴, 𝑤) → 𝑧 ∈ dom 𝐹)) | 
| 14 | 13 | con3d 152 | . . . . . . . 8
⊢
(Pred(𝑅, 𝐴, 𝑤) ⊆ dom 𝐹 → (¬ 𝑧 ∈ dom 𝐹 → ¬ 𝑧 ∈ Pred(𝑅, 𝐴, 𝑤))) | 
| 15 | 7, 14 | syl5com 31 | . . . . . . 7
⊢ (𝑧 ∈ (𝐴 ∖ dom 𝐹) → (Pred(𝑅, 𝐴, 𝑤) ⊆ dom 𝐹 → ¬ 𝑧 ∈ Pred(𝑅, 𝐴, 𝑤))) | 
| 16 | 1 | wfrdmclOLD 8358 | . . . . . . 7
⊢ (𝑤 ∈ dom 𝐹 → Pred(𝑅, 𝐴, 𝑤) ⊆ dom 𝐹) | 
| 17 | 15, 16 | impel 505 | . . . . . 6
⊢ ((𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ 𝑤 ∈ dom 𝐹) → ¬ 𝑧 ∈ Pred(𝑅, 𝐴, 𝑤)) | 
| 18 |  | eldifi 4130 | . . . . . . 7
⊢ (𝑧 ∈ (𝐴 ∖ dom 𝐹) → 𝑧 ∈ 𝐴) | 
| 19 |  | elpredg 6334 | . . . . . . . 8
⊢ ((𝑤 ∈ dom 𝐹 ∧ 𝑧 ∈ 𝐴) → (𝑧 ∈ Pred(𝑅, 𝐴, 𝑤) ↔ 𝑧𝑅𝑤)) | 
| 20 | 19 | ancoms 458 | . . . . . . 7
⊢ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ dom 𝐹) → (𝑧 ∈ Pred(𝑅, 𝐴, 𝑤) ↔ 𝑧𝑅𝑤)) | 
| 21 | 18, 20 | sylan 580 | . . . . . 6
⊢ ((𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ 𝑤 ∈ dom 𝐹) → (𝑧 ∈ Pred(𝑅, 𝐴, 𝑤) ↔ 𝑧𝑅𝑤)) | 
| 22 | 17, 21 | mtbid 324 | . . . . 5
⊢ ((𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ 𝑤 ∈ dom 𝐹) → ¬ 𝑧𝑅𝑤) | 
| 23 | 1 | wfrdmssOLD 8356 | . . . . . . 7
⊢ dom 𝐹 ⊆ 𝐴 | 
| 24 | 23 | sseli 3978 | . . . . . 6
⊢ (𝑤 ∈ dom 𝐹 → 𝑤 ∈ 𝐴) | 
| 25 |  | wfrlem10OLD.1 | . . . . . . . 8
⊢ 𝑅 We 𝐴 | 
| 26 |  | weso 5675 | . . . . . . . 8
⊢ (𝑅 We 𝐴 → 𝑅 Or 𝐴) | 
| 27 | 25, 26 | ax-mp 5 | . . . . . . 7
⊢ 𝑅 Or 𝐴 | 
| 28 |  | solin 5618 | . . . . . . 7
⊢ ((𝑅 Or 𝐴 ∧ (𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → (𝑤𝑅𝑧 ∨ 𝑤 = 𝑧 ∨ 𝑧𝑅𝑤)) | 
| 29 | 27, 28 | mpan 690 | . . . . . 6
⊢ ((𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) → (𝑤𝑅𝑧 ∨ 𝑤 = 𝑧 ∨ 𝑧𝑅𝑤)) | 
| 30 | 24, 18, 29 | syl2anr 597 | . . . . 5
⊢ ((𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ 𝑤 ∈ dom 𝐹) → (𝑤𝑅𝑧 ∨ 𝑤 = 𝑧 ∨ 𝑧𝑅𝑤)) | 
| 31 | 12, 22, 30 | ecase23d 1474 | . . . 4
⊢ ((𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ 𝑤 ∈ dom 𝐹) → 𝑤𝑅𝑧) | 
| 32 |  | vex 3483 | . . . . . 6
⊢ 𝑤 ∈ V | 
| 33 | 32 | elpred 6337 | . . . . 5
⊢ (𝑧 ∈ V → (𝑤 ∈ Pred(𝑅, dom 𝐹, 𝑧) ↔ (𝑤 ∈ dom 𝐹 ∧ 𝑤𝑅𝑧))) | 
| 34 | 33 | elv 3484 | . . . 4
⊢ (𝑤 ∈ Pred(𝑅, dom 𝐹, 𝑧) ↔ (𝑤 ∈ dom 𝐹 ∧ 𝑤𝑅𝑧)) | 
| 35 | 6, 31, 34 | sylanbrc 583 | . . 3
⊢ ((𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ 𝑤 ∈ dom 𝐹) → 𝑤 ∈ Pred(𝑅, dom 𝐹, 𝑧)) | 
| 36 | 5, 35 | eqelssd 4004 | . 2
⊢ (𝑧 ∈ (𝐴 ∖ dom 𝐹) → Pred(𝑅, dom 𝐹, 𝑧) = dom 𝐹) | 
| 37 | 3, 36 | sylan9eqr 2798 | 1
⊢ ((𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅) → Pred(𝑅, 𝐴, 𝑧) = dom 𝐹) |