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

Theorem frrlem13 8323
Description: Lemma for well-founded recursion. Assuming that 𝑆 is a subset of 𝐴 and that 𝑧 is 𝑅-minimal, then 𝐶 is an acceptable function. (Contributed by Scott Fenton, 7-Dec-2022.)
Hypotheses
Ref Expression
frrlem11.1 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}
frrlem11.2 𝐹 = frecs(𝑅, 𝐴, 𝐺)
frrlem11.3 ((𝜑 ∧ (𝑔𝐵𝐵)) → ((𝑥𝑔𝑢𝑥𝑣) → 𝑢 = 𝑣))
frrlem11.4 𝐶 = ((𝐹𝑆) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩})
frrlem12.5 (𝜑𝑅 Fr 𝐴)
frrlem12.6 ((𝜑𝑧𝐴) → Pred(𝑅, 𝐴, 𝑧) ⊆ 𝑆)
frrlem12.7 ((𝜑𝑧𝐴) → ∀𝑤𝑆 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑆)
frrlem13.8 ((𝜑𝑧𝐴) → 𝑆 ∈ V)
frrlem13.9 ((𝜑𝑧𝐴) → 𝑆𝐴)
Assertion
Ref Expression
frrlem13 ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → 𝐶𝐵)
Distinct variable groups:   𝐴,𝑓,𝑥,𝑦,𝑧   𝑓,𝐺,𝑥,𝑦,𝑧   𝑅,𝑓,𝑥,𝑦,𝑧   𝐵,𝑔,,𝑧   𝑥,𝐹,𝑢,𝑣,𝑧   𝜑,𝑓,𝑧   𝑓,𝐹   𝜑,𝑔,,𝑥,𝑢,𝑣   𝐴,,𝑤,𝑓,𝑦,𝑥   𝑤,𝐺   𝑤,𝑅   𝑦,𝐹   𝑥,𝐵   𝑤,𝐶   𝑤,𝐹   𝜑,𝑤   𝑤,𝑆   𝑧,𝑤
Allowed substitution hints:   𝜑(𝑦)   𝐴(𝑣,𝑢,𝑔)   𝐵(𝑦,𝑤,𝑣,𝑢,𝑓)   𝐶(𝑥,𝑦,𝑧,𝑣,𝑢,𝑓,𝑔,)   𝑅(𝑣,𝑢,𝑔,)   𝑆(𝑥,𝑦,𝑧,𝑣,𝑢,𝑓,𝑔,)   𝐹(𝑔,)   𝐺(𝑣,𝑢,𝑔,)

