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

Theorem wfrlem12OLD 8213
Description: Lemma for well-ordered recursion. Here, we compute the value of the recursive definition generator. Obsolete as of 18-Nov-2024. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by Scott Fenton, 21-Apr-2011.) (Revised by Mario Carneiro, 26-Jun-2015.)
Hypotheses
Ref Expression
wfrfunOLD.1 𝑅 We 𝐴
wfrfunOLD.2 𝑅 Se 𝐴
wfrfunOLD.3 𝐹 = wrecs(𝑅, 𝐴, 𝐺)
Assertion
Ref Expression
wfrlem12OLD (𝑦 ∈ dom 𝐹 → (𝐹𝑦) = (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦))))
Distinct variable groups:   𝑦,𝐴   𝑦,𝐺   𝑦,𝑅
Allowed substitution hint:   𝐹(𝑦)

Proof of Theorem wfrlem12OLD
Dummy variables 𝑓 𝑥 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 vex 3445 . . 3 𝑦 ∈ V
21eldm2 5837 . 2 (𝑦 ∈ dom 𝐹 ↔ ∃𝑧𝑦, 𝑧⟩ ∈ 𝐹)
3 wfrfunOLD.3 . . . . . . 7 𝐹 = wrecs(𝑅, 𝐴, 𝐺)
4 dfwrecsOLD 8191 . . . . . . 7 wrecs(𝑅, 𝐴, 𝐺) = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}
53, 4eqtri 2764 . . . . . 6 𝐹 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}
65eleq2i 2828 . . . . 5 (⟨𝑦, 𝑧⟩ ∈ 𝐹 ↔ ⟨𝑦, 𝑧⟩ ∈ {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))})
7 eluniab 4866 . . . . 5 (⟨𝑦, 𝑧⟩ ∈ {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} ↔ ∃𝑓(⟨𝑦, 𝑧⟩ ∈ 𝑓 ∧ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))))
86, 7bitri 274 . . . 4 (⟨𝑦, 𝑧⟩ ∈ 𝐹 ↔ ∃𝑓(⟨𝑦, 𝑧⟩ ∈ 𝑓 ∧ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))))
9 abid 2717 . . . . . . . 8 (𝑓 ∈ {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} ↔ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))))
10 elssuni 4884 . . . . . . . . 9 (𝑓 ∈ {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} → 𝑓 {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))})
1110, 5sseqtrrdi 3982 . . . . . . . 8 (𝑓 ∈ {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} → 𝑓𝐹)
129, 11sylbir 234 . . . . . . 7 (∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))) → 𝑓𝐹)
13 fnop 6588 . . . . . . . . . . 11 ((𝑓 Fn 𝑥 ∧ ⟨𝑦, 𝑧⟩ ∈ 𝑓) → 𝑦𝑥)
1413ex 413 . . . . . . . . . 10 (𝑓 Fn 𝑥 → (⟨𝑦, 𝑧⟩ ∈ 𝑓𝑦𝑥))
15 rsp 3226 . . . . . . . . . . . . . . 15 (∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))) → (𝑦𝑥 → (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))))
1615impcom 408 . . . . . . . . . . . . . 14 ((𝑦𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))) → (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))
17 rsp 3226 . . . . . . . . . . . . . . . . 17 (∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥 → (𝑦𝑥 → Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥))
18 fndm 6582 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑓 Fn 𝑥 → dom 𝑓 = 𝑥)
1918sseq2d 3963 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑓 Fn 𝑥 → (Pred(𝑅, 𝐴, 𝑦) ⊆ dom 𝑓 ↔ Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥))
2018eleq2d 2822 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑓 Fn 𝑥 → (𝑦 ∈ dom 𝑓𝑦𝑥))
2119, 20anbi12d 631 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓 Fn 𝑥 → ((Pred(𝑅, 𝐴, 𝑦) ⊆ dom 𝑓𝑦 ∈ dom 𝑓) ↔ (Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥𝑦𝑥)))
2221biimprd 247 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓 Fn 𝑥 → ((Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥𝑦𝑥) → (Pred(𝑅, 𝐴, 𝑦) ⊆ dom 𝑓𝑦 ∈ dom 𝑓)))
2322expd 416 . . . . . . . . . . . . . . . . . . . . 21 (𝑓 Fn 𝑥 → (Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥 → (𝑦𝑥 → (Pred(𝑅, 𝐴, 𝑦) ⊆ dom 𝑓𝑦 ∈ dom 𝑓))))
2423impcom 408 . . . . . . . . . . . . . . . . . . . 20 ((Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥𝑓 Fn 𝑥) → (𝑦𝑥 → (Pred(𝑅, 𝐴, 𝑦) ⊆ dom 𝑓𝑦 ∈ dom 𝑓)))
25 wfrfunOLD.1 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑅 We 𝐴
26 wfrfunOLD.2 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑅 Se 𝐴
2725, 26, 3wfrfunOLD 8212 . . . . . . . . . . . . . . . . . . . . . . 23 Fun 𝐹
28 funssfv 6840 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((Fun 𝐹𝑓𝐹𝑦 ∈ dom 𝑓) → (𝐹𝑦) = (𝑓𝑦))
29283adant3l 1179 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((Fun 𝐹𝑓𝐹 ∧ (Pred(𝑅, 𝐴, 𝑦) ⊆ dom 𝑓𝑦 ∈ dom 𝑓)) → (𝐹𝑦) = (𝑓𝑦))
30 fun2ssres 6523 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((Fun 𝐹𝑓𝐹 ∧ Pred(𝑅, 𝐴, 𝑦) ⊆ dom 𝑓) → (𝐹 ↾ Pred(𝑅, 𝐴, 𝑦)) = (𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))
31303adant3r 1180 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((Fun 𝐹𝑓𝐹 ∧ (Pred(𝑅, 𝐴, 𝑦) ⊆ dom 𝑓𝑦 ∈ dom 𝑓)) → (𝐹 ↾ Pred(𝑅, 𝐴, 𝑦)) = (𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))
3231fveq2d 6823 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((Fun 𝐹𝑓𝐹 ∧ (Pred(𝑅, 𝐴, 𝑦) ⊆ dom 𝑓𝑦 ∈ dom 𝑓)) → (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦))) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))
3329, 32eqeq12d 2752 . . . . . . . . . . . . . . . . . . . . . . . 24 ((Fun 𝐹𝑓𝐹 ∧ (Pred(𝑅, 𝐴, 𝑦) ⊆ dom 𝑓𝑦 ∈ dom 𝑓)) → ((𝐹𝑦) = (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦))) ↔ (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))))
3433biimprd 247 . . . . . . . . . . . . . . . . . . . . . . 23 ((Fun 𝐹𝑓𝐹 ∧ (Pred(𝑅, 𝐴, 𝑦) ⊆ dom 𝑓𝑦 ∈ dom 𝑓)) → ((𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))) → (𝐹𝑦) = (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦)))))
3527, 34mp3an1 1447 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑓𝐹 ∧ (Pred(𝑅, 𝐴, 𝑦) ⊆ dom 𝑓𝑦 ∈ dom 𝑓)) → ((𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))) → (𝐹𝑦) = (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦)))))
3635expcom 414 . . . . . . . . . . . . . . . . . . . . 21 ((Pred(𝑅, 𝐴, 𝑦) ⊆ dom 𝑓𝑦 ∈ dom 𝑓) → (𝑓𝐹 → ((𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))) → (𝐹𝑦) = (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦))))))
3736com23 86 . . . . . . . . . . . . . . . . . . . 20 ((Pred(𝑅, 𝐴, 𝑦) ⊆ dom 𝑓𝑦 ∈ dom 𝑓) → ((𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))) → (𝑓𝐹 → (𝐹𝑦) = (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦))))))
3824, 37syl6com 37 . . . . . . . . . . . . . . . . . . 19 (𝑦𝑥 → ((Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥𝑓 Fn 𝑥) → ((𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))) → (𝑓𝐹 → (𝐹𝑦) = (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦)))))))
3938expd 416 . . . . . . . . . . . . . . . . . 18 (𝑦𝑥 → (Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥 → (𝑓 Fn 𝑥 → ((𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))) → (𝑓𝐹 → (𝐹𝑦) = (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦))))))))
4039com34 91 . . . . . . . . . . . . . . . . 17 (𝑦𝑥 → (Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥 → ((𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))) → (𝑓 Fn 𝑥 → (𝑓𝐹 → (𝐹𝑦) = (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦))))))))
4117, 40sylcom 30 . . . . . . . . . . . . . . . 16 (∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥 → (𝑦𝑥 → ((𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))) → (𝑓 Fn 𝑥 → (𝑓𝐹 → (𝐹𝑦) = (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦))))))))
4241adantl 482 . . . . . . . . . . . . . . 15 ((𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) → (𝑦𝑥 → ((𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))) → (𝑓 Fn 𝑥 → (𝑓𝐹 → (𝐹𝑦) = (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦))))))))
4342com14 96 . . . . . . . . . . . . . 14 (𝑓 Fn 𝑥 → (𝑦𝑥 → ((𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))) → ((𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) → (𝑓𝐹 → (𝐹𝑦) = (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦))))))))
4416, 43syl7 74 . . . . . . . . . . . . 13 (𝑓 Fn 𝑥 → (𝑦𝑥 → ((𝑦𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))) → ((𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) → (𝑓𝐹 → (𝐹𝑦) = (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦))))))))
4544exp4a 432 . . . . . . . . . . . 12 (𝑓 Fn 𝑥 → (𝑦𝑥 → (𝑦𝑥 → (∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))) → ((𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) → (𝑓𝐹 → (𝐹𝑦) = (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦)))))))))
4645pm2.43d 53 . . . . . . . . . . 11 (𝑓 Fn 𝑥 → (𝑦𝑥 → (∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))) → ((𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) → (𝑓𝐹 → (𝐹𝑦) = (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦))))))))
4746com34 91 . . . . . . . . . 10 (𝑓 Fn 𝑥 → (𝑦𝑥 → ((𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) → (∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))) → (𝑓𝐹 → (𝐹𝑦) = (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦))))))))
4814, 47syldc 48 . . . . . . . . 9 (⟨𝑦, 𝑧⟩ ∈ 𝑓 → (𝑓 Fn 𝑥 → ((𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) → (∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))) → (𝑓𝐹 → (𝐹𝑦) = (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦))))))))
49483impd 1347 . . . . . . . 8 (⟨𝑦, 𝑧⟩ ∈ 𝑓 → ((𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))) → (𝑓𝐹 → (𝐹𝑦) = (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦))))))
5049exlimdv 1935 . . . . . . 7 (⟨𝑦, 𝑧⟩ ∈ 𝑓 → (∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))) → (𝑓𝐹 → (𝐹𝑦) = (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦))))))
5112, 50mpdi 45 . . . . . 6 (⟨𝑦, 𝑧⟩ ∈ 𝑓 → (∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))) → (𝐹𝑦) = (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦)))))
5251imp 407 . . . . 5 ((⟨𝑦, 𝑧⟩ ∈ 𝑓 ∧ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))) → (𝐹𝑦) = (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦))))
5352exlimiv 1932 . . . 4 (∃𝑓(⟨𝑦, 𝑧⟩ ∈ 𝑓 ∧ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))) → (𝐹𝑦) = (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦))))
548, 53sylbi 216 . . 3 (⟨𝑦, 𝑧⟩ ∈ 𝐹 → (𝐹𝑦) = (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦))))
5554exlimiv 1932 . 2 (∃𝑧𝑦, 𝑧⟩ ∈ 𝐹 → (𝐹𝑦) = (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦))))
562, 55sylbi 216 1 (𝑦 ∈ dom 𝐹 → (𝐹𝑦) = (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1086   = wceq 1540  wex 1780  wcel 2105  {cab 2713  wral 3061  wss 3897  cop 4578   cuni 4851   Se wse 5567   We wwe 5568  dom cdm 5614  cres 5616  Predcpred 6231  Fun wfun 6467   Fn wfn 6468  cfv 6473  wrecscwrecs 8189
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-sep 5240  ax-nul 5247  ax-pr 5369  ax-un 7642
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3404  df-v 3443  df-sbc 3727  df-csb 3843  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4269  df-if 4473  df-pw 4548  df-sn 4573  df-pr 4575  df-op 4579  df-uni 4852  df-iun 4940  df-br 5090  df-opab 5152  df-mpt 5173  df-id 5512  df-po 5526  df-so 5527  df-fr 5569  df-se 5570  df-we 5571  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627  df-pred 6232  df-iota 6425  df-fun 6475  df-fn 6476  df-f 6477  df-fo 6479  df-fv 6481  df-ov 7332  df-2nd 7892  df-frecs 8159  df-wrecs 8190
This theorem is referenced by:  wfrlem14OLD  8215  wfr2aOLD  8219
  Copyright terms: Public domain W3C validator