Metamath Proof Explorer


Theorem wfrlem15OLD

Description: 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. Obsolete as of 18-Nov-2024. (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 syl5bi ( ( 𝑧 ∈ ( 𝐴 ∖ 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 ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } )