Metamath Proof Explorer

Theorem wfrlem14

Description: Lemma for well-founded recursion. Compute the value of C . (Contributed by Scott Fenton, 21-Apr-2011)

Ref Expression
Hypotheses wfrlem13.1 ⊢ 𝑅 We 𝐴
wfrlem13.2 ⊢ 𝑅 Se 𝐴
wfrlem13.3 ⊢ 𝐹 = wrecs ( 𝑅 , 𝐴 , 𝐺 )
wfrlem13.4 ⊢ 𝐶 = ( 𝐹 ∪ { ⟨ 𝑧 , ( 𝐺 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } )
Assertion wfrlem14 ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) → ( 𝑦 ∈ ( dom 𝐹 ∪ { 𝑧 } ) → ( 𝐶 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 wfrlem13.1 ⊢ 𝑅 We 𝐴
2 wfrlem13.2 ⊢ 𝑅 Se 𝐴
3 wfrlem13.3 ⊢ 𝐹 = wrecs ( 𝑅 , 𝐴 , 𝐺 )
4 wfrlem13.4 ⊢ 𝐶 = ( 𝐹 ∪ { ⟨ 𝑧 , ( 𝐺 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } )
5 1 2 3 4 wfrlem13 ⊢ ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) → 𝐶 Fn ( dom 𝐹 ∪ { 𝑧 } ) )
6 elun ⊢ ( 𝑦 ∈ ( dom 𝐹 ∪ { 𝑧 } ) ↔ ( 𝑦 ∈ dom 𝐹 ∨ 𝑦 ∈ { 𝑧 } ) )
7 velsn ⊢ ( 𝑦 ∈ { 𝑧 } ↔ 𝑦 = 𝑧 )
8 7 orbi2i ⊢ ( ( 𝑦 ∈ dom 𝐹 ∨ 𝑦 ∈ { 𝑧 } ) ↔ ( 𝑦 ∈ dom 𝐹 ∨ 𝑦 = 𝑧 ) )
9 6 8 bitri ⊢ ( 𝑦 ∈ ( dom 𝐹 ∪ { 𝑧 } ) ↔ ( 𝑦 ∈ dom 𝐹 ∨ 𝑦 = 𝑧 ) )
10 1 2 3 wfrlem12 ⊢ ( 𝑦 ∈ dom 𝐹 → ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) )
11 fnfun ⊢ ( 𝐶 Fn ( dom 𝐹 ∪ { 𝑧 } ) → Fun 𝐶 )
12 ssun1 ⊢ 𝐹 ⊆ ( 𝐹 ∪ { ⟨ 𝑧 , ( 𝐺 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } )
13 12 4 sseqtrri ⊢ 𝐹 ⊆ 𝐶
14 funssfv ⊢ ( ( Fun 𝐶 ∧ 𝐹 ⊆ 𝐶 ∧ 𝑦 ∈ dom 𝐹 ) → ( 𝐶 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) )
15 3 wfrdmcl ⊢ ( 𝑦 ∈ dom 𝐹 → Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ dom 𝐹 )
16 fun2ssres ⊢ ( ( Fun 𝐶 ∧ 𝐹 ⊆ 𝐶 ∧ Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ dom 𝐹 ) → ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) = ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) )
17 15 16 syl3an3 ⊢ ( ( Fun 𝐶 ∧ 𝐹 ⊆ 𝐶 ∧ 𝑦 ∈ dom 𝐹 ) → ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) = ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) )
18 17 fveq2d ⊢ ( ( Fun 𝐶 ∧ 𝐹 ⊆ 𝐶 ∧ 𝑦 ∈ dom 𝐹 ) → ( 𝐺 ‘ ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) = ( 𝐺 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) )
19 14 18 eqeq12d ⊢ ( ( Fun 𝐶 ∧ 𝐹 ⊆ 𝐶 ∧ 𝑦 ∈ dom 𝐹 ) → ( ( 𝐶 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ↔ ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) )
20 13 19 mp3an2 ⊢ ( ( Fun 𝐶 ∧ 𝑦 ∈ dom 𝐹 ) → ( ( 𝐶 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ↔ ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) )
21 11 20 sylan ⊢ ( ( 𝐶 Fn ( dom 𝐹 ∪ { 𝑧 } ) ∧ 𝑦 ∈ dom 𝐹 ) → ( ( 𝐶 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ↔ ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) )
22 10 21 syl5ibr ⊢ ( ( 𝐶 Fn ( dom 𝐹 ∪ { 𝑧 } ) ∧ 𝑦 ∈ dom 𝐹 ) → ( 𝑦 ∈ dom 𝐹 → ( 𝐶 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) )
23 22 ex ⊢ ( 𝐶 Fn ( dom 𝐹 ∪ { 𝑧 } ) → ( 𝑦 ∈ dom 𝐹 → ( 𝑦 ∈ dom 𝐹 → ( 𝐶 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ) )
24 23 pm2.43d ⊢ ( 𝐶 Fn ( dom 𝐹 ∪ { 𝑧 } ) → ( 𝑦 ∈ dom 𝐹 → ( 𝐶 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) )
25 vsnid ⊢ 𝑧 ∈ { 𝑧 }
26 elun2 ⊢ ( 𝑧 ∈ { 𝑧 } → 𝑧 ∈ ( dom 𝐹 ∪ { 𝑧 } ) )
27 25 26 ax-mp ⊢ 𝑧 ∈ ( dom 𝐹 ∪ { 𝑧 } )
28 4 reseq1i ⊢ ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) = ( ( 𝐹 ∪ { ⟨ 𝑧 , ( 𝐺 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } ) ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) )
29 resundir ⊢ ( ( 𝐹 ∪ { ⟨ 𝑧 , ( 𝐺 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } ) ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) = ( ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ∪ ( { ⟨ 𝑧 , ( 𝐺 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) )
30 wefr ⊢ ( 𝑅 We 𝐴 → 𝑅 Fr 𝐴 )
31 1 30 ax-mp ⊢ 𝑅 Fr 𝐴
32 predfrirr ⊢ ( 𝑅 Fr 𝐴 → ¬ 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑧 ) )
33 ressnop0 ⊢ ( ¬ 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑧 ) → ( { ⟨ 𝑧 , ( 𝐺 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) = ∅ )
34 31 32 33 mp2b ⊢ ( { ⟨ 𝑧 , ( 𝐺 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) = ∅
35 34 uneq2i ⊢ ( ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ∪ ( { ⟨ 𝑧 , ( 𝐺 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) = ( ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ∪ ∅ )
36 un0 ⊢ ( ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ∪ ∅ ) = ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) )
37 35 36 eqtri ⊢ ( ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ∪ ( { ⟨ 𝑧 , ( 𝐺 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) = ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) )
38 28 29 37 3eqtri ⊢ ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) = ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) )
39 38 fveq2i ⊢ ( 𝐺 ‘ ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) = ( 𝐺 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) )
40 39 opeq2i ⊢ ⟨ 𝑧 , ( 𝐺 ‘ ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ = ⟨ 𝑧 , ( 𝐺 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩
41 opex ⊢ ⟨ 𝑧 , ( 𝐺 ‘ ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ ∈ V
42 41 elsn ⊢ ( ⟨ 𝑧 , ( 𝐺 ‘ ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ ∈ { ⟨ 𝑧 , ( 𝐺 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } ↔ ⟨ 𝑧 , ( 𝐺 ‘ ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ = ⟨ 𝑧 , ( 𝐺 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ )
43 40 42 mpbir ⊢ ⟨ 𝑧 , ( 𝐺 ‘ ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ ∈ { ⟨ 𝑧 , ( 𝐺 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ }
44 elun2 ⊢ ( ⟨ 𝑧 , ( 𝐺 ‘ ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ ∈ { ⟨ 𝑧 , ( 𝐺 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } → ⟨ 𝑧 , ( 𝐺 ‘ ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ ∈ ( 𝐹 ∪ { ⟨ 𝑧 , ( 𝐺 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } ) )
45 43 44 ax-mp ⊢ ⟨ 𝑧 , ( 𝐺 ‘ ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ ∈ ( 𝐹 ∪ { ⟨ 𝑧 , ( 𝐺 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } )
46 45 4 eleqtrri ⊢ ⟨ 𝑧 , ( 𝐺 ‘ ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ ∈ 𝐶
47 fnopfvb ⊢ ( ( 𝐶 Fn ( dom 𝐹 ∪ { 𝑧 } ) ∧ 𝑧 ∈ ( dom 𝐹 ∪ { 𝑧 } ) ) → ( ( 𝐶 ‘ 𝑧 ) = ( 𝐺 ‘ ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ↔ ⟨ 𝑧 , ( 𝐺 ‘ ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ ∈ 𝐶 ) )
48 46 47 mpbiri ⊢ ( ( 𝐶 Fn ( dom 𝐹 ∪ { 𝑧 } ) ∧ 𝑧 ∈ ( dom 𝐹 ∪ { 𝑧 } ) ) → ( 𝐶 ‘ 𝑧 ) = ( 𝐺 ‘ ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) )
49 27 48 mpan2 ⊢ ( 𝐶 Fn ( dom 𝐹 ∪ { 𝑧 } ) → ( 𝐶 ‘ 𝑧 ) = ( 𝐺 ‘ ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) )
50 fveq2 ⊢ ( 𝑦 = 𝑧 → ( 𝐶 ‘ 𝑦 ) = ( 𝐶 ‘ 𝑧 ) )
51 predeq3 ⊢ ( 𝑦 = 𝑧 → Pred ( 𝑅 , 𝐴 , 𝑦 ) = Pred ( 𝑅 , 𝐴 , 𝑧 ) )
52 51 reseq2d ⊢ ( 𝑦 = 𝑧 → ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) = ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) )
53 52 fveq2d ⊢ ( 𝑦 = 𝑧 → ( 𝐺 ‘ ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) = ( 𝐺 ‘ ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) )
54 50 53 eqeq12d ⊢ ( 𝑦 = 𝑧 → ( ( 𝐶 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ↔ ( 𝐶 ‘ 𝑧 ) = ( 𝐺 ‘ ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ) )
55 49 54 syl5ibrcom ⊢ ( 𝐶 Fn ( dom 𝐹 ∪ { 𝑧 } ) → ( 𝑦 = 𝑧 → ( 𝐶 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) )
56 24 55 jaod ⊢ ( 𝐶 Fn ( dom 𝐹 ∪ { 𝑧 } ) → ( ( 𝑦 ∈ dom 𝐹 ∨ 𝑦 = 𝑧 ) → ( 𝐶 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) )
57 9 56 syl5bi ⊢ ( 𝐶 Fn ( dom 𝐹 ∪ { 𝑧 } ) → ( 𝑦 ∈ ( dom 𝐹 ∪ { 𝑧 } ) → ( 𝐶 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) )
58 5 57 syl ⊢ ( 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) → ( 𝑦 ∈ ( dom 𝐹 ∪ { 𝑧 } ) → ( 𝐶 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝐶 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) )