Proof of Theorem frrlem13
Dummy variables 𝑐 𝑡 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eldifi 4131 . . . . . 6 (𝑧 ∈ (𝐴 ∖ dom 𝐹) → 𝑧𝐴)
2 frrlem13.8 . . . . . 6 ((𝜑𝑧𝐴) → 𝑆 ∈ V)
31, 2sylan2 593 . . . . 5 ((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) → 𝑆 ∈ V)
43adantrr 717 . . . 4 ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → 𝑆 ∈ V)
5 inex1g 5319 . . . . 5 (𝑆 ∈ V → (𝑆 ∩ dom 𝐹) ∈ V)
6 snex 5436 . . . . 5 {𝑧} ∈ V
7 unexg 7763 . . . . 5 (((𝑆 ∩ dom 𝐹) ∈ V ∧ {𝑧} ∈ V) → ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) ∈ V)
85, 6, 7sylancl 586 . . . 4 (𝑆 ∈ V → ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) ∈ V)
94, 8syl 17 . . 3 ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) ∈ V)
10 frrlem11.1 . . . . 5 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}
11 frrlem11.2 . . . . 5 𝐹 = frecs(𝑅, 𝐴, 𝐺)
12 frrlem11.3 . . . . 5 ((𝜑 ∧ (𝑔𝐵𝐵)) → ((𝑥𝑔𝑢𝑥𝑣) → 𝑢 = 𝑣))
13 frrlem11.4 . . . . 5 𝐶 = ((𝐹𝑆) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩})
1410, 11, 12, 13frrlem11 8321 . . . 4 ((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) → 𝐶 Fn ((𝑆 ∩ dom 𝐹) ∪ {𝑧}))
1514adantrr 717 . . 3 ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → 𝐶 Fn ((𝑆 ∩ dom 𝐹) ∪ {𝑧}))
16 inss1 4237 . . . . . 6 (𝑆 ∩ dom 𝐹) ⊆ 𝑆
17 frrlem13.9 . . . . . . . 8 ((𝜑𝑧𝐴) → 𝑆𝐴)
181, 17sylan2 593 . . . . . . 7 ((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) → 𝑆𝐴)
1918adantrr 717 . . . . . 6 ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → 𝑆𝐴)
2016, 19sstrid 3995 . . . . 5 ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → (𝑆 ∩ dom 𝐹) ⊆ 𝐴)
211adantl 481 . . . . . . 7 ((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) → 𝑧𝐴)
2221adantrr 717 . . . . . 6 ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → 𝑧𝐴)
2322snssd 4809 . . . . 5 ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → {𝑧} ⊆ 𝐴)
2420, 23unssd 4192 . . . 4 ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) ⊆ 𝐴)
25 elun 4153 . . . . . . . . 9 (𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) ↔ (𝑤 ∈ (𝑆 ∩ dom 𝐹) ∨ 𝑤 ∈ {𝑧}))
26 elin 3967 . . . . . . . . . 10 (𝑤 ∈ (𝑆 ∩ dom 𝐹) ↔ (𝑤𝑆𝑤 ∈ dom 𝐹))
27 velsn 4642 . . . . . . . . . 10 (𝑤 ∈ {𝑧} ↔ 𝑤 = 𝑧)
2826, 27orbi12i 915 . . . . . . . . 9 ((𝑤 ∈ (𝑆 ∩ dom 𝐹) ∨ 𝑤 ∈ {𝑧}) ↔ ((𝑤𝑆𝑤 ∈ dom 𝐹) ∨ 𝑤 = 𝑧))
2925, 28bitri 275 . . . . . . . 8 (𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) ↔ ((𝑤𝑆𝑤 ∈ dom 𝐹) ∨ 𝑤 = 𝑧))
30 frrlem12.7 . . . . . . . . . . . . . 14 ((𝜑𝑧𝐴) → ∀𝑤𝑆 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑆)
311, 30sylan2 593 . . . . . . . . . . . . 13 ((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) → ∀𝑤𝑆 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑆)
3231adantrr 717 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → ∀𝑤𝑆 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑆)
33 rsp 3247 . . . . . . . . . . . 12 (∀𝑤𝑆 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑆 → (𝑤𝑆 → Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑆))
3432, 33syl 17 . . . . . . . . . . 11 ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → (𝑤𝑆 → Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑆))
3510, 11frrlem8 8318 . . . . . . . . . . 11 (𝑤 ∈ dom 𝐹 → Pred(𝑅, 𝐴, 𝑤) ⊆ dom 𝐹)
3634, 35anim12d1 610 . . . . . . . . . 10 ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → ((𝑤𝑆𝑤 ∈ dom 𝐹) → (Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑆 ∧ Pred(𝑅, 𝐴, 𝑤) ⊆ dom 𝐹)))
37 ssin 4239 . . . . . . . . . 10 ((Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑆 ∧ Pred(𝑅, 𝐴, 𝑤) ⊆ dom 𝐹) ↔ Pred(𝑅, 𝐴, 𝑤) ⊆ (𝑆 ∩ dom 𝐹))
3836, 37imbitrdi 251 . . . . . . . . 9 ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → ((𝑤𝑆𝑤 ∈ dom 𝐹) → Pred(𝑅, 𝐴, 𝑤) ⊆ (𝑆 ∩ dom 𝐹)))
39 frrlem12.6 . . . . . . . . . . . . 13 ((𝜑𝑧𝐴) → Pred(𝑅, 𝐴, 𝑧) ⊆ 𝑆)
401, 39sylan2 593 . . . . . . . . . . . 12 ((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) → Pred(𝑅, 𝐴, 𝑧) ⊆ 𝑆)
4140adantrr 717 . . . . . . . . . . 11 ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → Pred(𝑅, 𝐴, 𝑧) ⊆ 𝑆)
42 preddif 6350 . . . . . . . . . . . . . . . 16 Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = (Pred(𝑅, 𝐴, 𝑧) ∖ Pred(𝑅, dom 𝐹, 𝑧))
4342eqeq1i 2742 . . . . . . . . . . . . . . 15 (Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅ ↔ (Pred(𝑅, 𝐴, 𝑧) ∖ Pred(𝑅, dom 𝐹, 𝑧)) = ∅)
44 ssdif0 4366 . . . . . . . . . . . . . . 15 (Pred(𝑅, 𝐴, 𝑧) ⊆ Pred(𝑅, dom 𝐹, 𝑧) ↔ (Pred(𝑅, 𝐴, 𝑧) ∖ Pred(𝑅, dom 𝐹, 𝑧)) = ∅)
4543, 44sylbb2 238 . . . . . . . . . . . . . 14 (Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅ → Pred(𝑅, 𝐴, 𝑧) ⊆ Pred(𝑅, dom 𝐹, 𝑧))
46 predss 6329 . . . . . . . . . . . . . 14 Pred(𝑅, dom 𝐹, 𝑧) ⊆ dom 𝐹
4745, 46sstrdi 3996 . . . . . . . . . . . . 13 (Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅ → Pred(𝑅, 𝐴, 𝑧) ⊆ dom 𝐹)
4847adantl 481 . . . . . . . . . . . 12 ((𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅) → Pred(𝑅, 𝐴, 𝑧) ⊆ dom 𝐹)
4948adantl 481 . . . . . . . . . . 11 ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → Pred(𝑅, 𝐴, 𝑧) ⊆ dom 𝐹)
5041, 49ssind 4241 . . . . . . . . . 10 ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → Pred(𝑅, 𝐴, 𝑧) ⊆ (𝑆 ∩ dom 𝐹))
51 predeq3 6325 . . . . . . . . . . 11 (𝑤 = 𝑧 → Pred(𝑅, 𝐴, 𝑤) = Pred(𝑅, 𝐴, 𝑧))
5251sseq1d 4015 . . . . . . . . . 10 (𝑤 = 𝑧 → (Pred(𝑅, 𝐴, 𝑤) ⊆ (𝑆 ∩ dom 𝐹) ↔ Pred(𝑅, 𝐴, 𝑧) ⊆ (𝑆 ∩ dom 𝐹)))
5350, 52syl5ibrcom 247 . . . . . . . . 9 ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → (𝑤 = 𝑧 → Pred(𝑅, 𝐴, 𝑤) ⊆ (𝑆 ∩ dom 𝐹)))
5438, 53jaod 860 . . . . . . . 8 ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → (((𝑤𝑆𝑤 ∈ dom 𝐹) ∨ 𝑤 = 𝑧) → Pred(𝑅, 𝐴, 𝑤) ⊆ (𝑆 ∩ dom 𝐹)))
5529, 54biimtrid 242 . . . . . . 7 ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → (𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) → Pred(𝑅, 𝐴, 𝑤) ⊆ (𝑆 ∩ dom 𝐹)))
5655imp 406 . . . . . 6 (((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) ∧ 𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})) → Pred(𝑅, 𝐴, 𝑤) ⊆ (𝑆 ∩ dom 𝐹))
57 ssun1 4178 . . . . . 6 (𝑆 ∩ dom 𝐹) ⊆ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})
5856, 57sstrdi 3996 . . . . 5 (((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) ∧ 𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})) → Pred(𝑅, 𝐴, 𝑤) ⊆ ((𝑆 ∩ dom 𝐹) ∪ {𝑧}))
5958ralrimiva 3146 . . . 4 ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → ∀𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})Pred(𝑅, 𝐴, 𝑤) ⊆ ((𝑆 ∩ dom 𝐹) ∪ {𝑧}))
6024, 59jca 511 . . 3 ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → (((𝑆 ∩ dom 𝐹) ∪ {𝑧}) ⊆ 𝐴 ∧ ∀𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})Pred(𝑅, 𝐴, 𝑤) ⊆ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})))
61 frrlem12.5 . . . . . . 7 (𝜑𝑅 Fr 𝐴)
6210, 11, 12, 13, 61, 39, 30frrlem12 8322 . . . . . 6 ((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ 𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})) → (𝐶𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))))
63623expa 1119 . . . . 5 (((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) ∧ 𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})) → (𝐶𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))))
6463ralrimiva 3146 . . . 4 ((𝜑𝑧 ∈ (𝐴 ∖ dom 𝐹)) → ∀𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})(𝐶𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))))
6564adantrr 717 . . 3 ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → ∀𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})(𝐶𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))))
66 fneq2 6660 . . . . . 6 (𝑡 = ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) → (𝐶 Fn 𝑡𝐶 Fn ((𝑆 ∩ dom 𝐹) ∪ {𝑧})))
67 sseq1 4009 . . . . . . 7 (𝑡 = ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) → (𝑡𝐴 ↔ ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) ⊆ 𝐴))
68 sseq2 4010 . . . . . . . 8 (𝑡 = ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) → (Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑡 ↔ Pred(𝑅, 𝐴, 𝑤) ⊆ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})))
6968raleqbi1dv 3338 . . . . . . 7 (𝑡 = ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) → (∀𝑤𝑡 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑡 ↔ ∀𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})Pred(𝑅, 𝐴, 𝑤) ⊆ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})))
7067, 69anbi12d 632 . . . . . 6 (𝑡 = ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) → ((𝑡𝐴 ∧ ∀𝑤𝑡 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑡) ↔ (((𝑆 ∩ dom 𝐹) ∪ {𝑧}) ⊆ 𝐴 ∧ ∀𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})Pred(𝑅, 𝐴, 𝑤) ⊆ ((𝑆 ∩ dom 𝐹) ∪ {𝑧}))))
71 raleq 3323 . . . . . 6 (𝑡 = ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) → (∀𝑤𝑡 (𝐶𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))) ↔ ∀𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})(𝐶𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)))))
7266, 70, 713anbi123d 1438 . . . . 5 (𝑡 = ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) → ((𝐶 Fn 𝑡 ∧ (𝑡𝐴 ∧ ∀𝑤𝑡 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑡) ∧ ∀𝑤𝑡 (𝐶𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)))) ↔ (𝐶 Fn ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) ∧ (((𝑆 ∩ dom 𝐹) ∪ {𝑧}) ⊆ 𝐴 ∧ ∀𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})Pred(𝑅, 𝐴, 𝑤) ⊆ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})) ∧ ∀𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})(𝐶𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))))))
7372spcegv 3597 . . . 4 (((𝑆 ∩ dom 𝐹) ∪ {𝑧}) ∈ V → ((𝐶 Fn ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) ∧ (((𝑆 ∩ dom 𝐹) ∪ {𝑧}) ⊆ 𝐴 ∧ ∀𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})Pred(𝑅, 𝐴, 𝑤) ⊆ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})) ∧ ∀𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})(𝐶𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)))) → ∃𝑡(𝐶 Fn 𝑡 ∧ (𝑡𝐴 ∧ ∀𝑤𝑡 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑡) ∧ ∀𝑤𝑡 (𝐶𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))))))
7473imp 406 . . 3 ((((𝑆 ∩ dom 𝐹) ∪ {𝑧}) ∈ V ∧ (𝐶 Fn ((𝑆 ∩ dom 𝐹) ∪ {𝑧}) ∧ (((𝑆 ∩ dom 𝐹) ∪ {𝑧}) ⊆ 𝐴 ∧ ∀𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})Pred(𝑅, 𝐴, 𝑤) ⊆ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})) ∧ ∀𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})(𝐶𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))))) → ∃𝑡(𝐶 Fn 𝑡 ∧ (𝑡𝐴 ∧ ∀𝑤𝑡 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑡) ∧ ∀𝑤𝑡 (𝐶𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)))))
759, 15, 60, 65, 74syl13anc 1374 . 2 ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → ∃𝑡(𝐶 Fn 𝑡 ∧ (𝑡𝐴 ∧ ∀𝑤𝑡 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑡) ∧ ∀𝑤𝑡 (𝐶𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)))))
7610, 11, 12frrlem9 8319 . . . . . 6 (𝜑 → Fun 𝐹)
77 resfunexg 7235 . . . . . 6 ((Fun 𝐹𝑆 ∈ V) → (𝐹𝑆) ∈ V)
7876, 4, 77syl2an2r 685 . . . . 5 ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → (𝐹𝑆) ∈ V)
79 snex 5436 . . . . 5 {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} ∈ V
80 unexg 7763 . . . . 5 (((𝐹𝑆) ∈ V ∧ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} ∈ V) → ((𝐹𝑆) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩}) ∈ V)
8178, 79, 80sylancl 586 . . . 4 ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → ((𝐹𝑆) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩}) ∈ V)
8213, 81eqeltrid 2845 . . 3 ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → 𝐶 ∈ V)
83 fneq1 6659 . . . . . 6 (𝑐 = 𝐶 → (𝑐 Fn 𝑡𝐶 Fn 𝑡))
84 fveq1 6905 . . . . . . . 8 (𝑐 = 𝐶 → (𝑐𝑤) = (𝐶𝑤))
85 reseq1 5991 . . . . . . . . 9 (𝑐 = 𝐶 → (𝑐 ↾ Pred(𝑅, 𝐴, 𝑤)) = (𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)))
8685oveq2d 7447 . . . . . . . 8 (𝑐 = 𝐶 → (𝑤𝐺(𝑐 ↾ Pred(𝑅, 𝐴, 𝑤))) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))))
8784, 86eqeq12d 2753 . . . . . . 7 (𝑐 = 𝐶 → ((𝑐𝑤) = (𝑤𝐺(𝑐 ↾ Pred(𝑅, 𝐴, 𝑤))) ↔ (𝐶𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)))))
8887ralbidv 3178 . . . . . 6 (𝑐 = 𝐶 → (∀𝑤𝑡 (𝑐𝑤) = (𝑤𝐺(𝑐 ↾ Pred(𝑅, 𝐴, 𝑤))) ↔ ∀𝑤𝑡 (𝐶𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)))))
8983, 883anbi13d 1440 . . . . 5 (𝑐 = 𝐶 → ((𝑐 Fn 𝑡 ∧ (𝑡𝐴 ∧ ∀𝑤𝑡 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑡) ∧ ∀𝑤𝑡 (𝑐𝑤) = (𝑤𝐺(𝑐 ↾ Pred(𝑅, 𝐴, 𝑤)))) ↔ (𝐶 Fn 𝑡 ∧ (𝑡𝐴 ∧ ∀𝑤𝑡 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑡) ∧ ∀𝑤𝑡 (𝐶𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))))))
9089exbidv 1921 . . . 4 (𝑐 = 𝐶 → (∃𝑡(𝑐 Fn 𝑡 ∧ (𝑡𝐴 ∧ ∀𝑤𝑡 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑡) ∧ ∀𝑤𝑡 (𝑐𝑤) = (𝑤𝐺(𝑐 ↾ Pred(𝑅, 𝐴, 𝑤)))) ↔ ∃𝑡(𝐶 Fn 𝑡 ∧ (𝑡𝐴 ∧ ∀𝑤𝑡 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑡) ∧ ∀𝑤𝑡 (𝐶𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))))))
9110frrlem1 8311 . . . 4 𝐵 = {𝑐 ∣ ∃𝑡(𝑐 Fn 𝑡 ∧ (𝑡𝐴 ∧ ∀𝑤𝑡 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑡) ∧ ∀𝑤𝑡 (𝑐𝑤) = (𝑤𝐺(𝑐 ↾ Pred(𝑅, 𝐴, 𝑤))))}
9290, 91elab2g 3680 . . 3 (𝐶 ∈ V → (𝐶𝐵 ↔ ∃𝑡(𝐶 Fn 𝑡 ∧ (𝑡𝐴 ∧ ∀𝑤𝑡 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑡) ∧ ∀𝑤𝑡 (𝐶𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))))))
9382, 92syl 17 . 2 ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → (𝐶𝐵 ↔ ∃𝑡(𝐶 Fn 𝑡 ∧ (𝑡𝐴 ∧ ∀𝑤𝑡 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑡) ∧ ∀𝑤𝑡 (𝐶𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤))))))
9475, 93mpbird 257 1 ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → 𝐶𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  wo 848  w3a 1087   = wceq 1540  wex 1779  wcel 2108  {cab 2714  wral 3061  Vcvv 3480  cdif 3948  cun 3949  cin 3950  wss 3951  c0 4333  {csn 4626  cop 4632   class class class wbr 5143   Fr wfr 5634  dom cdm 5685  cres 5687  Predcpred 6320  Fun wfun 6555   Fn wfn 6556  cfv 6561  (class class class)co 7431  frecscfrecs 8305
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pr 5432  ax-un 7755
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-fr 5637  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-ov 7434  df-frecs 8306
This theorem is referenced by:  frrlem14  8324
  Copyright terms: Public domain W3C validator