Metamath Proof Explorer

Theorem wfrlem15OLD

Description: Obsolete version as of 18-Nov-2024. Lemma for well-ordered recursion. When z is R minimal, C is an acceptable function. This step is where the Axiom of Replacement becomes required. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by Scott Fenton, 21-Apr-2011)

Ref Expression
Hypotheses wfrlem13OLD.1 ⊢ 𝑅 We 𝐴
wfrlem13OLD.2 ⊢ 𝑅 Se 𝐴
wfrlem13OLD.3 ⊢ 𝐹 = wrecs ( 𝑅 , 𝐴 , 𝐺 )
wfrlem13OLD.4 ⊢ 𝐶 = ( 𝐹 ∪ { ⟨ 𝑧 , ( 𝐺 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } )
Assertion wfrlem15OLD ( ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ∧ Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑧 ) = ∅ ) → 𝐶 ∈ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } )

Proof

Step Hyp Ref Expression
1 wfrlem13OLD.1 ⊢ 𝑅 We 𝐴
2 wfrlem13OLD.2 ⊢ 𝑅 Se 𝐴
3 wfrlem13OLD.3 ⊢ 𝐹 = wrecs ( 𝑅 , 𝐴 , 𝐺 )
4 wfrlem13OLD.4 ⊢ 𝐶 = ( 𝐹 ∪ { ⟨ 𝑧 , ( 𝐺 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } )
5 1 2 3 4 wfrlem13OLD ⊢ ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) → 𝐶 Fn ( dom 𝐹 ∪ { 𝑧 } ) )
6 5 adantr ⊢ ( ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ∧ Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑧 ) = ∅ ) → 𝐶 Fn ( dom 𝐹 ∪ { 𝑧 } ) )
7 1 3 wfrlem10OLD ⊢ ( ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ∧ Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑧 ) = ∅ ) → Pred ( 𝑅 , 𝐴 , 𝑧 ) = dom 𝐹 )
8 eldifi ⊢ ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) → 𝑧 ∈ 𝐴 )
9 setlikespec ⊢ ( ( 𝑧 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) → Pred ( 𝑅 , 𝐴 , 𝑧 ) ∈ V )
10 8 2 9 sylancl ⊢ ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) → Pred ( 𝑅 , 𝐴 , 𝑧 ) ∈ V )
11 10 adantr ⊢ ( ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ∧ Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑧 ) = ∅ ) → Pred ( 𝑅 , 𝐴 , 𝑧 ) ∈ V )
12 7 11 eqeltrrd ⊢ ( ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ∧ Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑧 ) = ∅ ) → dom 𝐹 ∈ V )
13 snex ⊢ { 𝑧 } ∈ V
14 unexg ⊢ ( ( dom 𝐹 ∈ V ∧ { 𝑧 } ∈ V ) → ( dom 𝐹 ∪ { 𝑧 } ) ∈ V )
15 13 14 mpan2 ⊢ ( dom 𝐹 ∈ V → ( dom 𝐹 ∪ { 𝑧 } ) ∈ V )
16 fnex ⊢ ( ( 𝐶 Fn ( dom 𝐹 ∪ { 𝑧 } ) ∧ ( dom 𝐹 ∪ { 𝑧 } ) ∈ V ) → 𝐶 ∈ V )
17 15 16 sylan2 ⊢ ( ( 𝐶 Fn ( dom 𝐹 ∪ { 𝑧 } ) ∧ dom 𝐹 ∈ V ) → 𝐶 ∈ V )
18 6 12 17 syl2anc ⊢ ( ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ∧ Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑧 ) = ∅ ) → 𝐶 ∈ V )
19 12 13 14 sylancl ⊢ ( ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ∧ Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑧 ) = ∅ ) → ( dom 𝐹 ∪ { 𝑧 } ) ∈ V )
20 3 wfrdmssOLD ⊢ dom 𝐹 ⊆ 𝐴
21 8 snssd ⊢ ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) → { 𝑧 } ⊆ 𝐴 )
22 unss ⊢ ( ( dom 𝐹 ⊆ 𝐴 ∧ { 𝑧 } ⊆ 𝐴 ) ↔ ( dom 𝐹 ∪ { 𝑧 } ) ⊆ 𝐴 )
23 22 biimpi ⊢ ( ( dom 𝐹 ⊆ 𝐴 ∧ { 𝑧 } ⊆ 𝐴 ) → ( dom 𝐹 ∪ { 𝑧 } ) ⊆ 𝐴 )
24 20 21 23 sylancr ⊢ ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) → ( dom 𝐹 ∪ { 𝑧 } ) ⊆ 𝐴 )
25 24 adantr ⊢ ( ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ∧ Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑧 ) = ∅ ) → ( dom 𝐹 ∪ { 𝑧 } ) ⊆ 𝐴 )
26 elun ⊢ ( 𝑦 ∈ ( dom 𝐹 ∪ { 𝑧 } ) ↔ ( 𝑦 ∈ dom 𝐹 ∨ 𝑦 ∈ { 𝑧 } ) )
27 velsn ⊢ ( 𝑦 ∈ { 𝑧 } ↔ 𝑦 = 𝑧 )
28 27 orbi2i ⊢ ( ( 𝑦 ∈ dom 𝐹 ∨ 𝑦 ∈ { 𝑧 } ) ↔ ( 𝑦 ∈ dom 𝐹 ∨ 𝑦 = 𝑧 ) )
29 26 28 bitri ⊢ ( 𝑦 ∈ ( dom 𝐹 ∪ { 𝑧 } ) ↔ ( 𝑦 ∈ dom 𝐹 ∨ 𝑦 = 𝑧 ) )
30 3 wfrdmclOLD ⊢ ( 𝑦 ∈ dom 𝐹 → Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ dom 𝐹 )
31 ssun3 ⊢ ( Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ dom 𝐹 → Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ ( dom 𝐹 ∪ { 𝑧 } ) )
32 30 31 syl ⊢ ( 𝑦 ∈ dom 𝐹 → Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ ( dom 𝐹 ∪ { 𝑧 } ) )
33 32 a1i ⊢ ( ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ∧ Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑧 ) = ∅ ) → ( 𝑦 ∈ dom 𝐹 → Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ ( dom 𝐹 ∪ { 𝑧 } ) ) )
34 ssun1 ⊢ dom 𝐹 ⊆ ( dom 𝐹 ∪ { 𝑧 } )
35 7 34 eqsstrdi ⊢ ( ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ∧ Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑧 ) = ∅ ) → Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ ( dom 𝐹 ∪ { 𝑧 } ) )
36 predeq3 ⊢ ( 𝑦 = 𝑧 → Pred ( 𝑅 , 𝐴 , 𝑦 ) = Pred ( 𝑅 , 𝐴 , 𝑧 ) )
37 36 sseq1d ⊢ ( 𝑦 = 𝑧 → ( Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ ( dom 𝐹 ∪ { 𝑧 } ) ↔ Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ ( dom 𝐹 ∪ { 𝑧 } ) ) )
38 35 37 syl5ibrcom ⊢ ( ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ∧ Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑧 ) = ∅ ) → ( 𝑦 = 𝑧 → Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ ( dom 𝐹 ∪ { 𝑧 } ) ) )
39 33 38 jaod ⊢ ( ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ∧ Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑧 ) = ∅ ) → ( ( 𝑦 ∈ dom 𝐹 ∨ 𝑦 = 𝑧 ) → Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ ( dom 𝐹 ∪ { 𝑧 } ) ) )
40 29 39 biimtrid ⊢ ( ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ∧ Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑧 ) = ∅ ) → ( 𝑦 ∈ ( dom 𝐹 ∪ { 𝑧 } ) → Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ ( dom 𝐹 ∪ { 𝑧 } ) ) )
41 40 ralrimiv ⊢ ( ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ∧ Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑧 ) = ∅ ) → ∀ 𝑦 ∈ ( dom 𝐹 ∪ { 𝑧 } ) Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ ( dom 𝐹 ∪ { 𝑧 } ) )
42 25 41 jca ⊢ ( ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ∧ Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑧 ) = ∅ ) → ( ( dom 𝐹 ∪ { 𝑧 } ) ⊆ 𝐴 ∧ ∀ 𝑦 ∈ ( dom 𝐹 ∪ { 𝑧 } ) Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ ( dom 𝐹 ∪ { 𝑧 } ) ) )
43 1 2 3 4 wfrlem14OLD ⊢ ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) → ( 𝑦 ∈ ( dom 𝐹 ∪ { 𝑧 } ) → ( 𝐶 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) )
44 43 ralrimiv ⊢ ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) → ∀ 𝑦 ∈ ( dom 𝐹 ∪ { 𝑧 } ) ( 𝐶 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) )
45 44 adantr ⊢ ( ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ∧ Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑧 ) = ∅ ) → ∀ 𝑦 ∈ ( dom 𝐹 ∪ { 𝑧 } ) ( 𝐶 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) )
46 6 42 45 3jca ⊢ ( ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ∧ Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑧 ) = ∅ ) → ( 𝐶 Fn ( dom 𝐹 ∪ { 𝑧 } ) ∧ ( ( dom 𝐹 ∪ { 𝑧 } ) ⊆ 𝐴 ∧ ∀ 𝑦 ∈ ( dom 𝐹 ∪ { 𝑧 } ) Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ ( dom 𝐹 ∪ { 𝑧 } ) ) ∧ ∀ 𝑦 ∈ ( dom 𝐹 ∪ { 𝑧 } ) ( 𝐶 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) )
47 fneq2 ⊢ ( 𝑥 = ( dom 𝐹 ∪ { 𝑧 } ) → ( 𝐶 Fn 𝑥 ↔ 𝐶 Fn ( dom 𝐹 ∪ { 𝑧 } ) ) )
48 sseq1 ⊢ ( 𝑥 = ( dom 𝐹 ∪ { 𝑧 } ) → ( 𝑥 ⊆ 𝐴 ↔ ( dom 𝐹 ∪ { 𝑧 } ) ⊆ 𝐴 ) )
49 sseq2 ⊢ ( 𝑥 = ( dom 𝐹 ∪ { 𝑧 } ) → ( Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ↔ Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ ( dom 𝐹 ∪ { 𝑧 } ) ) )
50 49 raleqbi1dv ⊢ ( 𝑥 = ( dom 𝐹 ∪ { 𝑧 } ) → ( ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ↔ ∀ 𝑦 ∈ ( dom 𝐹 ∪ { 𝑧 } ) Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ ( dom 𝐹 ∪ { 𝑧 } ) ) )
51 48 50 anbi12d ⊢ ( 𝑥 = ( dom 𝐹 ∪ { 𝑧 } ) → ( ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ↔ ( ( dom 𝐹 ∪ { 𝑧 } ) ⊆ 𝐴 ∧ ∀ 𝑦 ∈ ( dom 𝐹 ∪ { 𝑧 } ) Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ ( dom 𝐹 ∪ { 𝑧 } ) ) ) )
52 raleq ⊢ ( 𝑥 = ( dom 𝐹 ∪ { 𝑧 } ) → ( ∀ 𝑦 ∈ 𝑥 ( 𝐶 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ↔ ∀ 𝑦 ∈ ( dom 𝐹 ∪ { 𝑧 } ) ( 𝐶 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) )
53 47 51 52 3anbi123d ⊢ ( 𝑥 = ( dom 𝐹 ∪ { 𝑧 } ) → ( ( 𝐶 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐶 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ↔ ( 𝐶 Fn ( dom 𝐹 ∪ { 𝑧 } ) ∧ ( ( dom 𝐹 ∪ { 𝑧 } ) ⊆ 𝐴 ∧ ∀ 𝑦 ∈ ( dom 𝐹 ∪ { 𝑧 } ) Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ ( dom 𝐹 ∪ { 𝑧 } ) ) ∧ ∀ 𝑦 ∈ ( dom 𝐹 ∪ { 𝑧 } ) ( 𝐶 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ) )
54 19 46 53 spcedv ⊢ ( ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ∧ Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑧 ) = ∅ ) → ∃ 𝑥 ( 𝐶 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐶 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) )
55 fneq1 ⊢ ( 𝑓 = 𝐶 → ( 𝑓 Fn 𝑥 ↔ 𝐶 Fn 𝑥 ) )
56 fveq1 ⊢ ( 𝑓 = 𝐶 → ( 𝑓 ‘ 𝑦 ) = ( 𝐶 ‘ 𝑦 ) )
57 reseq1 ⊢ ( 𝑓 = 𝐶 → ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) = ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) )
58 57 fveq2d ⊢ ( 𝑓 = 𝐶 → ( 𝐺 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) = ( 𝐺 ‘ ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) )
59 56 58 eqeq12d ⊢ ( 𝑓 = 𝐶 → ( ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ↔ ( 𝐶 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) )
60 59 ralbidv ⊢ ( 𝑓 = 𝐶 → ( ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ↔ ∀ 𝑦 ∈ 𝑥 ( 𝐶 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) )
61 55 60 3anbi13d ⊢ ( 𝑓 = 𝐶 → ( ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ↔ ( 𝐶 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐶 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ) )
62 61 exbidv ⊢ ( 𝑓 = 𝐶 → ( ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ↔ ∃ 𝑥 ( 𝐶 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐶 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ) )
63 18 54 62 elabd ⊢ ( ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) ∧ Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑧 ) = ∅ ) → 𝐶 ∈ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } )