Description: Obsolete proof of wfr1 as of 18-Nov-2024. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by Scott Fenton, 22-Apr-2011) (Revised by Mario Carneiro, 26-Jun-2015)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | wfr1OLD.1 | ⊢ 𝑅 We 𝐴 | |
| wfr1OLD.2 | ⊢ 𝑅 Se 𝐴 | ||
| wfr1OLD.3 | ⊢ 𝐹 = wrecs ( 𝑅 , 𝐴 , 𝐺 ) | ||
| Assertion | wfr1OLD | ⊢ 𝐹 Fn 𝐴 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | wfr1OLD.1 | ⊢ 𝑅 We 𝐴 | |
| 2 | wfr1OLD.2 | ⊢ 𝑅 Se 𝐴 | |
| 3 | wfr1OLD.3 | ⊢ 𝐹 = wrecs ( 𝑅 , 𝐴 , 𝐺 ) | |
| 4 | 1 2 3 | wfrfunOLD | ⊢ Fun 𝐹 |
| 5 | eqid | ⊢ ( 𝐹 ∪ { ⟨ 𝑧 , ( 𝐺 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } ) = ( 𝐹 ∪ { ⟨ 𝑧 , ( 𝐺 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } ) | |
| 6 | 1 2 3 5 | wfrlem16OLD | ⊢ dom 𝐹 = 𝐴 |
| 7 | df-fn | ⊢ ( 𝐹 Fn 𝐴 ↔ ( Fun 𝐹 ∧ dom 𝐹 = 𝐴 ) ) | |
| 8 | 4 6 7 | mpbir2an | ⊢ 𝐹 Fn 𝐴 |