MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  wfr3g Structured version   Visualization version   GIF version

Theorem wfr3g 7278
Description: Functions defined by well-founded recursion are identical up to relation, domain, and characteristic function. (Contributed by Scott Fenton, 11-Feb-2011.)
Assertion
Ref Expression
wfr3g (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐹 Fn 𝐴 ∧ ∀𝑦𝐴 (𝐹𝑦) = (𝐻‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦)))) ∧ (𝐺 Fn 𝐴 ∧ ∀𝑦𝐴 (𝐺𝑦) = (𝐻‘(𝐺 ↾ Pred(𝑅, 𝐴, 𝑦))))) → 𝐹 = 𝐺)
Distinct variable groups:   𝑦,𝐴   𝑦,𝐹   𝑦,𝐺   𝑦,𝐻   𝑦,𝑅

Proof of Theorem wfr3g
Dummy variables 𝑤 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 r19.26 3045 . . . . . . 7 (∀𝑦𝐴 ((𝐹𝑦) = (𝐻‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦))) ∧ (𝐺𝑦) = (𝐻‘(𝐺 ↾ Pred(𝑅, 𝐴, 𝑦)))) ↔ (∀𝑦𝐴 (𝐹𝑦) = (𝐻‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦))) ∧ ∀𝑦𝐴 (𝐺𝑦) = (𝐻‘(𝐺 ↾ Pred(𝑅, 𝐴, 𝑦)))))
2 fveq2 6088 . . . . . . . . . . . 12 (𝑧 = 𝑤 → (𝐹𝑧) = (𝐹𝑤))
3 fveq2 6088 . . . . . . . . . . . 12 (𝑧 = 𝑤 → (𝐺𝑧) = (𝐺𝑤))
42, 3eqeq12d 2624 . . . . . . . . . . 11 (𝑧 = 𝑤 → ((𝐹𝑧) = (𝐺𝑧) ↔ (𝐹𝑤) = (𝐺𝑤)))
54imbi2d 328 . . . . . . . . . 10 (𝑧 = 𝑤 → ((((𝐹 Fn 𝐴𝐺 Fn 𝐴) ∧ ∀𝑦𝐴 ((𝐹𝑦) = (𝐻‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦))) ∧ (𝐺𝑦) = (𝐻‘(𝐺 ↾ Pred(𝑅, 𝐴, 𝑦))))) → (𝐹𝑧) = (𝐺𝑧)) ↔ (((𝐹 Fn 𝐴𝐺 Fn 𝐴) ∧ ∀𝑦𝐴 ((𝐹𝑦) = (𝐻‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦))) ∧ (𝐺𝑦) = (𝐻‘(𝐺 ↾ Pred(𝑅, 𝐴, 𝑦))))) → (𝐹𝑤) = (𝐺𝑤))))
6 ra4v 3489 . . . . . . . . . . 11 (∀𝑤 ∈ Pred (𝑅, 𝐴, 𝑧)(((𝐹 Fn 𝐴𝐺 Fn 𝐴) ∧ ∀𝑦𝐴 ((𝐹𝑦) = (𝐻‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦))) ∧ (𝐺𝑦) = (𝐻‘(𝐺 ↾ Pred(𝑅, 𝐴, 𝑦))))) → (𝐹𝑤) = (𝐺𝑤)) → (((𝐹 Fn 𝐴𝐺 Fn 𝐴) ∧ ∀𝑦𝐴 ((𝐹𝑦) = (𝐻‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦))) ∧ (𝐺𝑦) = (𝐻‘(𝐺 ↾ Pred(𝑅, 𝐴, 𝑦))))) → ∀𝑤 ∈ Pred (𝑅, 𝐴, 𝑧)(𝐹𝑤) = (𝐺𝑤)))
7 fveq2 6088 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝑧 → (𝐹𝑦) = (𝐹𝑧))
8 predeq3 5587 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = 𝑧 → Pred(𝑅, 𝐴, 𝑦) = Pred(𝑅, 𝐴, 𝑧))
98reseq2d 5304 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 𝑧 → (𝐹 ↾ Pred(𝑅, 𝐴, 𝑦)) = (𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))
109fveq2d 6092 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝑧 → (𝐻‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦))) = (𝐻‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧))))
117, 10eqeq12d 2624 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝑧 → ((𝐹𝑦) = (𝐻‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦))) ↔ (𝐹𝑧) = (𝐻‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))))
12 fveq2 6088 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝑧 → (𝐺𝑦) = (𝐺𝑧))
138reseq2d 5304 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 𝑧 → (𝐺 ↾ Pred(𝑅, 𝐴, 𝑦)) = (𝐺 ↾ Pred(𝑅, 𝐴, 𝑧)))
1413fveq2d 6092 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝑧 → (𝐻‘(𝐺 ↾ Pred(𝑅, 𝐴, 𝑦))) = (𝐻‘(𝐺 ↾ Pred(𝑅, 𝐴, 𝑧))))
1512, 14eqeq12d 2624 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝑧 → ((𝐺𝑦) = (𝐻‘(𝐺 ↾ Pred(𝑅, 𝐴, 𝑦))) ↔ (𝐺𝑧) = (𝐻‘(𝐺 ↾ Pred(𝑅, 𝐴, 𝑧)))))
1611, 15anbi12d 742 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑧 → (((𝐹𝑦) = (𝐻‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦))) ∧ (𝐺𝑦) = (𝐻‘(𝐺 ↾ Pred(𝑅, 𝐴, 𝑦)))) ↔ ((𝐹𝑧) = (𝐻‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧))) ∧ (𝐺𝑧) = (𝐻‘(𝐺 ↾ Pred(𝑅, 𝐴, 𝑧))))))
1716rspcva 3279 . . . . . . . . . . . . . . . 16 ((𝑧𝐴 ∧ ∀𝑦𝐴 ((𝐹𝑦) = (𝐻‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦))) ∧ (𝐺𝑦) = (𝐻‘(𝐺 ↾ Pred(𝑅, 𝐴, 𝑦))))) → ((𝐹𝑧) = (𝐻‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧))) ∧ (𝐺𝑧) = (𝐻‘(𝐺 ↾ Pred(𝑅, 𝐴, 𝑧)))))
18 predss 5590 . . . . . . . . . . . . . . . . . . . . . . 23 Pred(𝑅, 𝐴, 𝑧) ⊆ 𝐴
19 fvreseq 6212 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐹 Fn 𝐴𝐺 Fn 𝐴) ∧ Pred(𝑅, 𝐴, 𝑧) ⊆ 𝐴) → ((𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)) = (𝐺 ↾ Pred(𝑅, 𝐴, 𝑧)) ↔ ∀𝑤 ∈ Pred (𝑅, 𝐴, 𝑧)(𝐹𝑤) = (𝐺𝑤)))
2018, 19mpan2 702 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹 Fn 𝐴𝐺 Fn 𝐴) → ((𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)) = (𝐺 ↾ Pred(𝑅, 𝐴, 𝑧)) ↔ ∀𝑤 ∈ Pred (𝑅, 𝐴, 𝑧)(𝐹𝑤) = (𝐺𝑤)))
2120biimpar 500 . . . . . . . . . . . . . . . . . . . . 21 (((𝐹 Fn 𝐴𝐺 Fn 𝐴) ∧ ∀𝑤 ∈ Pred (𝑅, 𝐴, 𝑧)(𝐹𝑤) = (𝐺𝑤)) → (𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)) = (𝐺 ↾ Pred(𝑅, 𝐴, 𝑧)))
2221eqcomd 2615 . . . . . . . . . . . . . . . . . . . 20 (((𝐹 Fn 𝐴𝐺 Fn 𝐴) ∧ ∀𝑤 ∈ Pred (𝑅, 𝐴, 𝑧)(𝐹𝑤) = (𝐺𝑤)) → (𝐺 ↾ Pred(𝑅, 𝐴, 𝑧)) = (𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))
2322fveq2d 6092 . . . . . . . . . . . . . . . . . . 19 (((𝐹 Fn 𝐴𝐺 Fn 𝐴) ∧ ∀𝑤 ∈ Pred (𝑅, 𝐴, 𝑧)(𝐹𝑤) = (𝐺𝑤)) → (𝐻‘(𝐺 ↾ Pred(𝑅, 𝐴, 𝑧))) = (𝐻‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧))))
24 eqtr3 2630 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐹𝑧) = (𝐻‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧))) ∧ (𝐻‘(𝐺 ↾ Pred(𝑅, 𝐴, 𝑧))) = (𝐻‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))) → (𝐹𝑧) = (𝐻‘(𝐺 ↾ Pred(𝑅, 𝐴, 𝑧))))
2524ancoms 467 . . . . . . . . . . . . . . . . . . . . 21 (((𝐻‘(𝐺 ↾ Pred(𝑅, 𝐴, 𝑧))) = (𝐻‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧))) ∧ (𝐹𝑧) = (𝐻‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))) → (𝐹𝑧) = (𝐻‘(𝐺 ↾ Pred(𝑅, 𝐴, 𝑧))))
26 eqtr3 2630 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐹𝑧) = (𝐻‘(𝐺 ↾ Pred(𝑅, 𝐴, 𝑧))) ∧ (𝐺𝑧) = (𝐻‘(𝐺 ↾ Pred(𝑅, 𝐴, 𝑧)))) → (𝐹𝑧) = (𝐺𝑧))
2726ex 448 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹𝑧) = (𝐻‘(𝐺 ↾ Pred(𝑅, 𝐴, 𝑧))) → ((𝐺𝑧) = (𝐻‘(𝐺 ↾ Pred(𝑅, 𝐴, 𝑧))) → (𝐹𝑧) = (𝐺𝑧)))
2825, 27syl 17 . . . . . . . . . . . . . . . . . . . 20 (((𝐻‘(𝐺 ↾ Pred(𝑅, 𝐴, 𝑧))) = (𝐻‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧))) ∧ (𝐹𝑧) = (𝐻‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))) → ((𝐺𝑧) = (𝐻‘(𝐺 ↾ Pred(𝑅, 𝐴, 𝑧))) → (𝐹𝑧) = (𝐺𝑧)))
2928expimpd 626 . . . . . . . . . . . . . . . . . . 19 ((𝐻‘(𝐺 ↾ Pred(𝑅, 𝐴, 𝑧))) = (𝐻‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧))) → (((𝐹𝑧) = (𝐻‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧))) ∧ (𝐺𝑧) = (𝐻‘(𝐺 ↾ Pred(𝑅, 𝐴, 𝑧)))) → (𝐹𝑧) = (𝐺𝑧)))
3023, 29syl 17 . . . . . . . . . . . . . . . . . 18 (((𝐹 Fn 𝐴𝐺 Fn 𝐴) ∧ ∀𝑤 ∈ Pred (𝑅, 𝐴, 𝑧)(𝐹𝑤) = (𝐺𝑤)) → (((𝐹𝑧) = (𝐻‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧))) ∧ (𝐺𝑧) = (𝐻‘(𝐺 ↾ Pred(𝑅, 𝐴, 𝑧)))) → (𝐹𝑧) = (𝐺𝑧)))
3130com12 32 . . . . . . . . . . . . . . . . 17 (((𝐹𝑧) = (𝐻‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧))) ∧ (𝐺𝑧) = (𝐻‘(𝐺 ↾ Pred(𝑅, 𝐴, 𝑧)))) → (((𝐹 Fn 𝐴𝐺 Fn 𝐴) ∧ ∀𝑤 ∈ Pred (𝑅, 𝐴, 𝑧)(𝐹𝑤) = (𝐺𝑤)) → (𝐹𝑧) = (𝐺𝑧)))
3231expd 450 . . . . . . . . . . . . . . . 16 (((𝐹𝑧) = (𝐻‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧))) ∧ (𝐺𝑧) = (𝐻‘(𝐺 ↾ Pred(𝑅, 𝐴, 𝑧)))) → ((𝐹 Fn 𝐴𝐺 Fn 𝐴) → (∀𝑤 ∈ Pred (𝑅, 𝐴, 𝑧)(𝐹𝑤) = (𝐺𝑤) → (𝐹𝑧) = (𝐺𝑧))))
3317, 32syl 17 . . . . . . . . . . . . . . 15 ((𝑧𝐴 ∧ ∀𝑦𝐴 ((𝐹𝑦) = (𝐻‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦))) ∧ (𝐺𝑦) = (𝐻‘(𝐺 ↾ Pred(𝑅, 𝐴, 𝑦))))) → ((𝐹 Fn 𝐴𝐺 Fn 𝐴) → (∀𝑤 ∈ Pred (𝑅, 𝐴, 𝑧)(𝐹𝑤) = (𝐺𝑤) → (𝐹𝑧) = (𝐺𝑧))))
3433ex 448 . . . . . . . . . . . . . 14 (𝑧𝐴 → (∀𝑦𝐴 ((𝐹𝑦) = (𝐻‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦))) ∧ (𝐺𝑦) = (𝐻‘(𝐺 ↾ Pred(𝑅, 𝐴, 𝑦)))) → ((𝐹 Fn 𝐴𝐺 Fn 𝐴) → (∀𝑤 ∈ Pred (𝑅, 𝐴, 𝑧)(𝐹𝑤) = (𝐺𝑤) → (𝐹𝑧) = (𝐺𝑧)))))
3534com23 83 . . . . . . . . . . . . 13 (𝑧𝐴 → ((𝐹 Fn 𝐴𝐺 Fn 𝐴) → (∀𝑦𝐴 ((𝐹𝑦) = (𝐻‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦))) ∧ (𝐺𝑦) = (𝐻‘(𝐺 ↾ Pred(𝑅, 𝐴, 𝑦)))) → (∀𝑤 ∈ Pred (𝑅, 𝐴, 𝑧)(𝐹𝑤) = (𝐺𝑤) → (𝐹𝑧) = (𝐺𝑧)))))
3635impd 445 . . . . . . . . . . . 12 (𝑧𝐴 → (((𝐹 Fn 𝐴𝐺 Fn 𝐴) ∧ ∀𝑦𝐴 ((𝐹𝑦) = (𝐻‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦))) ∧ (𝐺𝑦) = (𝐻‘(𝐺 ↾ Pred(𝑅, 𝐴, 𝑦))))) → (∀𝑤 ∈ Pred (𝑅, 𝐴, 𝑧)(𝐹𝑤) = (𝐺𝑤) → (𝐹𝑧) = (𝐺𝑧))))
3736a2d 29 . . . . . . . . . . 11 (𝑧𝐴 → ((((𝐹 Fn 𝐴𝐺 Fn 𝐴) ∧ ∀𝑦𝐴 ((𝐹𝑦) = (𝐻‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦))) ∧ (𝐺𝑦) = (𝐻‘(𝐺 ↾ Pred(𝑅, 𝐴, 𝑦))))) → ∀𝑤 ∈ Pred (𝑅, 𝐴, 𝑧)(𝐹𝑤) = (𝐺𝑤)) → (((𝐹 Fn 𝐴𝐺 Fn 𝐴) ∧ ∀𝑦𝐴 ((𝐹𝑦) = (𝐻‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦))) ∧ (𝐺𝑦) = (𝐻‘(𝐺 ↾ Pred(𝑅, 𝐴, 𝑦))))) → (𝐹𝑧) = (𝐺𝑧))))
386, 37syl5 33 . . . . . . . . . 10 (𝑧𝐴 → (∀𝑤 ∈ Pred (𝑅, 𝐴, 𝑧)(((𝐹 Fn 𝐴𝐺 Fn 𝐴) ∧ ∀𝑦𝐴 ((𝐹𝑦) = (𝐻‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦))) ∧ (𝐺𝑦) = (𝐻‘(𝐺 ↾ Pred(𝑅, 𝐴, 𝑦))))) → (𝐹𝑤) = (𝐺𝑤)) → (((𝐹 Fn 𝐴𝐺 Fn 𝐴) ∧ ∀𝑦𝐴 ((𝐹𝑦) = (𝐻‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦))) ∧ (𝐺𝑦) = (𝐻‘(𝐺 ↾ Pred(𝑅, 𝐴, 𝑦))))) → (𝐹𝑧) = (𝐺𝑧))))
395, 38wfis2g 5622 . . . . . . . . 9 ((𝑅 We 𝐴𝑅 Se 𝐴) → ∀𝑧𝐴 (((𝐹 Fn 𝐴𝐺 Fn 𝐴) ∧ ∀𝑦𝐴 ((𝐹𝑦) = (𝐻‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦))) ∧ (𝐺𝑦) = (𝐻‘(𝐺 ↾ Pred(𝑅, 𝐴, 𝑦))))) → (𝐹𝑧) = (𝐺𝑧)))
40 r19.21v 2942 . . . . . . . . 9 (∀𝑧𝐴 (((𝐹 Fn 𝐴𝐺 Fn 𝐴) ∧ ∀𝑦𝐴 ((𝐹𝑦) = (𝐻‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦))) ∧ (𝐺𝑦) = (𝐻‘(𝐺 ↾ Pred(𝑅, 𝐴, 𝑦))))) → (𝐹𝑧) = (𝐺𝑧)) ↔ (((𝐹 Fn 𝐴𝐺 Fn 𝐴) ∧ ∀𝑦𝐴 ((𝐹𝑦) = (𝐻‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦))) ∧ (𝐺𝑦) = (𝐻‘(𝐺 ↾ Pred(𝑅, 𝐴, 𝑦))))) → ∀𝑧𝐴 (𝐹𝑧) = (𝐺𝑧)))
4139, 40sylib 206 . . . . . . . 8 ((𝑅 We 𝐴𝑅 Se 𝐴) → (((𝐹 Fn 𝐴𝐺 Fn 𝐴) ∧ ∀𝑦𝐴 ((𝐹𝑦) = (𝐻‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦))) ∧ (𝐺𝑦) = (𝐻‘(𝐺 ↾ Pred(𝑅, 𝐴, 𝑦))))) → ∀𝑧𝐴 (𝐹𝑧) = (𝐺𝑧)))
4241com12 32 . . . . . . 7 (((𝐹 Fn 𝐴𝐺 Fn 𝐴) ∧ ∀𝑦𝐴 ((𝐹𝑦) = (𝐻‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦))) ∧ (𝐺𝑦) = (𝐻‘(𝐺 ↾ Pred(𝑅, 𝐴, 𝑦))))) → ((𝑅 We 𝐴𝑅 Se 𝐴) → ∀𝑧𝐴 (𝐹𝑧) = (𝐺𝑧)))
431, 42sylan2br 491 . . . . . 6 (((𝐹 Fn 𝐴𝐺 Fn 𝐴) ∧ (∀𝑦𝐴 (𝐹𝑦) = (𝐻‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦))) ∧ ∀𝑦𝐴 (𝐺𝑦) = (𝐻‘(𝐺 ↾ Pred(𝑅, 𝐴, 𝑦))))) → ((𝑅 We 𝐴𝑅 Se 𝐴) → ∀𝑧𝐴 (𝐹𝑧) = (𝐺𝑧)))
4443an4s 864 . . . . 5 (((𝐹 Fn 𝐴 ∧ ∀𝑦𝐴 (𝐹𝑦) = (𝐻‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦)))) ∧ (𝐺 Fn 𝐴 ∧ ∀𝑦𝐴 (𝐺𝑦) = (𝐻‘(𝐺 ↾ Pred(𝑅, 𝐴, 𝑦))))) → ((𝑅 We 𝐴𝑅 Se 𝐴) → ∀𝑧𝐴 (𝐹𝑧) = (𝐺𝑧)))
4544com12 32 . . . 4 ((𝑅 We 𝐴𝑅 Se 𝐴) → (((𝐹 Fn 𝐴 ∧ ∀𝑦𝐴 (𝐹𝑦) = (𝐻‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦)))) ∧ (𝐺 Fn 𝐴 ∧ ∀𝑦𝐴 (𝐺𝑦) = (𝐻‘(𝐺 ↾ Pred(𝑅, 𝐴, 𝑦))))) → ∀𝑧𝐴 (𝐹𝑧) = (𝐺𝑧)))
46453impib 1253 . . 3 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐹 Fn 𝐴 ∧ ∀𝑦𝐴 (𝐹𝑦) = (𝐻‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦)))) ∧ (𝐺 Fn 𝐴 ∧ ∀𝑦𝐴 (𝐺𝑦) = (𝐻‘(𝐺 ↾ Pred(𝑅, 𝐴, 𝑦))))) → ∀𝑧𝐴 (𝐹𝑧) = (𝐺𝑧))
47 eqid 2609 . . 3 𝐴 = 𝐴
4846, 47jctil 557 . 2 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐹 Fn 𝐴 ∧ ∀𝑦𝐴 (𝐹𝑦) = (𝐻‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦)))) ∧ (𝐺 Fn 𝐴 ∧ ∀𝑦𝐴 (𝐺𝑦) = (𝐻‘(𝐺 ↾ Pred(𝑅, 𝐴, 𝑦))))) → (𝐴 = 𝐴 ∧ ∀𝑧𝐴 (𝐹𝑧) = (𝐺𝑧)))
49 eqfnfv2 6205 . . . 4 ((𝐹 Fn 𝐴𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ (𝐴 = 𝐴 ∧ ∀𝑧𝐴 (𝐹𝑧) = (𝐺𝑧))))
5049ad2ant2r 778 . . 3 (((𝐹 Fn 𝐴 ∧ ∀𝑦𝐴 (𝐹𝑦) = (𝐻‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦)))) ∧ (𝐺 Fn 𝐴 ∧ ∀𝑦𝐴 (𝐺𝑦) = (𝐻‘(𝐺 ↾ Pred(𝑅, 𝐴, 𝑦))))) → (𝐹 = 𝐺 ↔ (𝐴 = 𝐴 ∧ ∀𝑧𝐴 (𝐹𝑧) = (𝐺𝑧))))
51503adant1 1071 . 2 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐹 Fn 𝐴 ∧ ∀𝑦𝐴 (𝐹𝑦) = (𝐻‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦)))) ∧ (𝐺 Fn 𝐴 ∧ ∀𝑦𝐴 (𝐺𝑦) = (𝐻‘(𝐺 ↾ Pred(𝑅, 𝐴, 𝑦))))) → (𝐹 = 𝐺 ↔ (𝐴 = 𝐴 ∧ ∀𝑧𝐴 (𝐹𝑧) = (𝐺𝑧))))
5248, 51mpbird 245 1 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐹 Fn 𝐴 ∧ ∀𝑦𝐴 (𝐹𝑦) = (𝐻‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦)))) ∧ (𝐺 Fn 𝐴 ∧ ∀𝑦𝐴 (𝐺𝑦) = (𝐻‘(𝐺 ↾ Pred(𝑅, 𝐴, 𝑦))))) → 𝐹 = 𝐺)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382  w3a 1030   = wceq 1474  wcel 1976  wral 2895  wss 3539   Se wse 4985   We wwe 4986  cres 5030  Predcpred 5582   Fn wfn 5785  cfv 5790
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-sep 4703  ax-nul 4712  ax-pow 4764  ax-pr 4828
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-ral 2900  df-rex 2901  df-reu 2902  df-rmo 2903  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-sn 4125  df-pr 4127  df-op 4131  df-uni 4367  df-br 4578  df-opab 4638  df-mpt 4639  df-id 4943  df-po 4949  df-so 4950  df-fr 4987  df-se 4988  df-we 4989  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-pred 5583  df-iota 5754  df-fun 5792  df-fn 5793  df-fv 5798
This theorem is referenced by:  wfrlem5  7284  wfr3  7300
  Copyright terms: Public domain W3C validator