Metamath Proof Explorer

Theorem frrlem13

Description: Lemma for well-founded recursion. Assuming that S is a subset of A and that z is R -minimal, then C is an acceptable function. (Contributed by Scott Fenton, 7-Dec-2022)

Ref Expression
Hypotheses 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 frrlem13 ( ( 𝜑 ∧ ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ∧ Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑧 ) = ∅ ) ) → 𝐶 ∈ 𝐵 )

Proof

Step Hyp Ref Expression
1 frrlem11.1 ⊢ 𝐵 = { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) }
2 frrlem11.2 ⊢ 𝐹 = frecs ( 𝑅 , 𝐴 , 𝐺 )
3 frrlem11.3 ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ) → ( ( 𝑥 𝑔 𝑢 ∧ 𝑥 ℎ 𝑣 ) → 𝑢 = 𝑣 ) )
4 frrlem11.4 ⊢ 𝐶 = ( ( 𝐹 ↾ 𝑆 ) ∪ { ⟨ 𝑧 , ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } )
5 frrlem12.5 ⊢ ( 𝜑 → 𝑅 Fr 𝐴 )
6 frrlem12.6 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ 𝑆 )
7 frrlem12.7 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ∀ 𝑤 ∈ 𝑆 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑆 )
8 frrlem13.8 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → 𝑆 ∈ V )
9 frrlem13.9 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → 𝑆 ⊆ 𝐴 )
10 eldifi ⊢ ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) → 𝑧 ∈ 𝐴 )
11 10 8 sylan2 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) → 𝑆 ∈ V )
12 11 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ∧ Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑧 ) = ∅ ) ) → 𝑆 ∈ V )
13 inex1g ⊢ ( 𝑆 ∈ V → ( 𝑆 ∩ dom 𝐹 ) ∈ V )
14 snex ⊢ { 𝑧 } ∈ V
15 unexg ⊢ ( ( ( 𝑆 ∩ dom 𝐹 ) ∈ V ∧ { 𝑧 } ∈ V ) → ( ( 𝑆 ∩ dom 𝐹 ) ∪ { 𝑧 } ) ∈ V )
16 13 14 15 sylancl ⊢ ( 𝑆 ∈ V → ( ( 𝑆 ∩ dom 𝐹 ) ∪ { 𝑧 } ) ∈ V )
17 12 16 syl ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ∧ Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑧 ) = ∅ ) ) → ( ( 𝑆 ∩ dom 𝐹 ) ∪ { 𝑧 } ) ∈ V )
18 1 2 3 4 frrlem11 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) → 𝐶 Fn ( ( 𝑆 ∩ dom 𝐹 ) ∪ { 𝑧 } ) )
19 18 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ∧ Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑧 ) = ∅ ) ) → 𝐶 Fn ( ( 𝑆 ∩ dom 𝐹 ) ∪ { 𝑧 } ) )
20 inss1 ⊢ ( 𝑆 ∩ dom 𝐹 ) ⊆ 𝑆
21 10 9 sylan2 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) → 𝑆 ⊆ 𝐴 )
22 21 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ∧ Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑧 ) = ∅ ) ) → 𝑆 ⊆ 𝐴 )
23 20 22 sstrid ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ∧ Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑧 ) = ∅ ) ) → ( 𝑆 ∩ dom 𝐹 ) ⊆ 𝐴 )
24 10 adantl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) → 𝑧 ∈ 𝐴 )
25 24 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ∧ Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑧 ) = ∅ ) ) → 𝑧 ∈ 𝐴 )
26 25 snssd ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ∧ Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑧 ) = ∅ ) ) → { 𝑧 } ⊆ 𝐴 )
27 23 26 unssd ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ∧ Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑧 ) = ∅ ) ) → ( ( 𝑆 ∩ dom 𝐹 ) ∪ { 𝑧 } ) ⊆ 𝐴 )
28 elun ⊢ ( 𝑤 ∈ ( ( 𝑆 ∩ dom 𝐹 ) ∪ { 𝑧 } ) ↔ ( 𝑤 ∈ ( 𝑆 ∩ dom 𝐹 ) ∨ 𝑤 ∈ { 𝑧 } ) )
29 elin ⊢ ( 𝑤 ∈ ( 𝑆 ∩ dom 𝐹 ) ↔ ( 𝑤 ∈ 𝑆 ∧ 𝑤 ∈ dom 𝐹 ) )
30 velsn ⊢ ( 𝑤 ∈ { 𝑧 } ↔ 𝑤 = 𝑧 )
31 29 30 orbi12i ⊢ ( ( 𝑤 ∈ ( 𝑆 ∩ dom 𝐹 ) ∨ 𝑤 ∈ { 𝑧 } ) ↔ ( ( 𝑤 ∈ 𝑆 ∧ 𝑤 ∈ dom 𝐹 ) ∨ 𝑤 = 𝑧 ) )
32 28 31 bitri ⊢ ( 𝑤 ∈ ( ( 𝑆 ∩ dom 𝐹 ) ∪ { 𝑧 } ) ↔ ( ( 𝑤 ∈ 𝑆 ∧ 𝑤 ∈ dom 𝐹 ) ∨ 𝑤 = 𝑧 ) )
33 10 7 sylan2 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) → ∀ 𝑤 ∈ 𝑆 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑆 )
34 33 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ∧ Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑧 ) = ∅ ) ) → ∀ 𝑤 ∈ 𝑆 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑆 )
35 rsp ⊢ ( ∀ 𝑤 ∈ 𝑆 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑆 → ( 𝑤 ∈ 𝑆 → Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑆 ) )
36 34 35 syl ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ∧ Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑧 ) = ∅ ) ) → ( 𝑤 ∈ 𝑆 → Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑆 ) )
37 1 2 frrlem8 ⊢ ( 𝑤 ∈ dom 𝐹 → Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ dom 𝐹 )
38 36 37 anim12d1 ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ∧ Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑧 ) = ∅ ) ) → ( ( 𝑤 ∈ 𝑆 ∧ 𝑤 ∈ dom 𝐹 ) → ( Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑆 ∧ Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ dom 𝐹 ) ) )
39 ssin ⊢ ( ( Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑆 ∧ Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ dom 𝐹 ) ↔ Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ ( 𝑆 ∩ dom 𝐹 ) )
40 38 39 syl6ib ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ∧ Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑧 ) = ∅ ) ) → ( ( 𝑤 ∈ 𝑆 ∧ 𝑤 ∈ dom 𝐹 ) → Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ ( 𝑆 ∩ dom 𝐹 ) ) )
41 10 6 sylan2 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) → Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ 𝑆 )
42 41 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ∧ Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑧 ) = ∅ ) ) → Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ 𝑆 )
43 preddif ⊢ Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑧 ) = ( Pred ( 𝑅 , 𝐴 , 𝑧 ) ∖ Pred ( 𝑅 , dom 𝐹 , 𝑧 ) )
44 43 eqeq1i ⊢ ( Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑧 ) = ∅ ↔ ( Pred ( 𝑅 , 𝐴 , 𝑧 ) ∖ Pred ( 𝑅 , dom 𝐹 , 𝑧 ) ) = ∅ )
45 ssdif0 ⊢ ( Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ Pred ( 𝑅 , dom 𝐹 , 𝑧 ) ↔ ( Pred ( 𝑅 , 𝐴 , 𝑧 ) ∖ Pred ( 𝑅 , dom 𝐹 , 𝑧 ) ) = ∅ )
46 44 45 sylbb2 ⊢ ( Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑧 ) = ∅ → Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ Pred ( 𝑅 , dom 𝐹 , 𝑧 ) )
47 predss ⊢ Pred ( 𝑅 , dom 𝐹 , 𝑧 ) ⊆ dom 𝐹
48 46 47 sstrdi ⊢ ( Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑧 ) = ∅ → Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ dom 𝐹 )
49 48 adantl ⊢ ( ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ∧ Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑧 ) = ∅ ) → Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ dom 𝐹 )
50 49 adantl ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ∧ Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑧 ) = ∅ ) ) → Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ dom 𝐹 )
51 42 50 ssind ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ∧ Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑧 ) = ∅ ) ) → Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ ( 𝑆 ∩ dom 𝐹 ) )
52 predeq3 ⊢ ( 𝑤 = 𝑧 → Pred ( 𝑅 , 𝐴 , 𝑤 ) = Pred ( 𝑅 , 𝐴 , 𝑧 ) )
53 52 sseq1d ⊢ ( 𝑤 = 𝑧 → ( Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ ( 𝑆 ∩ dom 𝐹 ) ↔ Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ ( 𝑆 ∩ dom 𝐹 ) ) )
54 51 53 syl5ibrcom ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ∧ Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑧 ) = ∅ ) ) → ( 𝑤 = 𝑧 → Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ ( 𝑆 ∩ dom 𝐹 ) ) )
55 40 54 jaod ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ∧ Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑧 ) = ∅ ) ) → ( ( ( 𝑤 ∈ 𝑆 ∧ 𝑤 ∈ dom 𝐹 ) ∨ 𝑤 = 𝑧 ) → Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ ( 𝑆 ∩ dom 𝐹 ) ) )
56 32 55 syl5bi ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ∧ Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑧 ) = ∅ ) ) → ( 𝑤 ∈ ( ( 𝑆 ∩ dom 𝐹 ) ∪ { 𝑧 } ) → Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ ( 𝑆 ∩ dom 𝐹 ) ) )
57 56 imp ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ∧ Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑧 ) = ∅ ) ) ∧ 𝑤 ∈ ( ( 𝑆 ∩ dom 𝐹 ) ∪ { 𝑧 } ) ) → Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ ( 𝑆 ∩ dom 𝐹 ) )
58 ssun1 ⊢ ( 𝑆 ∩ dom 𝐹 ) ⊆ ( ( 𝑆 ∩ dom 𝐹 ) ∪ { 𝑧 } )
59 57 58 sstrdi ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ∧ Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑧 ) = ∅ ) ) ∧ 𝑤 ∈ ( ( 𝑆 ∩ dom 𝐹 ) ∪ { 𝑧 } ) ) → Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ ( ( 𝑆 ∩ dom 𝐹 ) ∪ { 𝑧 } ) )
60 59 ralrimiva ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ∧ Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑧 ) = ∅ ) ) → ∀ 𝑤 ∈ ( ( 𝑆 ∩ dom 𝐹 ) ∪ { 𝑧 } ) Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ ( ( 𝑆 ∩ dom 𝐹 ) ∪ { 𝑧 } ) )
61 27 60 jca ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ∧ Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑧 ) = ∅ ) ) → ( ( ( 𝑆 ∩ dom 𝐹 ) ∪ { 𝑧 } ) ⊆ 𝐴 ∧ ∀ 𝑤 ∈ ( ( 𝑆 ∩ dom 𝐹 ) ∪ { 𝑧 } ) Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ ( ( 𝑆 ∩ dom 𝐹 ) ∪ { 𝑧 } ) ) )
62 1 2 3 4 5 6 7 frrlem12 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ∧ 𝑤 ∈ ( ( 𝑆 ∩ dom 𝐹 ) ∪ { 𝑧 } ) ) → ( 𝐶 ‘ 𝑤 ) = ( 𝑤 𝐺 ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) )
63 62 3expa ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) ∧ 𝑤 ∈ ( ( 𝑆 ∩ dom 𝐹 ) ∪ { 𝑧 } ) ) → ( 𝐶 ‘ 𝑤 ) = ( 𝑤 𝐺 ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) )
64 63 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ) → ∀ 𝑤 ∈ ( ( 𝑆 ∩ dom 𝐹 ) ∪ { 𝑧 } ) ( 𝐶 ‘ 𝑤 ) = ( 𝑤 𝐺 ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) )
65 64 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ∧ Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑧 ) = ∅ ) ) → ∀ 𝑤 ∈ ( ( 𝑆 ∩ dom 𝐹 ) ∪ { 𝑧 } ) ( 𝐶 ‘ 𝑤 ) = ( 𝑤 𝐺 ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) )
66 fneq2 ⊢ ( 𝑡 = ( ( 𝑆 ∩ dom 𝐹 ) ∪ { 𝑧 } ) → ( 𝐶 Fn 𝑡 ↔ 𝐶 Fn ( ( 𝑆 ∩ dom 𝐹 ) ∪ { 𝑧 } ) ) )
67 sseq1 ⊢ ( 𝑡 = ( ( 𝑆 ∩ dom 𝐹 ) ∪ { 𝑧 } ) → ( 𝑡 ⊆ 𝐴 ↔ ( ( 𝑆 ∩ dom 𝐹 ) ∪ { 𝑧 } ) ⊆ 𝐴 ) )
68 sseq2 ⊢ ( 𝑡 = ( ( 𝑆 ∩ dom 𝐹 ) ∪ { 𝑧 } ) → ( Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑡 ↔ Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ ( ( 𝑆 ∩ dom 𝐹 ) ∪ { 𝑧 } ) ) )
69 68 raleqbi1dv ⊢ ( 𝑡 = ( ( 𝑆 ∩ dom 𝐹 ) ∪ { 𝑧 } ) → ( ∀ 𝑤 ∈ 𝑡 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑡 ↔ ∀ 𝑤 ∈ ( ( 𝑆 ∩ dom 𝐹 ) ∪ { 𝑧 } ) Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ ( ( 𝑆 ∩ dom 𝐹 ) ∪ { 𝑧 } ) ) )
70 67 69 anbi12d ⊢ ( 𝑡 = ( ( 𝑆 ∩ dom 𝐹 ) ∪ { 𝑧 } ) → ( ( 𝑡 ⊆ 𝐴 ∧ ∀ 𝑤 ∈ 𝑡 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑡 ) ↔ ( ( ( 𝑆 ∩ dom 𝐹 ) ∪ { 𝑧 } ) ⊆ 𝐴 ∧ ∀ 𝑤 ∈ ( ( 𝑆 ∩ dom 𝐹 ) ∪ { 𝑧 } ) Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ ( ( 𝑆 ∩ dom 𝐹 ) ∪ { 𝑧 } ) ) ) )
71 raleq ⊢ ( 𝑡 = ( ( 𝑆 ∩ dom 𝐹 ) ∪ { 𝑧 } ) → ( ∀ 𝑤 ∈ 𝑡 ( 𝐶 ‘ 𝑤 ) = ( 𝑤 𝐺 ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) ↔ ∀ 𝑤 ∈ ( ( 𝑆 ∩ dom 𝐹 ) ∪ { 𝑧 } ) ( 𝐶 ‘ 𝑤 ) = ( 𝑤 𝐺 ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) ) )
72 66 70 71 3anbi123d ⊢ ( 𝑡 = ( ( 𝑆 ∩ dom 𝐹 ) ∪ { 𝑧 } ) → ( ( 𝐶 Fn 𝑡 ∧ ( 𝑡 ⊆ 𝐴 ∧ ∀ 𝑤 ∈ 𝑡 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑡 ) ∧ ∀ 𝑤 ∈ 𝑡 ( 𝐶 ‘ 𝑤 ) = ( 𝑤 𝐺 ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) ) ↔ ( 𝐶 Fn ( ( 𝑆 ∩ dom 𝐹 ) ∪ { 𝑧 } ) ∧ ( ( ( 𝑆 ∩ dom 𝐹 ) ∪ { 𝑧 } ) ⊆ 𝐴 ∧ ∀ 𝑤 ∈ ( ( 𝑆 ∩ dom 𝐹 ) ∪ { 𝑧 } ) Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ ( ( 𝑆 ∩ dom 𝐹 ) ∪ { 𝑧 } ) ) ∧ ∀ 𝑤 ∈ ( ( 𝑆 ∩ dom 𝐹 ) ∪ { 𝑧 } ) ( 𝐶 ‘ 𝑤 ) = ( 𝑤 𝐺 ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) ) ) )
73 72 spcegv ⊢ ( ( ( 𝑆 ∩ dom 𝐹 ) ∪ { 𝑧 } ) ∈ V → ( ( 𝐶 Fn ( ( 𝑆 ∩ dom 𝐹 ) ∪ { 𝑧 } ) ∧ ( ( ( 𝑆 ∩ dom 𝐹 ) ∪ { 𝑧 } ) ⊆ 𝐴 ∧ ∀ 𝑤 ∈ ( ( 𝑆 ∩ dom 𝐹 ) ∪ { 𝑧 } ) Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ ( ( 𝑆 ∩ dom 𝐹 ) ∪ { 𝑧 } ) ) ∧ ∀ 𝑤 ∈ ( ( 𝑆 ∩ dom 𝐹 ) ∪ { 𝑧 } ) ( 𝐶 ‘ 𝑤 ) = ( 𝑤 𝐺 ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) ) → ∃ 𝑡 ( 𝐶 Fn 𝑡 ∧ ( 𝑡 ⊆ 𝐴 ∧ ∀ 𝑤 ∈ 𝑡 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑡 ) ∧ ∀ 𝑤 ∈ 𝑡 ( 𝐶 ‘ 𝑤 ) = ( 𝑤 𝐺 ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) ) ) )
74 73 imp ⊢ ( ( ( ( 𝑆 ∩ dom 𝐹 ) ∪ { 𝑧 } ) ∈ V ∧ ( 𝐶 Fn ( ( 𝑆 ∩ dom 𝐹 ) ∪ { 𝑧 } ) ∧ ( ( ( 𝑆 ∩ dom 𝐹 ) ∪ { 𝑧 } ) ⊆ 𝐴 ∧ ∀ 𝑤 ∈ ( ( 𝑆 ∩ dom 𝐹 ) ∪ { 𝑧 } ) Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ ( ( 𝑆 ∩ dom 𝐹 ) ∪ { 𝑧 } ) ) ∧ ∀ 𝑤 ∈ ( ( 𝑆 ∩ dom 𝐹 ) ∪ { 𝑧 } ) ( 𝐶 ‘ 𝑤 ) = ( 𝑤 𝐺 ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) ) ) → ∃ 𝑡 ( 𝐶 Fn 𝑡 ∧ ( 𝑡 ⊆ 𝐴 ∧ ∀ 𝑤 ∈ 𝑡 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑡 ) ∧ ∀ 𝑤 ∈ 𝑡 ( 𝐶 ‘ 𝑤 ) = ( 𝑤 𝐺 ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) ) )
75 17 19 61 65 74 syl13anc ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ∧ Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑧 ) = ∅ ) ) → ∃ 𝑡 ( 𝐶 Fn 𝑡 ∧ ( 𝑡 ⊆ 𝐴 ∧ ∀ 𝑤 ∈ 𝑡 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑡 ) ∧ ∀ 𝑤 ∈ 𝑡 ( 𝐶 ‘ 𝑤 ) = ( 𝑤 𝐺 ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) ) )
76 1 2 3 frrlem9 ⊢ ( 𝜑 → Fun 𝐹 )
77 resfunexg ⊢ ( ( Fun 𝐹 ∧ 𝑆 ∈ V ) → ( 𝐹 ↾ 𝑆 ) ∈ V )
78 76 12 77 syl2an2r ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ∧ Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑧 ) = ∅ ) ) → ( 𝐹 ↾ 𝑆 ) ∈ V )
79 snex ⊢ { ⟨ 𝑧 , ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } ∈ V
80 unexg ⊢ ( ( ( 𝐹 ↾ 𝑆 ) ∈ V ∧ { ⟨ 𝑧 , ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } ∈ V ) → ( ( 𝐹 ↾ 𝑆 ) ∪ { ⟨ 𝑧 , ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } ) ∈ V )
81 78 79 80 sylancl ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ∧ Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑧 ) = ∅ ) ) → ( ( 𝐹 ↾ 𝑆 ) ∪ { ⟨ 𝑧 , ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } ) ∈ V )
82 4 81 eqeltrid ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ∧ Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑧 ) = ∅ ) ) → 𝐶 ∈ V )
83 fneq1 ⊢ ( 𝑐 = 𝐶 → ( 𝑐 Fn 𝑡 ↔ 𝐶 Fn 𝑡 ) )
84 fveq1 ⊢ ( 𝑐 = 𝐶 → ( 𝑐 ‘ 𝑤 ) = ( 𝐶 ‘ 𝑤 ) )
85 reseq1 ⊢ ( 𝑐 = 𝐶 → ( 𝑐 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) = ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) )
86 85 oveq2d ⊢ ( 𝑐 = 𝐶 → ( 𝑤 𝐺 ( 𝑐 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) = ( 𝑤 𝐺 ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) )
87 84 86 eqeq12d ⊢ ( 𝑐 = 𝐶 → ( ( 𝑐 ‘ 𝑤 ) = ( 𝑤 𝐺 ( 𝑐 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) ↔ ( 𝐶 ‘ 𝑤 ) = ( 𝑤 𝐺 ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) ) )
88 87 ralbidv ⊢ ( 𝑐 = 𝐶 → ( ∀ 𝑤 ∈ 𝑡 ( 𝑐 ‘ 𝑤 ) = ( 𝑤 𝐺 ( 𝑐 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) ↔ ∀ 𝑤 ∈ 𝑡 ( 𝐶 ‘ 𝑤 ) = ( 𝑤 𝐺 ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) ) )
89 83 88 3anbi13d ⊢ ( 𝑐 = 𝐶 → ( ( 𝑐 Fn 𝑡 ∧ ( 𝑡 ⊆ 𝐴 ∧ ∀ 𝑤 ∈ 𝑡 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑡 ) ∧ ∀ 𝑤 ∈ 𝑡 ( 𝑐 ‘ 𝑤 ) = ( 𝑤 𝐺 ( 𝑐 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) ) ↔ ( 𝐶 Fn 𝑡 ∧ ( 𝑡 ⊆ 𝐴 ∧ ∀ 𝑤 ∈ 𝑡 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑡 ) ∧ ∀ 𝑤 ∈ 𝑡 ( 𝐶 ‘ 𝑤 ) = ( 𝑤 𝐺 ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) ) ) )
90 89 exbidv ⊢ ( 𝑐 = 𝐶 → ( ∃ 𝑡 ( 𝑐 Fn 𝑡 ∧ ( 𝑡 ⊆ 𝐴 ∧ ∀ 𝑤 ∈ 𝑡 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑡 ) ∧ ∀ 𝑤 ∈ 𝑡 ( 𝑐 ‘ 𝑤 ) = ( 𝑤 𝐺 ( 𝑐 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) ) ↔ ∃ 𝑡 ( 𝐶 Fn 𝑡 ∧ ( 𝑡 ⊆ 𝐴 ∧ ∀ 𝑤 ∈ 𝑡 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑡 ) ∧ ∀ 𝑤 ∈ 𝑡 ( 𝐶 ‘ 𝑤 ) = ( 𝑤 𝐺 ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) ) ) )
91 1 frrlem1 ⊢ 𝐵 = { 𝑐 ∣ ∃ 𝑡 ( 𝑐 Fn 𝑡 ∧ ( 𝑡 ⊆ 𝐴 ∧ ∀ 𝑤 ∈ 𝑡 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑡 ) ∧ ∀ 𝑤 ∈ 𝑡 ( 𝑐 ‘ 𝑤 ) = ( 𝑤 𝐺 ( 𝑐 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) ) }
92 90 91 elab2g ⊢ ( 𝐶 ∈ V → ( 𝐶 ∈ 𝐵 ↔ ∃ 𝑡 ( 𝐶 Fn 𝑡 ∧ ( 𝑡 ⊆ 𝐴 ∧ ∀ 𝑤 ∈ 𝑡 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑡 ) ∧ ∀ 𝑤 ∈ 𝑡 ( 𝐶 ‘ 𝑤 ) = ( 𝑤 𝐺 ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) ) ) )
93 82 92 syl ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ∧ Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑧 ) = ∅ ) ) → ( 𝐶 ∈ 𝐵 ↔ ∃ 𝑡 ( 𝐶 Fn 𝑡 ∧ ( 𝑡 ⊆ 𝐴 ∧ ∀ 𝑤 ∈ 𝑡 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑡 ) ∧ ∀ 𝑤 ∈ 𝑡 ( 𝐶 ‘ 𝑤 ) = ( 𝑤 𝐺 ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) ) ) )
94 75 93 mpbird ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ∧ Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑧 ) = ∅ ) ) → 𝐶 ∈ 𝐵 )