Description: Obsolete version of wfr2 as of 18-Nov-2024. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by Scott Fenton, 18-Apr-2011) (Revised by Mario Carneiro, 26-Jun-2015)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | wfr2OLD.1 | ⊢ 𝑅 We 𝐴 | |
| wfr2OLD.2 | ⊢ 𝑅 Se 𝐴 | ||
| wfr2OLD.3 | ⊢ 𝐹 = wrecs ( 𝑅 , 𝐴 , 𝐺 ) | ||
| Assertion | wfr2OLD | ⊢ ( 𝑋 ∈ 𝐴 → ( 𝐹 ‘ 𝑋 ) = ( 𝐺 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | wfr2OLD.1 | ⊢ 𝑅 We 𝐴 | |
| 2 | wfr2OLD.2 | ⊢ 𝑅 Se 𝐴 | |
| 3 | wfr2OLD.3 | ⊢ 𝐹 = wrecs ( 𝑅 , 𝐴 , 𝐺 ) | |
| 4 | eqid | ⊢ ( 𝐹 ∪ { ⟨ 𝑥 , ( 𝐺 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑥 ) ) ) ⟩ } ) = ( 𝐹 ∪ { ⟨ 𝑥 , ( 𝐺 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑥 ) ) ) ⟩ } ) | |
| 5 | 1 2 3 4 | wfrlem16OLD | ⊢ dom 𝐹 = 𝐴 |
| 6 | 5 | eleq2i | ⊢ ( 𝑋 ∈ dom 𝐹 ↔ 𝑋 ∈ 𝐴 ) |
| 7 | 1 2 3 | wfr2aOLD | ⊢ ( 𝑋 ∈ dom 𝐹 → ( 𝐹 ‘ 𝑋 ) = ( 𝐺 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ) ) |
| 8 | 6 7 | sylbir | ⊢ ( 𝑋 ∈ 𝐴 → ( 𝐹 ‘ 𝑋 ) = ( 𝐺 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ) ) |