| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | wfrlem13OLD.3 | . . 3
⊢ 𝐹 = wrecs(𝑅, 𝐴, 𝐺) | 
| 2 | 1 | wfrdmssOLD 8356 | . 2
⊢ dom 𝐹 ⊆ 𝐴 | 
| 3 |  | eldifn 4131 | . . . . . 6
⊢ (𝑧 ∈ (𝐴 ∖ dom 𝐹) → ¬ 𝑧 ∈ dom 𝐹) | 
| 4 |  | ssun2 4178 | . . . . . . . . 9
⊢ {𝑧} ⊆ (dom 𝐹 ∪ {𝑧}) | 
| 5 |  | vsnid 4662 | . . . . . . . . 9
⊢ 𝑧 ∈ {𝑧} | 
| 6 | 4, 5 | sselii 3979 | . . . . . . . 8
⊢ 𝑧 ∈ (dom 𝐹 ∪ {𝑧}) | 
| 7 |  | wfrlem13OLD.4 | . . . . . . . . . 10
⊢ 𝐶 = (𝐹 ∪ {〈𝑧, (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))〉}) | 
| 8 | 7 | dmeqi 5914 | . . . . . . . . 9
⊢ dom 𝐶 = dom (𝐹 ∪ {〈𝑧, (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))〉}) | 
| 9 |  | dmun 5920 | . . . . . . . . 9
⊢ dom
(𝐹 ∪ {〈𝑧, (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))〉}) = (dom 𝐹 ∪ dom {〈𝑧, (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))〉}) | 
| 10 |  | fvex 6918 | . . . . . . . . . . 11
⊢ (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧))) ∈ V | 
| 11 | 10 | dmsnop 6235 | . . . . . . . . . 10
⊢ dom
{〈𝑧, (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))〉} = {𝑧} | 
| 12 | 11 | uneq2i 4164 | . . . . . . . . 9
⊢ (dom
𝐹 ∪ dom {〈𝑧, (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))〉}) = (dom 𝐹 ∪ {𝑧}) | 
| 13 | 8, 9, 12 | 3eqtri 2768 | . . . . . . . 8
⊢ dom 𝐶 = (dom 𝐹 ∪ {𝑧}) | 
| 14 | 6, 13 | eleqtrri 2839 | . . . . . . 7
⊢ 𝑧 ∈ dom 𝐶 | 
| 15 |  | wfrlem13OLD.1 | . . . . . . . . . . . 12
⊢ 𝑅 We 𝐴 | 
| 16 |  | wfrlem13OLD.2 | . . . . . . . . . . . 12
⊢ 𝑅 Se 𝐴 | 
| 17 | 15, 16, 1, 7 | wfrlem15OLD 8364 | . . . . . . . . . . 11
⊢ ((𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅) → 𝐶 ∈ {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}) | 
| 18 |  | elssuni 4936 | . . . . . . . . . . 11
⊢ (𝐶 ∈ {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} → 𝐶 ⊆ ∪ {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}) | 
| 19 | 17, 18 | syl 17 | . . . . . . . . . 10
⊢ ((𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅) → 𝐶 ⊆ ∪ {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}) | 
| 20 |  | dfwrecsOLD 8339 | . . . . . . . . . . 11
⊢
wrecs(𝑅, 𝐴, 𝐺) = ∪ {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} | 
| 21 | 1, 20 | eqtri 2764 | . . . . . . . . . 10
⊢ 𝐹 = ∪
{𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} | 
| 22 | 19, 21 | sseqtrrdi 4024 | . . . . . . . . 9
⊢ ((𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅) → 𝐶 ⊆ 𝐹) | 
| 23 |  | dmss 5912 | . . . . . . . . 9
⊢ (𝐶 ⊆ 𝐹 → dom 𝐶 ⊆ dom 𝐹) | 
| 24 | 22, 23 | syl 17 | . . . . . . . 8
⊢ ((𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅) → dom 𝐶 ⊆ dom 𝐹) | 
| 25 | 24 | sseld 3981 | . . . . . . 7
⊢ ((𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅) → (𝑧 ∈ dom 𝐶 → 𝑧 ∈ dom 𝐹)) | 
| 26 | 14, 25 | mpi 20 | . . . . . 6
⊢ ((𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅) → 𝑧 ∈ dom 𝐹) | 
| 27 | 3, 26 | mtand 815 | . . . . 5
⊢ (𝑧 ∈ (𝐴 ∖ dom 𝐹) → ¬ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅) | 
| 28 | 27 | nrex 3073 | . . . 4
⊢  ¬
∃𝑧 ∈ (𝐴 ∖ dom 𝐹)Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅ | 
| 29 |  | df-ne 2940 | . . . . 5
⊢ ((𝐴 ∖ dom 𝐹) ≠ ∅ ↔ ¬ (𝐴 ∖ dom 𝐹) = ∅) | 
| 30 |  | difss 4135 | . . . . . 6
⊢ (𝐴 ∖ dom 𝐹) ⊆ 𝐴 | 
| 31 | 15, 16 | tz6.26i 6369 | . . . . . 6
⊢ (((𝐴 ∖ dom 𝐹) ⊆ 𝐴 ∧ (𝐴 ∖ dom 𝐹) ≠ ∅) → ∃𝑧 ∈ (𝐴 ∖ dom 𝐹)Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅) | 
| 32 | 30, 31 | mpan 690 | . . . . 5
⊢ ((𝐴 ∖ dom 𝐹) ≠ ∅ → ∃𝑧 ∈ (𝐴 ∖ dom 𝐹)Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅) | 
| 33 | 29, 32 | sylbir 235 | . . . 4
⊢ (¬
(𝐴 ∖ dom 𝐹) = ∅ → ∃𝑧 ∈ (𝐴 ∖ dom 𝐹)Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅) | 
| 34 | 28, 33 | mt3 201 | . . 3
⊢ (𝐴 ∖ dom 𝐹) = ∅ | 
| 35 |  | ssdif0 4365 | . . 3
⊢ (𝐴 ⊆ dom 𝐹 ↔ (𝐴 ∖ dom 𝐹) = ∅) | 
| 36 | 34, 35 | mpbir 231 | . 2
⊢ 𝐴 ⊆ dom 𝐹 | 
| 37 | 2, 36 | eqssi 3999 | 1
⊢ dom 𝐹 = 𝐴 |