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 ⊢ R We A
wfrlem13.2 ⊢ R Se A
wfrlem13.3 ⊢ F = wrecs ⁡ R A G
wfrlem13.4 ⊢ C = F ∪ z G ⁡ F ↾ Pred R A z
Assertion wfrlem14 ⊢ z ∈ A ∖ dom ⁡ F → y ∈ dom ⁡ F ∪ z → C ⁡ y = G ⁡ C ↾ Pred R A y

Proof

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