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

Theorem wfrlem17 7600
 Description: Without using ax-rep 4923, show that all restrictions of wrecs are sets. (Contributed by Scott Fenton, 31-Jul-2020.)
Hypotheses
Ref Expression
wfrlem17.1 𝑅 We 𝐴
wfrlem17.2 𝑅 Se 𝐴
wfrlem17.3 𝐹 = wrecs(𝑅, 𝐴, 𝐺)
Assertion
Ref Expression
wfrlem17 (𝑋 ∈ dom 𝐹 → (𝐹 ↾ Pred(𝑅, 𝐴, 𝑋)) ∈ V)

Proof of Theorem wfrlem17
Dummy variables 𝑓 𝑔 𝑥 𝑦 𝑧 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 wfrlem17.1 . . . . 5 𝑅 We 𝐴
2 wfrlem17.2 . . . . 5 𝑅 Se 𝐴
3 wfrlem17.3 . . . . 5 𝐹 = wrecs(𝑅, 𝐴, 𝐺)
41, 2, 3wfrfun 7594 . . . 4 Fun 𝐹
5 funfvop 6492 . . . 4 ((Fun 𝐹𝑋 ∈ dom 𝐹) → ⟨𝑋, (𝐹𝑋)⟩ ∈ 𝐹)
64, 5mpan 708 . . 3 (𝑋 ∈ dom 𝐹 → ⟨𝑋, (𝐹𝑋)⟩ ∈ 𝐹)
7 df-wrecs 7576 . . . . . 6 wrecs(𝑅, 𝐴, 𝐺) = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}
83, 7eqtri 2782 . . . . 5 𝐹 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}
98eleq2i 2831 . . . 4 (⟨𝑋, (𝐹𝑋)⟩ ∈ 𝐹 ↔ ⟨𝑋, (𝐹𝑋)⟩ ∈ {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))})
10 eluni 4591 . . . 4 (⟨𝑋, (𝐹𝑋)⟩ ∈ {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} ↔ ∃𝑔(⟨𝑋, (𝐹𝑋)⟩ ∈ 𝑔𝑔 ∈ {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}))
119, 10bitri 264 . . 3 (⟨𝑋, (𝐹𝑋)⟩ ∈ 𝐹 ↔ ∃𝑔(⟨𝑋, (𝐹𝑋)⟩ ∈ 𝑔𝑔 ∈ {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}))
126, 11sylib 208 . 2 (𝑋 ∈ dom 𝐹 → ∃𝑔(⟨𝑋, (𝐹𝑋)⟩ ∈ 𝑔𝑔 ∈ {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}))
13 simprr 813 . . . 4 ((𝑋 ∈ dom 𝐹 ∧ (⟨𝑋, (𝐹𝑋)⟩ ∈ 𝑔𝑔 ∈ {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))})) → 𝑔 ∈ {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))})
14 eqid 2760 . . . . 5 {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}
15 vex 3343 . . . . 5 𝑔 ∈ V
1614, 15wfrlem3a 7586 . . . 4 (𝑔 ∈ {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} ↔ ∃𝑧(𝑔 Fn 𝑧 ∧ (𝑧𝐴 ∧ ∀𝑤𝑧 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑧) ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑤)))))
1713, 16sylib 208 . . 3 ((𝑋 ∈ dom 𝐹 ∧ (⟨𝑋, (𝐹𝑋)⟩ ∈ 𝑔𝑔 ∈ {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))})) → ∃𝑧(𝑔 Fn 𝑧 ∧ (𝑧𝐴 ∧ ∀𝑤𝑧 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑧) ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑤)))))
18 3simpa 1143 . . . . 5 ((𝑔 Fn 𝑧 ∧ (𝑧𝐴 ∧ ∀𝑤𝑧 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑧) ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑤)))) → (𝑔 Fn 𝑧 ∧ (𝑧𝐴 ∧ ∀𝑤𝑧 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑧)))
19 simprlr 822 . . . . . . . . 9 ((𝑋 ∈ dom 𝐹 ∧ ((⟨𝑋, (𝐹𝑋)⟩ ∈ 𝑔𝑔 ∈ {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}) ∧ (𝑔 Fn 𝑧 ∧ (𝑧𝐴 ∧ ∀𝑤𝑧 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑧)))) → 𝑔 ∈ {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))})
20 elssuni 4619 . . . . . . . . . 10 (𝑔 ∈ {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} → 𝑔 {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))})
2120, 8syl6sseqr 3793 . . . . . . . . 9 (𝑔 ∈ {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} → 𝑔𝐹)
2219, 21syl 17 . . . . . . . 8 ((𝑋 ∈ dom 𝐹 ∧ ((⟨𝑋, (𝐹𝑋)⟩ ∈ 𝑔𝑔 ∈ {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}) ∧ (𝑔 Fn 𝑧 ∧ (𝑧𝐴 ∧ ∀𝑤𝑧 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑧)))) → 𝑔𝐹)
23 predeq3 5845 . . . . . . . . . . 11 (𝑤 = 𝑋 → Pred(𝑅, 𝐴, 𝑤) = Pred(𝑅, 𝐴, 𝑋))
2423sseq1d 3773 . . . . . . . . . 10 (𝑤 = 𝑋 → (Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑧 ↔ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝑧))
25 simprrr 824 . . . . . . . . . . 11 (((⟨𝑋, (𝐹𝑋)⟩ ∈ 𝑔𝑔 ∈ {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}) ∧ (𝑔 Fn 𝑧 ∧ (𝑧𝐴 ∧ ∀𝑤𝑧 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑧))) → ∀𝑤𝑧 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑧)
2625adantl 473 . . . . . . . . . 10 ((𝑋 ∈ dom 𝐹 ∧ ((⟨𝑋, (𝐹𝑋)⟩ ∈ 𝑔𝑔 ∈ {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}) ∧ (𝑔 Fn 𝑧 ∧ (𝑧𝐴 ∧ ∀𝑤𝑧 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑧)))) → ∀𝑤𝑧 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑧)
27 simprll 821 . . . . . . . . . . . . 13 ((𝑋 ∈ dom 𝐹 ∧ ((⟨𝑋, (𝐹𝑋)⟩ ∈ 𝑔𝑔 ∈ {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}) ∧ (𝑔 Fn 𝑧 ∧ (𝑧𝐴 ∧ ∀𝑤𝑧 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑧)))) → ⟨𝑋, (𝐹𝑋)⟩ ∈ 𝑔)
28 df-br 4805 . . . . . . . . . . . . 13 (𝑋𝑔(𝐹𝑋) ↔ ⟨𝑋, (𝐹𝑋)⟩ ∈ 𝑔)
2927, 28sylibr 224 . . . . . . . . . . . 12 ((𝑋 ∈ dom 𝐹 ∧ ((⟨𝑋, (𝐹𝑋)⟩ ∈ 𝑔𝑔 ∈ {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}) ∧ (𝑔 Fn 𝑧 ∧ (𝑧𝐴 ∧ ∀𝑤𝑧 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑧)))) → 𝑋𝑔(𝐹𝑋))
30 fvex 6362 . . . . . . . . . . . . 13 (𝐹𝑋) ∈ V
31 breldmg 5485 . . . . . . . . . . . . 13 ((𝑋 ∈ dom 𝐹 ∧ (𝐹𝑋) ∈ V ∧ 𝑋𝑔(𝐹𝑋)) → 𝑋 ∈ dom 𝑔)
3230, 31mp3an2 1561 . . . . . . . . . . . 12 ((𝑋 ∈ dom 𝐹𝑋𝑔(𝐹𝑋)) → 𝑋 ∈ dom 𝑔)
3329, 32syldan 488 . . . . . . . . . . 11 ((𝑋 ∈ dom 𝐹 ∧ ((⟨𝑋, (𝐹𝑋)⟩ ∈ 𝑔𝑔 ∈ {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}) ∧ (𝑔 Fn 𝑧 ∧ (𝑧𝐴 ∧ ∀𝑤𝑧 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑧)))) → 𝑋 ∈ dom 𝑔)
34 simprrl 823 . . . . . . . . . . . 12 ((𝑋 ∈ dom 𝐹 ∧ ((⟨𝑋, (𝐹𝑋)⟩ ∈ 𝑔𝑔 ∈ {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}) ∧ (𝑔 Fn 𝑧 ∧ (𝑧𝐴 ∧ ∀𝑤𝑧 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑧)))) → 𝑔 Fn 𝑧)
35 fndm 6151 . . . . . . . . . . . 12 (𝑔 Fn 𝑧 → dom 𝑔 = 𝑧)
3634, 35syl 17 . . . . . . . . . . 11 ((𝑋 ∈ dom 𝐹 ∧ ((⟨𝑋, (𝐹𝑋)⟩ ∈ 𝑔𝑔 ∈ {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}) ∧ (𝑔 Fn 𝑧 ∧ (𝑧𝐴 ∧ ∀𝑤𝑧 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑧)))) → dom 𝑔 = 𝑧)
3733, 36eleqtrd 2841 . . . . . . . . . 10 ((𝑋 ∈ dom 𝐹 ∧ ((⟨𝑋, (𝐹𝑋)⟩ ∈ 𝑔𝑔 ∈ {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}) ∧ (𝑔 Fn 𝑧 ∧ (𝑧𝐴 ∧ ∀𝑤𝑧 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑧)))) → 𝑋𝑧)
3824, 26, 37rspcdva 3455 . . . . . . . . 9 ((𝑋 ∈ dom 𝐹 ∧ ((⟨𝑋, (𝐹𝑋)⟩ ∈ 𝑔𝑔 ∈ {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}) ∧ (𝑔 Fn 𝑧 ∧ (𝑧𝐴 ∧ ∀𝑤𝑧 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑧)))) → Pred(𝑅, 𝐴, 𝑋) ⊆ 𝑧)
3938, 36sseqtr4d 3783 . . . . . . . 8 ((𝑋 ∈ dom 𝐹 ∧ ((⟨𝑋, (𝐹𝑋)⟩ ∈ 𝑔𝑔 ∈ {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}) ∧ (𝑔 Fn 𝑧 ∧ (𝑧𝐴 ∧ ∀𝑤𝑧 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑧)))) → Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝑔)
40 fun2ssres 6092 . . . . . . . . 9 ((Fun 𝐹𝑔𝐹 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝑔) → (𝐹 ↾ Pred(𝑅, 𝐴, 𝑋)) = (𝑔 ↾ Pred(𝑅, 𝐴, 𝑋)))
414, 40mp3an1 1560 . . . . . . . 8 ((𝑔𝐹 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝑔) → (𝐹 ↾ Pred(𝑅, 𝐴, 𝑋)) = (𝑔 ↾ Pred(𝑅, 𝐴, 𝑋)))
4222, 39, 41syl2anc 696 . . . . . . 7 ((𝑋 ∈ dom 𝐹 ∧ ((⟨𝑋, (𝐹𝑋)⟩ ∈ 𝑔𝑔 ∈ {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}) ∧ (𝑔 Fn 𝑧 ∧ (𝑧𝐴 ∧ ∀𝑤𝑧 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑧)))) → (𝐹 ↾ Pred(𝑅, 𝐴, 𝑋)) = (𝑔 ↾ Pred(𝑅, 𝐴, 𝑋)))
4315resex 5601 . . . . . . 7 (𝑔 ↾ Pred(𝑅, 𝐴, 𝑋)) ∈ V
4442, 43syl6eqel 2847 . . . . . 6 ((𝑋 ∈ dom 𝐹 ∧ ((⟨𝑋, (𝐹𝑋)⟩ ∈ 𝑔𝑔 ∈ {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}) ∧ (𝑔 Fn 𝑧 ∧ (𝑧𝐴 ∧ ∀𝑤𝑧 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑧)))) → (𝐹 ↾ Pred(𝑅, 𝐴, 𝑋)) ∈ V)
4544expr 644 . . . . 5 ((𝑋 ∈ dom 𝐹 ∧ (⟨𝑋, (𝐹𝑋)⟩ ∈ 𝑔𝑔 ∈ {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))})) → ((𝑔 Fn 𝑧 ∧ (𝑧𝐴 ∧ ∀𝑤𝑧 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑧)) → (𝐹 ↾ Pred(𝑅, 𝐴, 𝑋)) ∈ V))
4618, 45syl5 34 . . . 4 ((𝑋 ∈ dom 𝐹 ∧ (⟨𝑋, (𝐹𝑋)⟩ ∈ 𝑔𝑔 ∈ {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))})) → ((𝑔 Fn 𝑧 ∧ (𝑧𝐴 ∧ ∀𝑤𝑧 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑧) ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑤)))) → (𝐹 ↾ Pred(𝑅, 𝐴, 𝑋)) ∈ V))
4746exlimdv 2010 . . 3 ((𝑋 ∈ dom 𝐹 ∧ (⟨𝑋, (𝐹𝑋)⟩ ∈ 𝑔𝑔 ∈ {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))})) → (∃𝑧(𝑔 Fn 𝑧 ∧ (𝑧𝐴 ∧ ∀𝑤𝑧 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑧) ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑤)))) → (𝐹 ↾ Pred(𝑅, 𝐴, 𝑋)) ∈ V))
4817, 47mpd 15 . 2 ((𝑋 ∈ dom 𝐹 ∧ (⟨𝑋, (𝐹𝑋)⟩ ∈ 𝑔𝑔 ∈ {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))})) → (𝐹 ↾ Pred(𝑅, 𝐴, 𝑋)) ∈ V)
4912, 48exlimddv 2012 1 (𝑋 ∈ dom 𝐹 → (𝐹 ↾ Pred(𝑅, 𝐴, 𝑋)) ∈ V)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1072   = wceq 1632  ∃wex 1853   ∈ wcel 2139  {cab 2746  ∀wral 3050  Vcvv 3340   ⊆ wss 3715  ⟨cop 4327  ∪ cuni 4588   class class class wbr 4804   Se wse 5223   We wwe 5224  dom cdm 5266   ↾ cres 5268  Predcpred 5840  Fun wfun 6043   Fn wfn 6044  ‘cfv 6049  wrecscwrecs 7575 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-ral 3055  df-rex 3056  df-reu 3057  df-rmo 3058  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-iun 4674  df-br 4805  df-opab 4865  df-mpt 4882  df-id 5174  df-po 5187  df-so 5188  df-fr 5225  df-se 5226  df-we 5227  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-pred 5841  df-iota 6012  df-fun 6051  df-fn 6052  df-fv 6057  df-wrecs 7576 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator