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

Theorem wfrlem12 7658
Description: Lemma for well-founded recursion. Here, we compute the value of the recursive definition generator. (Contributed by Scott Fenton, 21-Apr-2011.) (Revised by Mario Carneiro, 26-Jun-2015.)
Hypotheses
Ref Expression
wfrfun.1 𝑅 We 𝐴
wfrfun.2 𝑅 Se 𝐴
wfrfun.3 𝐹 = wrecs(𝑅, 𝐴, 𝐺)
Assertion
Ref Expression
wfrlem12 (𝑦 ∈ dom 𝐹 → (𝐹𝑦) = (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦))))
Distinct variable groups:   𝑦,𝐴   𝑦,𝐺   𝑦,𝑅
Allowed substitution hint:   𝐹(𝑦)

Proof of Theorem wfrlem12
Dummy variables 𝑓 𝑥 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 vex 3394 . . 3 𝑦 ∈ V
21eldm2 5523 . 2 (𝑦 ∈ dom 𝐹 ↔ ∃𝑧𝑦, 𝑧⟩ ∈ 𝐹)
3 wfrfun.3 . . . . . . 7 𝐹 = wrecs(𝑅, 𝐴, 𝐺)
4 df-wrecs 7638 . . . . . . 7 wrecs(𝑅, 𝐴, 𝐺) = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}
53, 4eqtri 2828 . . . . . 6 𝐹 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}
65eleq2i 2877 . . . . 5 (⟨𝑦, 𝑧⟩ ∈ 𝐹 ↔ ⟨𝑦, 𝑧⟩ ∈ {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))})
7 eluniab 4641 . . . . 5 (⟨𝑦, 𝑧⟩ ∈ {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} ↔ ∃𝑓(⟨𝑦, 𝑧⟩ ∈ 𝑓 ∧ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))))
86, 7bitri 266 . . . 4 (⟨𝑦, 𝑧⟩ ∈ 𝐹 ↔ ∃𝑓(⟨𝑦, 𝑧⟩ ∈ 𝑓 ∧ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))))
9 abid 2794 . . . . . . . 8 (𝑓 ∈ {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} ↔ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))))
10 elssuni 4661 . . . . . . . . 9 (𝑓 ∈ {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} → 𝑓 {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))})
1110, 5syl6sseqr 3849 . . . . . . . 8 (𝑓 ∈ {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} → 𝑓𝐹)
129, 11sylbir 226 . . . . . . 7 (∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))) → 𝑓𝐹)
13 fnop 6201 . . . . . . . . . . 11 ((𝑓 Fn 𝑥 ∧ ⟨𝑦, 𝑧⟩ ∈ 𝑓) → 𝑦𝑥)
1413ex 399 . . . . . . . . . 10 (𝑓 Fn 𝑥 → (⟨𝑦, 𝑧⟩ ∈ 𝑓𝑦𝑥))
15 rsp 3117 . . . . . . . . . . . . . . 15 (∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))) → (𝑦𝑥 → (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))))
1615impcom 396 . . . . . . . . . . . . . 14 ((𝑦𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))) → (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))
17 rsp 3117 . . . . . . . . . . . . . . . . 17 (∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥 → (𝑦𝑥 → Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥))
18 fndm 6197 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑓 Fn 𝑥 → dom 𝑓 = 𝑥)
1918sseq2d 3830 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑓 Fn 𝑥 → (Pred(𝑅, 𝐴, 𝑦) ⊆ dom 𝑓 ↔ Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥))
2018eleq2d 2871 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑓 Fn 𝑥 → (𝑦 ∈ dom 𝑓𝑦𝑥))
2119, 20anbi12d 618 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓 Fn 𝑥 → ((Pred(𝑅, 𝐴, 𝑦) ⊆ dom 𝑓𝑦 ∈ dom 𝑓) ↔ (Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥𝑦𝑥)))
2221biimprd 239 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓 Fn 𝑥 → ((Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥𝑦𝑥) → (Pred(𝑅, 𝐴, 𝑦) ⊆ dom 𝑓𝑦 ∈ dom 𝑓)))
2322expd 402 . . . . . . . . . . . . . . . . . . . . 21 (𝑓 Fn 𝑥 → (Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥 → (𝑦𝑥 → (Pred(𝑅, 𝐴, 𝑦) ⊆ dom 𝑓𝑦 ∈ dom 𝑓))))
2423impcom 396 . . . . . . . . . . . . . . . . . . . 20 ((Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥𝑓 Fn 𝑥) → (𝑦𝑥 → (Pred(𝑅, 𝐴, 𝑦) ⊆ dom 𝑓𝑦 ∈ dom 𝑓)))
25 wfrfun.1 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑅 We 𝐴
26 wfrfun.2 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑅 Se 𝐴
2725, 26, 3wfrfun 7657 . . . . . . . . . . . . . . . . . . . . . . 23 Fun 𝐹
28 funssfv 6425 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((Fun 𝐹𝑓𝐹𝑦 ∈ dom 𝑓) → (𝐹𝑦) = (𝑓𝑦))
29283adant3l 1222 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((Fun 𝐹𝑓𝐹 ∧ (Pred(𝑅, 𝐴, 𝑦) ⊆ dom 𝑓𝑦 ∈ dom 𝑓)) → (𝐹𝑦) = (𝑓𝑦))
30 fun2ssres 6141 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((Fun 𝐹𝑓𝐹 ∧ Pred(𝑅, 𝐴, 𝑦) ⊆ dom 𝑓) → (𝐹 ↾ Pred(𝑅, 𝐴, 𝑦)) = (𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))
31303adant3r 1224 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((Fun 𝐹𝑓𝐹 ∧ (Pred(𝑅, 𝐴, 𝑦) ⊆ dom 𝑓𝑦 ∈ dom 𝑓)) → (𝐹 ↾ Pred(𝑅, 𝐴, 𝑦)) = (𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))
3231fveq2d 6408 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((Fun 𝐹𝑓𝐹 ∧ (Pred(𝑅, 𝐴, 𝑦) ⊆ dom 𝑓𝑦 ∈ dom 𝑓)) → (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦))) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))
3329, 32eqeq12d 2821 . . . . . . . . . . . . . . . . . . . . . . . 24 ((Fun 𝐹𝑓𝐹 ∧ (Pred(𝑅, 𝐴, 𝑦) ⊆ dom 𝑓𝑦 ∈ dom 𝑓)) → ((𝐹𝑦) = (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦))) ↔ (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))))
3433biimprd 239 . . . . . . . . . . . . . . . . . . . . . . 23 ((Fun 𝐹𝑓𝐹 ∧ (Pred(𝑅, 𝐴, 𝑦) ⊆ dom 𝑓𝑦 ∈ dom 𝑓)) → ((𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))) → (𝐹𝑦) = (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦)))))
3527, 34mp3an1 1565 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑓𝐹 ∧ (Pred(𝑅, 𝐴, 𝑦) ⊆ dom 𝑓𝑦 ∈ dom 𝑓)) → ((𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))) → (𝐹𝑦) = (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦)))))
3635expcom 400 . . . . . . . . . . . . . . . . . . . . 21 ((Pred(𝑅, 𝐴, 𝑦) ⊆ dom 𝑓𝑦 ∈ dom 𝑓) → (𝑓𝐹 → ((𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))) → (𝐹𝑦) = (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦))))))
3736com23 86 . . . . . . . . . . . . . . . . . . . 20 ((Pred(𝑅, 𝐴, 𝑦) ⊆ dom 𝑓𝑦 ∈ dom 𝑓) → ((𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))) → (𝑓𝐹 → (𝐹𝑦) = (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦))))))
3824, 37syl6com 37 . . . . . . . . . . . . . . . . . . 19 (𝑦𝑥 → ((Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥𝑓 Fn 𝑥) → ((𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))) → (𝑓𝐹 → (𝐹𝑦) = (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦)))))))
3938expd 402 . . . . . . . . . . . . . . . . . 18 (𝑦𝑥 → (Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥 → (𝑓 Fn 𝑥 → ((𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))) → (𝑓𝐹 → (𝐹𝑦) = (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦))))))))
4039com34 91 . . . . . . . . . . . . . . . . 17 (𝑦𝑥 → (Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥 → ((𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))) → (𝑓 Fn 𝑥 → (𝑓𝐹 → (𝐹𝑦) = (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦))))))))
4117, 40sylcom 30 . . . . . . . . . . . . . . . 16 (∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥 → (𝑦𝑥 → ((𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))) → (𝑓 Fn 𝑥 → (𝑓𝐹 → (𝐹𝑦) = (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦))))))))
4241adantl 469 . . . . . . . . . . . . . . 15 ((𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) → (𝑦𝑥 → ((𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))) → (𝑓 Fn 𝑥 → (𝑓𝐹 → (𝐹𝑦) = (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦))))))))
4342com14 96 . . . . . . . . . . . . . 14 (𝑓 Fn 𝑥 → (𝑦𝑥 → ((𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))) → ((𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) → (𝑓𝐹 → (𝐹𝑦) = (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦))))))))
4416, 43syl7 74 . . . . . . . . . . . . 13 (𝑓 Fn 𝑥 → (𝑦𝑥 → ((𝑦𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))) → ((𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) → (𝑓𝐹 → (𝐹𝑦) = (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦))))))))
4544exp4a 420 . . . . . . . . . . . 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 1450 . . . . . . . 8 (⟨𝑦, 𝑧⟩ ∈ 𝑓 → ((𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))) → (𝑓𝐹 → (𝐹𝑦) = (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦))))))
5049exlimdv 2024 . . . . . . 7 (⟨𝑦, 𝑧⟩ ∈ 𝑓 → (∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))) → (𝑓𝐹 → (𝐹𝑦) = (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦))))))
5112, 50mpdi 45 . . . . . 6 (⟨𝑦, 𝑧⟩ ∈ 𝑓 → (∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))) → (𝐹𝑦) = (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦)))))
5251imp 395 . . . . 5 ((⟨𝑦, 𝑧⟩ ∈ 𝑓 ∧ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))) → (𝐹𝑦) = (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦))))
5352exlimiv 2021 . . . 4 (∃𝑓(⟨𝑦, 𝑧⟩ ∈ 𝑓 ∧ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))) → (𝐹𝑦) = (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦))))
548, 53sylbi 208 . . 3 (⟨𝑦, 𝑧⟩ ∈ 𝐹 → (𝐹𝑦) = (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦))))
5554exlimiv 2021 . 2 (∃𝑧𝑦, 𝑧⟩ ∈ 𝐹 → (𝐹𝑦) = (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦))))
562, 55sylbi 208 1 (𝑦 ∈ dom 𝐹 → (𝐹𝑦) = (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1100   = wceq 1637  wex 1859  wcel 2156  {cab 2792  wral 3096  wss 3769  cop 4376   cuni 4630   Se wse 5268   We wwe 5269  dom cdm 5311  cres 5313  Predcpred 5892  Fun wfun 6091   Fn wfn 6092  cfv 6097  wrecscwrecs 7637
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-8 2158  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-sep 4975  ax-nul 4983  ax-pow 5035  ax-pr 5096
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ne 2979  df-ral 3101  df-rex 3102  df-reu 3103  df-rmo 3104  df-rab 3105  df-v 3393  df-sbc 3634  df-csb 3729  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4117  df-if 4280  df-sn 4371  df-pr 4373  df-op 4377  df-uni 4631  df-iun 4714  df-br 4845  df-opab 4907  df-mpt 4924  df-id 5219  df-po 5232  df-so 5233  df-fr 5270  df-se 5271  df-we 5272  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-res 5323  df-ima 5324  df-pred 5893  df-iota 6060  df-fun 6099  df-fn 6100  df-fv 6105  df-wrecs 7638
This theorem is referenced by:  wfrlem14  7660  wfr2a  7664
  Copyright terms: Public domain W3C validator