Metamath Proof Explorer

Theorem frrlem4

Description: Lemma for founded recursion. Properties of the restriction of an acceptable function to the domain of another acceptable function. (Contributed by Paul Chapman, 21-Apr-2012)

Ref Expression
Hypothesis frrlem4.1 ⊢ B = f | ∃ x f Fn x ∧ x ⊆ A ∧ ∀ y ∈ x Pred R A y ⊆ x ∧ ∀ y ∈ x f ⁡ y = y G f ↾ Pred R A y
Assertion frrlem4 ⊢ g ∈ B ∧ h ∈ B → g ↾ dom ⁡ g ∩ dom ⁡ h Fn dom ⁡ g ∩ dom ⁡ h ∧ ∀ a ∈ dom ⁡ g ∩ dom ⁡ h g ↾ dom ⁡ g ∩ dom ⁡ h ⁡ a = a G g ↾ dom ⁡ g ∩ dom ⁡ h ↾ Pred R dom ⁡ g ∩ dom ⁡ h a

Proof

Step Hyp Ref Expression
1 frrlem4.1 ⊢ B = f | ∃ x f Fn x ∧ x ⊆ A ∧ ∀ y ∈ x Pred R A y ⊆ x ∧ ∀ y ∈ x f ⁡ y = y G f ↾ Pred R A y
2 1 frrlem2 ⊢ g ∈ B → Fun ⁡ g
3 2 funfnd ⊢ g ∈ B → g Fn dom ⁡ g
4 fnresin1 ⊢ g Fn dom ⁡ g → g ↾ dom ⁡ g ∩ dom ⁡ h Fn dom ⁡ g ∩ dom ⁡ h
5 3 4 syl ⊢ g ∈ B → g ↾ dom ⁡ g ∩ dom ⁡ h Fn dom ⁡ g ∩ dom ⁡ h
6 5 adantr ⊢ g ∈ B ∧ h ∈ B → g ↾ dom ⁡ g ∩ dom ⁡ h Fn dom ⁡ g ∩ dom ⁡ h
7 1 frrlem1 ⊢ B = g | ∃ b g Fn b ∧ b ⊆ A ∧ ∀ a ∈ b Pred R A a ⊆ b ∧ ∀ a ∈ b g ⁡ a = a G g ↾ Pred R A a
8 7 abeq2i ⊢ g ∈ B ↔ ∃ b g Fn b ∧ b ⊆ A ∧ ∀ a ∈ b Pred R A a ⊆ b ∧ ∀ a ∈ b g ⁡ a = a G g ↾ Pred R A a
9 fndm ⊢ g Fn b → dom ⁡ g = b
10 9 adantr ⊢ g Fn b ∧ b ⊆ A ∧ ∀ a ∈ b Pred R A a ⊆ b → dom ⁡ g = b
11 10 raleqdv ⊢ g Fn b ∧ b ⊆ A ∧ ∀ a ∈ b Pred R A a ⊆ b → ∀ a ∈ dom ⁡ g g ⁡ a = a G g ↾ Pred R A a ↔ ∀ a ∈ b g ⁡ a = a G g ↾ Pred R A a
12 11 biimp3ar ⊢ g Fn b ∧ b ⊆ A ∧ ∀ a ∈ b Pred R A a ⊆ b ∧ ∀ a ∈ b g ⁡ a = a G g ↾ Pred R A a → ∀ a ∈ dom ⁡ g g ⁡ a = a G g ↾ Pred R A a
13 rsp ⊢ ∀ a ∈ dom ⁡ g g ⁡ a = a G g ↾ Pred R A a → a ∈ dom ⁡ g → g ⁡ a = a G g ↾ Pred R A a
14 12 13 syl ⊢ g Fn b ∧ b ⊆ A ∧ ∀ a ∈ b Pred R A a ⊆ b ∧ ∀ a ∈ b g ⁡ a = a G g ↾ Pred R A a → a ∈ dom ⁡ g → g ⁡ a = a G g ↾ Pred R A a
15 14 exlimiv ⊢ ∃ b g Fn b ∧ b ⊆ A ∧ ∀ a ∈ b Pred R A a ⊆ b ∧ ∀ a ∈ b g ⁡ a = a G g ↾ Pred R A a → a ∈ dom ⁡ g → g ⁡ a = a G g ↾ Pred R A a
16 8 15 sylbi ⊢ g ∈ B → a ∈ dom ⁡ g → g ⁡ a = a G g ↾ Pred R A a
17 elinel1 ⊢ a ∈ dom ⁡ g ∩ dom ⁡ h → a ∈ dom ⁡ g
18 16 17 impel ⊢ g ∈ B ∧ a ∈ dom ⁡ g ∩ dom ⁡ h → g ⁡ a = a G g ↾ Pred R A a
19 18 adantlr ⊢ g ∈ B ∧ h ∈ B ∧ a ∈ dom ⁡ g ∩ dom ⁡ h → g ⁡ a = a G g ↾ Pred R A a
20 simpr ⊢ g ∈ B ∧ h ∈ B ∧ a ∈ dom ⁡ g ∩ dom ⁡ h → a ∈ dom ⁡ g ∩ dom ⁡ h
21 20 fvresd ⊢ g ∈ B ∧ h ∈ B ∧ a ∈ dom ⁡ g ∩ dom ⁡ h → g ↾ dom ⁡ g ∩ dom ⁡ h ⁡ a = g ⁡ a
22 resres ⊢ g ↾ dom ⁡ g ∩ dom ⁡ h ↾ Pred R dom ⁡ g ∩ dom ⁡ h a = g ↾ dom ⁡ g ∩ dom ⁡ h ∩ Pred R dom ⁡ g ∩ dom ⁡ h a
23 predss ⊢ Pred R dom ⁡ g ∩ dom ⁡ h a ⊆ dom ⁡ g ∩ dom ⁡ h
24 sseqin2 ⊢ Pred R dom ⁡ g ∩ dom ⁡ h a ⊆ dom ⁡ g ∩ dom ⁡ h ↔ dom ⁡ g ∩ dom ⁡ h ∩ Pred R dom ⁡ g ∩ dom ⁡ h a = Pred R dom ⁡ g ∩ dom ⁡ h a
25 23 24 mpbi ⊢ dom ⁡ g ∩ dom ⁡ h ∩ Pred R dom ⁡ g ∩ dom ⁡ h a = Pred R dom ⁡ g ∩ dom ⁡ h a
26 1 frrlem1 ⊢ B = h | ∃ c h Fn c ∧ c ⊆ A ∧ ∀ a ∈ c Pred R A a ⊆ c ∧ ∀ a ∈ c h ⁡ a = a G h ↾ Pred R A a
27 26 abeq2i ⊢ h ∈ B ↔ ∃ c h Fn c ∧ c ⊆ A ∧ ∀ a ∈ c Pred R A a ⊆ c ∧ ∀ a ∈ c h ⁡ a = a G h ↾ Pred R A a
28 exdistrv ⊢ ∃ b ∃ c g Fn b ∧ b ⊆ A ∧ ∀ a ∈ b Pred R A a ⊆ b ∧ ∀ a ∈ b g ⁡ a = a G g ↾ Pred R A a ∧ h Fn c ∧ c ⊆ A ∧ ∀ a ∈ c Pred R A a ⊆ c ∧ ∀ a ∈ c h ⁡ a = a G h ↾ Pred R A a ↔ ∃ b g Fn b ∧ b ⊆ A ∧ ∀ a ∈ b Pred R A a ⊆ b ∧ ∀ a ∈ b g ⁡ a = a G g ↾ Pred R A a ∧ ∃ c h Fn c ∧ c ⊆ A ∧ ∀ a ∈ c Pred R A a ⊆ c ∧ ∀ a ∈ c h ⁡ a = a G h ↾ Pred R A a
29 inss1 ⊢ b ∩ c ⊆ b
30 simpl2l ⊢ g Fn b ∧ b ⊆ A ∧ ∀ a ∈ b Pred R A a ⊆ b ∧ ∀ a ∈ b g ⁡ a = a G g ↾ Pred R A a ∧ h Fn c ∧ c ⊆ A ∧ ∀ a ∈ c Pred R A a ⊆ c ∧ ∀ a ∈ c h ⁡ a = a G h ↾ Pred R A a → b ⊆ A
31 29 30 sstrid ⊢ g Fn b ∧ b ⊆ A ∧ ∀ a ∈ b Pred R A a ⊆ b ∧ ∀ a ∈ b g ⁡ a = a G g ↾ Pred R A a ∧ h Fn c ∧ c ⊆ A ∧ ∀ a ∈ c Pred R A a ⊆ c ∧ ∀ a ∈ c h ⁡ a = a G h ↾ Pred R A a → b ∩ c ⊆ A
32 simp2r ⊢ g Fn b ∧ b ⊆ A ∧ ∀ a ∈ b Pred R A a ⊆ b ∧ ∀ a ∈ b g ⁡ a = a G g ↾ Pred R A a → ∀ a ∈ b Pred R A a ⊆ b
33 simp2r ⊢ h Fn c ∧ c ⊆ A ∧ ∀ a ∈ c Pred R A a ⊆ c ∧ ∀ a ∈ c h ⁡ a = a G h ↾ Pred R A a → ∀ a ∈ c Pred R A a ⊆ c
34 nfra1 ⊢ Ⅎ a ∀ a ∈ b Pred R A a ⊆ b
35 nfra1 ⊢ Ⅎ a ∀ a ∈ c Pred R A a ⊆ c
36 34 35 nfan ⊢ Ⅎ a ∀ a ∈ b Pred R A a ⊆ b ∧ ∀ a ∈ c Pred R A a ⊆ c
37 elinel1 ⊢ a ∈ b ∩ c → a ∈ b
38 rsp ⊢ ∀ a ∈ b Pred R A a ⊆ b → a ∈ b → Pred R A a ⊆ b
39 37 38 syl5com ⊢ a ∈ b ∩ c → ∀ a ∈ b Pred R A a ⊆ b → Pred R A a ⊆ b
40 elinel2 ⊢ a ∈ b ∩ c → a ∈ c
41 rsp ⊢ ∀ a ∈ c Pred R A a ⊆ c → a ∈ c → Pred R A a ⊆ c
42 40 41 syl5com ⊢ a ∈ b ∩ c → ∀ a ∈ c Pred R A a ⊆ c → Pred R A a ⊆ c
43 39 42 anim12d ⊢ a ∈ b ∩ c → ∀ a ∈ b Pred R A a ⊆ b ∧ ∀ a ∈ c Pred R A a ⊆ c → Pred R A a ⊆ b ∧ Pred R A a ⊆ c
44 ssin ⊢ Pred R A a ⊆ b ∧ Pred R A a ⊆ c ↔ Pred R A a ⊆ b ∩ c
45 44 biimpi ⊢ Pred R A a ⊆ b ∧ Pred R A a ⊆ c → Pred R A a ⊆ b ∩ c
46 43 45 syl6com ⊢ ∀ a ∈ b Pred R A a ⊆ b ∧ ∀ a ∈ c Pred R A a ⊆ c → a ∈ b ∩ c → Pred R A a ⊆ b ∩ c
47 36 46 ralrimi ⊢ ∀ a ∈ b Pred R A a ⊆ b ∧ ∀ a ∈ c Pred R A a ⊆ c → ∀ a ∈ b ∩ c Pred R A a ⊆ b ∩ c
48 32 33 47 syl2an ⊢ g Fn b ∧ b ⊆ A ∧ ∀ a ∈ b Pred R A a ⊆ b ∧ ∀ a ∈ b g ⁡ a = a G g ↾ Pred R A a ∧ h Fn c ∧ c ⊆ A ∧ ∀ a ∈ c Pred R A a ⊆ c ∧ ∀ a ∈ c h ⁡ a = a G h ↾ Pred R A a → ∀ a ∈ b ∩ c Pred R A a ⊆ b ∩ c
49 simpl1 ⊢ g Fn b ∧ b ⊆ A ∧ ∀ a ∈ b Pred R A a ⊆ b ∧ ∀ a ∈ b g ⁡ a = a G g ↾ Pred R A a ∧ h Fn c ∧ c ⊆ A ∧ ∀ a ∈ c Pred R A a ⊆ c ∧ ∀ a ∈ c h ⁡ a = a G h ↾ Pred R A a → g Fn b
50 49 fndmd ⊢ g Fn b ∧ b ⊆ A ∧ ∀ a ∈ b Pred R A a ⊆ b ∧ ∀ a ∈ b g ⁡ a = a G g ↾ Pred R A a ∧ h Fn c ∧ c ⊆ A ∧ ∀ a ∈ c Pred R A a ⊆ c ∧ ∀ a ∈ c h ⁡ a = a G h ↾ Pred R A a → dom ⁡ g = b
51 simpr1 ⊢ g Fn b ∧ b ⊆ A ∧ ∀ a ∈ b Pred R A a ⊆ b ∧ ∀ a ∈ b g ⁡ a = a G g ↾ Pred R A a ∧ h Fn c ∧ c ⊆ A ∧ ∀ a ∈ c Pred R A a ⊆ c ∧ ∀ a ∈ c h ⁡ a = a G h ↾ Pred R A a → h Fn c
52 51 fndmd ⊢ g Fn b ∧ b ⊆ A ∧ ∀ a ∈ b Pred R A a ⊆ b ∧ ∀ a ∈ b g ⁡ a = a G g ↾ Pred R A a ∧ h Fn c ∧ c ⊆ A ∧ ∀ a ∈ c Pred R A a ⊆ c ∧ ∀ a ∈ c h ⁡ a = a G h ↾ Pred R A a → dom ⁡ h = c
53 ineq12 ⊢ dom ⁡ g = b ∧ dom ⁡ h = c → dom ⁡ g ∩ dom ⁡ h = b ∩ c
54 53 sseq1d ⊢ dom ⁡ g = b ∧ dom ⁡ h = c → dom ⁡ g ∩ dom ⁡ h ⊆ A ↔ b ∩ c ⊆ A
55 53 sseq2d ⊢ dom ⁡ g = b ∧ dom ⁡ h = c → Pred R A a ⊆ dom ⁡ g ∩ dom ⁡ h ↔ Pred R A a ⊆ b ∩ c
56 53 55 raleqbidv ⊢ dom ⁡ g = b ∧ dom ⁡ h = c → ∀ a ∈ dom ⁡ g ∩ dom ⁡ h Pred R A a ⊆ dom ⁡ g ∩ dom ⁡ h ↔ ∀ a ∈ b ∩ c Pred R A a ⊆ b ∩ c
57 54 56 anbi12d ⊢ dom ⁡ g = b ∧ dom ⁡ h = c → dom ⁡ g ∩ dom ⁡ h ⊆ A ∧ ∀ a ∈ dom ⁡ g ∩ dom ⁡ h Pred R A a ⊆ dom ⁡ g ∩ dom ⁡ h ↔ b ∩ c ⊆ A ∧ ∀ a ∈ b ∩ c Pred R A a ⊆ b ∩ c
58 50 52 57 syl2anc ⊢ g Fn b ∧ b ⊆ A ∧ ∀ a ∈ b Pred R A a ⊆ b ∧ ∀ a ∈ b g ⁡ a = a G g ↾ Pred R A a ∧ h Fn c ∧ c ⊆ A ∧ ∀ a ∈ c Pred R A a ⊆ c ∧ ∀ a ∈ c h ⁡ a = a G h ↾ Pred R A a → dom ⁡ g ∩ dom ⁡ h ⊆ A ∧ ∀ a ∈ dom ⁡ g ∩ dom ⁡ h Pred R A a ⊆ dom ⁡ g ∩ dom ⁡ h ↔ b ∩ c ⊆ A ∧ ∀ a ∈ b ∩ c Pred R A a ⊆ b ∩ c
59 31 48 58 mpbir2and ⊢ g Fn b ∧ b ⊆ A ∧ ∀ a ∈ b Pred R A a ⊆ b ∧ ∀ a ∈ b g ⁡ a = a G g ↾ Pred R A a ∧ h Fn c ∧ c ⊆ A ∧ ∀ a ∈ c Pred R A a ⊆ c ∧ ∀ a ∈ c h ⁡ a = a G h ↾ Pred R A a → dom ⁡ g ∩ dom ⁡ h ⊆ A ∧ ∀ a ∈ dom ⁡ g ∩ dom ⁡ h Pred R A a ⊆ dom ⁡ g ∩ dom ⁡ h
60 59 exlimivv ⊢ ∃ b ∃ c g Fn b ∧ b ⊆ A ∧ ∀ a ∈ b Pred R A a ⊆ b ∧ ∀ a ∈ b g ⁡ a = a G g ↾ Pred R A a ∧ h Fn c ∧ c ⊆ A ∧ ∀ a ∈ c Pred R A a ⊆ c ∧ ∀ a ∈ c h ⁡ a = a G h ↾ Pred R A a → dom ⁡ g ∩ dom ⁡ h ⊆ A ∧ ∀ a ∈ dom ⁡ g ∩ dom ⁡ h Pred R A a ⊆ dom ⁡ g ∩ dom ⁡ h
61 28 60 sylbir ⊢ ∃ b g Fn b ∧ b ⊆ A ∧ ∀ a ∈ b Pred R A a ⊆ b ∧ ∀ a ∈ b g ⁡ a = a G g ↾ Pred R A a ∧ ∃ c h Fn c ∧ c ⊆ A ∧ ∀ a ∈ c Pred R A a ⊆ c ∧ ∀ a ∈ c h ⁡ a = a G h ↾ Pred R A a → dom ⁡ g ∩ dom ⁡ h ⊆ A ∧ ∀ a ∈ dom ⁡ g ∩ dom ⁡ h Pred R A a ⊆ dom ⁡ g ∩ dom ⁡ h
62 8 27 61 syl2anb ⊢ g ∈ B ∧ h ∈ B → dom ⁡ g ∩ dom ⁡ h ⊆ A ∧ ∀ a ∈ dom ⁡ g ∩ dom ⁡ h Pred R A a ⊆ dom ⁡ g ∩ dom ⁡ h
63 62 adantr ⊢ g ∈ B ∧ h ∈ B ∧ a ∈ dom ⁡ g ∩ dom ⁡ h → dom ⁡ g ∩ dom ⁡ h ⊆ A ∧ ∀ a ∈ dom ⁡ g ∩ dom ⁡ h Pred R A a ⊆ dom ⁡ g ∩ dom ⁡ h
64 preddowncl ⊢ dom ⁡ g ∩ dom ⁡ h ⊆ A ∧ ∀ a ∈ dom ⁡ g ∩ dom ⁡ h Pred R A a ⊆ dom ⁡ g ∩ dom ⁡ h → a ∈ dom ⁡ g ∩ dom ⁡ h → Pred R dom ⁡ g ∩ dom ⁡ h a = Pred R A a
65 63 20 64 sylc ⊢ g ∈ B ∧ h ∈ B ∧ a ∈ dom ⁡ g ∩ dom ⁡ h → Pred R dom ⁡ g ∩ dom ⁡ h a = Pred R A a
66 25 65 syl5eq ⊢ g ∈ B ∧ h ∈ B ∧ a ∈ dom ⁡ g ∩ dom ⁡ h → dom ⁡ g ∩ dom ⁡ h ∩ Pred R dom ⁡ g ∩ dom ⁡ h a = Pred R A a
67 66 reseq2d ⊢ g ∈ B ∧ h ∈ B ∧ a ∈ dom ⁡ g ∩ dom ⁡ h → g ↾ dom ⁡ g ∩ dom ⁡ h ∩ Pred R dom ⁡ g ∩ dom ⁡ h a = g ↾ Pred R A a
68 22 67 syl5eq ⊢ g ∈ B ∧ h ∈ B ∧ a ∈ dom ⁡ g ∩ dom ⁡ h → g ↾ dom ⁡ g ∩ dom ⁡ h ↾ Pred R dom ⁡ g ∩ dom ⁡ h a = g ↾ Pred R A a
69 68 oveq2d ⊢ g ∈ B ∧ h ∈ B ∧ a ∈ dom ⁡ g ∩ dom ⁡ h → a G g ↾ dom ⁡ g ∩ dom ⁡ h ↾ Pred R dom ⁡ g ∩ dom ⁡ h a = a G g ↾ Pred R A a
70 19 21 69 3eqtr4d ⊢ g ∈ B ∧ h ∈ B ∧ a ∈ dom ⁡ g ∩ dom ⁡ h → g ↾ dom ⁡ g ∩ dom ⁡ h ⁡ a = a G g ↾ dom ⁡ g ∩ dom ⁡ h ↾ Pred R dom ⁡ g ∩ dom ⁡ h a
71 70 ralrimiva ⊢ g ∈ B ∧ h ∈ B → ∀ a ∈ dom ⁡ g ∩ dom ⁡ h g ↾ dom ⁡ g ∩ dom ⁡ h ⁡ a = a G g ↾ dom ⁡ g ∩ dom ⁡ h ↾ Pred R dom ⁡ g ∩ dom ⁡ h a
72 6 71 jca ⊢ g ∈ B ∧ h ∈ B → g ↾ dom ⁡ g ∩ dom ⁡ h Fn dom ⁡ g ∩ dom ⁡ h ∧ ∀ a ∈ dom ⁡ g ∩ dom ⁡ h g ↾ dom ⁡ g ∩ dom ⁡ h ⁡ a = a G g ↾ dom ⁡ g ∩ dom ⁡ h ↾ Pred R dom ⁡ g ∩ dom ⁡ h a