Mathbox for Scott Fenton < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  frrlem4 Structured version   Visualization version   GIF version

Theorem frrlem4 33186
 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.)
Hypothesis
Ref Expression
frrlem4.1 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}
Assertion
Ref Expression
frrlem4 ((𝑔𝐵𝐵) → ((𝑔 ↾ (dom 𝑔 ∩ dom )) Fn (dom 𝑔 ∩ dom ) ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom )((𝑔 ↾ (dom 𝑔 ∩ dom ))‘𝑎) = (𝑎𝐺((𝑔 ↾ (dom 𝑔 ∩ dom )) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ), 𝑎)))))
Distinct variable groups:   𝐴,𝑎,𝑓,𝑔   𝐴,,𝑥,𝑦,𝑎   𝐵,𝑎   𝑓,,𝑥,𝑦   𝐺,𝑎,𝑓,𝑔   ,𝐺,𝑥,𝑦   𝑥,𝑔,𝑦   𝑅,𝑎,𝑓,𝑔   𝑅,,𝑥,𝑦
Allowed substitution hints:   𝐵(𝑥,𝑦,𝑓,𝑔,)

Proof of Theorem frrlem4
Dummy variables 𝑏 𝑐 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 frrlem4.1 . . . . . 6 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}
21frrlem2 33184 . . . . 5 (𝑔𝐵 → Fun 𝑔)
32funfnd 6374 . . . 4 (𝑔𝐵𝑔 Fn dom 𝑔)
4 fnresin1 6461 . . . 4 (𝑔 Fn dom 𝑔 → (𝑔 ↾ (dom 𝑔 ∩ dom )) Fn (dom 𝑔 ∩ dom ))
53, 4syl 17 . . 3 (𝑔𝐵 → (𝑔 ↾ (dom 𝑔 ∩ dom )) Fn (dom 𝑔 ∩ dom ))
65adantr 484 . 2 ((𝑔𝐵𝐵) → (𝑔 ↾ (dom 𝑔 ∩ dom )) Fn (dom 𝑔 ∩ dom ))
71frrlem1 33183 . . . . . . . 8 𝐵 = {𝑔 ∣ ∃𝑏(𝑔 Fn 𝑏 ∧ (𝑏𝐴 ∧ ∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎𝑏 (𝑔𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎))))}
87abeq2i 2951 . . . . . . 7 (𝑔𝐵 ↔ ∃𝑏(𝑔 Fn 𝑏 ∧ (𝑏𝐴 ∧ ∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎𝑏 (𝑔𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))))
9 fndm 6443 . . . . . . . . . . . 12 (𝑔 Fn 𝑏 → dom 𝑔 = 𝑏)
109adantr 484 . . . . . . . . . . 11 ((𝑔 Fn 𝑏 ∧ (𝑏𝐴 ∧ ∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏)) → dom 𝑔 = 𝑏)
1110raleqdv 3402 . . . . . . . . . 10 ((𝑔 Fn 𝑏 ∧ (𝑏𝐴 ∧ ∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏)) → (∀𝑎 ∈ dom 𝑔(𝑔𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎))) ↔ ∀𝑎𝑏 (𝑔𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))))
1211biimp3ar 1467 . . . . . . . . 9 ((𝑔 Fn 𝑏 ∧ (𝑏𝐴 ∧ ∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎𝑏 (𝑔𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) → ∀𝑎 ∈ dom 𝑔(𝑔𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎))))
13 rsp 3200 . . . . . . . . 9 (∀𝑎 ∈ dom 𝑔(𝑔𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎))) → (𝑎 ∈ dom 𝑔 → (𝑔𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))))
1412, 13syl 17 . . . . . . . 8 ((𝑔 Fn 𝑏 ∧ (𝑏𝐴 ∧ ∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎𝑏 (𝑔𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) → (𝑎 ∈ dom 𝑔 → (𝑔𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))))
1514exlimiv 1932 . . . . . . 7 (∃𝑏(𝑔 Fn 𝑏 ∧ (𝑏𝐴 ∧ ∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎𝑏 (𝑔𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) → (𝑎 ∈ dom 𝑔 → (𝑔𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))))
168, 15sylbi 220 . . . . . 6 (𝑔𝐵 → (𝑎 ∈ dom 𝑔 → (𝑔𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))))
17 elinel1 4157 . . . . . 6 (𝑎 ∈ (dom 𝑔 ∩ dom ) → 𝑎 ∈ dom 𝑔)
1816, 17impel 509 . . . . 5 ((𝑔𝐵𝑎 ∈ (dom 𝑔 ∩ dom )) → (𝑔𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎))))
1918adantlr 714 . . . 4 (((𝑔𝐵𝐵) ∧ 𝑎 ∈ (dom 𝑔 ∩ dom )) → (𝑔𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎))))
20 simpr 488 . . . . 5 (((𝑔𝐵𝐵) ∧ 𝑎 ∈ (dom 𝑔 ∩ dom )) → 𝑎 ∈ (dom 𝑔 ∩ dom ))
2120fvresd 6681 . . . 4 (((𝑔𝐵𝐵) ∧ 𝑎 ∈ (dom 𝑔 ∩ dom )) → ((𝑔 ↾ (dom 𝑔 ∩ dom ))‘𝑎) = (𝑔𝑎))
22 resres 5853 . . . . . 6 ((𝑔 ↾ (dom 𝑔 ∩ dom )) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ), 𝑎)) = (𝑔 ↾ ((dom 𝑔 ∩ dom ) ∩ Pred(𝑅, (dom 𝑔 ∩ dom ), 𝑎)))
23 predss 6142 . . . . . . . . 9 Pred(𝑅, (dom 𝑔 ∩ dom ), 𝑎) ⊆ (dom 𝑔 ∩ dom )
24 sseqin2 4177 . . . . . . . . 9 (Pred(𝑅, (dom 𝑔 ∩ dom ), 𝑎) ⊆ (dom 𝑔 ∩ dom ) ↔ ((dom 𝑔 ∩ dom ) ∩ Pred(𝑅, (dom 𝑔 ∩ dom ), 𝑎)) = Pred(𝑅, (dom 𝑔 ∩ dom ), 𝑎))
2523, 24mpbi 233 . . . . . . . 8 ((dom 𝑔 ∩ dom ) ∩ Pred(𝑅, (dom 𝑔 ∩ dom ), 𝑎)) = Pred(𝑅, (dom 𝑔 ∩ dom ), 𝑎)
261frrlem1 33183 . . . . . . . . . . . 12 𝐵 = { ∣ ∃𝑐( Fn 𝑐 ∧ (𝑐𝐴 ∧ ∀𝑎𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) ∧ ∀𝑎𝑐 (𝑎) = (𝑎𝐺( ↾ Pred(𝑅, 𝐴, 𝑎))))}
2726abeq2i 2951 . . . . . . . . . . 11 (𝐵 ↔ ∃𝑐( Fn 𝑐 ∧ (𝑐𝐴 ∧ ∀𝑎𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) ∧ ∀𝑎𝑐 (𝑎) = (𝑎𝐺( ↾ Pred(𝑅, 𝐴, 𝑎)))))
28 exdistrv 1957 . . . . . . . . . . . 12 (∃𝑏𝑐((𝑔 Fn 𝑏 ∧ (𝑏𝐴 ∧ ∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎𝑏 (𝑔𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) ∧ ( Fn 𝑐 ∧ (𝑐𝐴 ∧ ∀𝑎𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) ∧ ∀𝑎𝑐 (𝑎) = (𝑎𝐺( ↾ Pred(𝑅, 𝐴, 𝑎))))) ↔ (∃𝑏(𝑔 Fn 𝑏 ∧ (𝑏𝐴 ∧ ∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎𝑏 (𝑔𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) ∧ ∃𝑐( Fn 𝑐 ∧ (𝑐𝐴 ∧ ∀𝑎𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) ∧ ∀𝑎𝑐 (𝑎) = (𝑎𝐺( ↾ Pred(𝑅, 𝐴, 𝑎))))))
29 inss1 4190 . . . . . . . . . . . . . . 15 (𝑏𝑐) ⊆ 𝑏
30 simpl2l 1223 . . . . . . . . . . . . . . 15 (((𝑔 Fn 𝑏 ∧ (𝑏𝐴 ∧ ∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎𝑏 (𝑔𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) ∧ ( Fn 𝑐 ∧ (𝑐𝐴 ∧ ∀𝑎𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) ∧ ∀𝑎𝑐 (𝑎) = (𝑎𝐺( ↾ Pred(𝑅, 𝐴, 𝑎))))) → 𝑏𝐴)
3129, 30sstrid 3964 . . . . . . . . . . . . . 14 (((𝑔 Fn 𝑏 ∧ (𝑏𝐴 ∧ ∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎𝑏 (𝑔𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) ∧ ( Fn 𝑐 ∧ (𝑐𝐴 ∧ ∀𝑎𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) ∧ ∀𝑎𝑐 (𝑎) = (𝑎𝐺( ↾ Pred(𝑅, 𝐴, 𝑎))))) → (𝑏𝑐) ⊆ 𝐴)
32 simp2r 1197 . . . . . . . . . . . . . . 15 ((𝑔 Fn 𝑏 ∧ (𝑏𝐴 ∧ ∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎𝑏 (𝑔𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) → ∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏)
33 simp2r 1197 . . . . . . . . . . . . . . 15 (( Fn 𝑐 ∧ (𝑐𝐴 ∧ ∀𝑎𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) ∧ ∀𝑎𝑐 (𝑎) = (𝑎𝐺( ↾ Pred(𝑅, 𝐴, 𝑎)))) → ∀𝑎𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐)
34 nfra1 3213 . . . . . . . . . . . . . . . . 17 𝑎𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏
35 nfra1 3213 . . . . . . . . . . . . . . . . 17 𝑎𝑎𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐
3634, 35nfan 1901 . . . . . . . . . . . . . . . 16 𝑎(∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏 ∧ ∀𝑎𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐)
37 elinel1 4157 . . . . . . . . . . . . . . . . . . 19 (𝑎 ∈ (𝑏𝑐) → 𝑎𝑏)
38 rsp 3200 . . . . . . . . . . . . . . . . . . 19 (∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏 → (𝑎𝑏 → Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏))
3937, 38syl5com 31 . . . . . . . . . . . . . . . . . 18 (𝑎 ∈ (𝑏𝑐) → (∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏 → Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏))
40 elinel2 4158 . . . . . . . . . . . . . . . . . . 19 (𝑎 ∈ (𝑏𝑐) → 𝑎𝑐)
41 rsp 3200 . . . . . . . . . . . . . . . . . . 19 (∀𝑎𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐 → (𝑎𝑐 → Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐))
4240, 41syl5com 31 . . . . . . . . . . . . . . . . . 18 (𝑎 ∈ (𝑏𝑐) → (∀𝑎𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐 → Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐))
4339, 42anim12d 611 . . . . . . . . . . . . . . . . 17 (𝑎 ∈ (𝑏𝑐) → ((∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏 ∧ ∀𝑎𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) → (Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏 ∧ Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐)))
44 ssin 4192 . . . . . . . . . . . . . . . . . 18 ((Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏 ∧ Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) ↔ Pred(𝑅, 𝐴, 𝑎) ⊆ (𝑏𝑐))
4544biimpi 219 . . . . . . . . . . . . . . . . 17 ((Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏 ∧ Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) → Pred(𝑅, 𝐴, 𝑎) ⊆ (𝑏𝑐))
4643, 45syl6com 37 . . . . . . . . . . . . . . . 16 ((∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏 ∧ ∀𝑎𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) → (𝑎 ∈ (𝑏𝑐) → Pred(𝑅, 𝐴, 𝑎) ⊆ (𝑏𝑐)))
4736, 46ralrimi 3210 . . . . . . . . . . . . . . 15 ((∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏 ∧ ∀𝑎𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) → ∀𝑎 ∈ (𝑏𝑐)Pred(𝑅, 𝐴, 𝑎) ⊆ (𝑏𝑐))
4832, 33, 47syl2an 598 . . . . . . . . . . . . . 14 (((𝑔 Fn 𝑏 ∧ (𝑏𝐴 ∧ ∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎𝑏 (𝑔𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) ∧ ( Fn 𝑐 ∧ (𝑐𝐴 ∧ ∀𝑎𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) ∧ ∀𝑎𝑐 (𝑎) = (𝑎𝐺( ↾ Pred(𝑅, 𝐴, 𝑎))))) → ∀𝑎 ∈ (𝑏𝑐)Pred(𝑅, 𝐴, 𝑎) ⊆ (𝑏𝑐))
49 simpl1 1188 . . . . . . . . . . . . . . . 16 (((𝑔 Fn 𝑏 ∧ (𝑏𝐴 ∧ ∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎𝑏 (𝑔𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) ∧ ( Fn 𝑐 ∧ (𝑐𝐴 ∧ ∀𝑎𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) ∧ ∀𝑎𝑐 (𝑎) = (𝑎𝐺( ↾ Pred(𝑅, 𝐴, 𝑎))))) → 𝑔 Fn 𝑏)
5049fndmd 6445 . . . . . . . . . . . . . . 15 (((𝑔 Fn 𝑏 ∧ (𝑏𝐴 ∧ ∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎𝑏 (𝑔𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) ∧ ( Fn 𝑐 ∧ (𝑐𝐴 ∧ ∀𝑎𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) ∧ ∀𝑎𝑐 (𝑎) = (𝑎𝐺( ↾ Pred(𝑅, 𝐴, 𝑎))))) → dom 𝑔 = 𝑏)
51 simpr1 1191 . . . . . . . . . . . . . . . 16 (((𝑔 Fn 𝑏 ∧ (𝑏𝐴 ∧ ∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎𝑏 (𝑔𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) ∧ ( Fn 𝑐 ∧ (𝑐𝐴 ∧ ∀𝑎𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) ∧ ∀𝑎𝑐 (𝑎) = (𝑎𝐺( ↾ Pred(𝑅, 𝐴, 𝑎))))) → Fn 𝑐)
5251fndmd 6445 . . . . . . . . . . . . . . 15 (((𝑔 Fn 𝑏 ∧ (𝑏𝐴 ∧ ∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎𝑏 (𝑔𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) ∧ ( Fn 𝑐 ∧ (𝑐𝐴 ∧ ∀𝑎𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) ∧ ∀𝑎𝑐 (𝑎) = (𝑎𝐺( ↾ Pred(𝑅, 𝐴, 𝑎))))) → dom = 𝑐)
53 ineq12 4169 . . . . . . . . . . . . . . . . 17 ((dom 𝑔 = 𝑏 ∧ dom = 𝑐) → (dom 𝑔 ∩ dom ) = (𝑏𝑐))
5453sseq1d 3984 . . . . . . . . . . . . . . . 16 ((dom 𝑔 = 𝑏 ∧ dom = 𝑐) → ((dom 𝑔 ∩ dom ) ⊆ 𝐴 ↔ (𝑏𝑐) ⊆ 𝐴))
5553sseq2d 3985 . . . . . . . . . . . . . . . . 17 ((dom 𝑔 = 𝑏 ∧ dom = 𝑐) → (Pred(𝑅, 𝐴, 𝑎) ⊆ (dom 𝑔 ∩ dom ) ↔ Pred(𝑅, 𝐴, 𝑎) ⊆ (𝑏𝑐)))
5653, 55raleqbidv 3392 . . . . . . . . . . . . . . . 16 ((dom 𝑔 = 𝑏 ∧ dom = 𝑐) → (∀𝑎 ∈ (dom 𝑔 ∩ dom )Pred(𝑅, 𝐴, 𝑎) ⊆ (dom 𝑔 ∩ dom ) ↔ ∀𝑎 ∈ (𝑏𝑐)Pred(𝑅, 𝐴, 𝑎) ⊆ (𝑏𝑐)))
5754, 56anbi12d 633 . . . . . . . . . . . . . . 15 ((dom 𝑔 = 𝑏 ∧ dom = 𝑐) → (((dom 𝑔 ∩ dom ) ⊆ 𝐴 ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom )Pred(𝑅, 𝐴, 𝑎) ⊆ (dom 𝑔 ∩ dom )) ↔ ((𝑏𝑐) ⊆ 𝐴 ∧ ∀𝑎 ∈ (𝑏𝑐)Pred(𝑅, 𝐴, 𝑎) ⊆ (𝑏𝑐))))
5850, 52, 57syl2anc 587 . . . . . . . . . . . . . 14 (((𝑔 Fn 𝑏 ∧ (𝑏𝐴 ∧ ∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎𝑏 (𝑔𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) ∧ ( Fn 𝑐 ∧ (𝑐𝐴 ∧ ∀𝑎𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) ∧ ∀𝑎𝑐 (𝑎) = (𝑎𝐺( ↾ Pred(𝑅, 𝐴, 𝑎))))) → (((dom 𝑔 ∩ dom ) ⊆ 𝐴 ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom )Pred(𝑅, 𝐴, 𝑎) ⊆ (dom 𝑔 ∩ dom )) ↔ ((𝑏𝑐) ⊆ 𝐴 ∧ ∀𝑎 ∈ (𝑏𝑐)Pred(𝑅, 𝐴, 𝑎) ⊆ (𝑏𝑐))))
5931, 48, 58mpbir2and 712 . . . . . . . . . . . . 13 (((𝑔 Fn 𝑏 ∧ (𝑏𝐴 ∧ ∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎𝑏 (𝑔𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) ∧ ( Fn 𝑐 ∧ (𝑐𝐴 ∧ ∀𝑎𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) ∧ ∀𝑎𝑐 (𝑎) = (𝑎𝐺( ↾ Pred(𝑅, 𝐴, 𝑎))))) → ((dom 𝑔 ∩ dom ) ⊆ 𝐴 ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom )Pred(𝑅, 𝐴, 𝑎) ⊆ (dom 𝑔 ∩ dom )))
6059exlimivv 1934 . . . . . . . . . . . 12 (∃𝑏𝑐((𝑔 Fn 𝑏 ∧ (𝑏𝐴 ∧ ∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎𝑏 (𝑔𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) ∧ ( Fn 𝑐 ∧ (𝑐𝐴 ∧ ∀𝑎𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) ∧ ∀𝑎𝑐 (𝑎) = (𝑎𝐺( ↾ Pred(𝑅, 𝐴, 𝑎))))) → ((dom 𝑔 ∩ dom ) ⊆ 𝐴 ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom )Pred(𝑅, 𝐴, 𝑎) ⊆ (dom 𝑔 ∩ dom )))
6128, 60sylbir 238 . . . . . . . . . . 11 ((∃𝑏(𝑔 Fn 𝑏 ∧ (𝑏𝐴 ∧ ∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎𝑏 (𝑔𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) ∧ ∃𝑐( Fn 𝑐 ∧ (𝑐𝐴 ∧ ∀𝑎𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) ∧ ∀𝑎𝑐 (𝑎) = (𝑎𝐺( ↾ Pred(𝑅, 𝐴, 𝑎))))) → ((dom 𝑔 ∩ dom ) ⊆ 𝐴 ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom )Pred(𝑅, 𝐴, 𝑎) ⊆ (dom 𝑔 ∩ dom )))
628, 27, 61syl2anb 600 . . . . . . . . . 10 ((𝑔𝐵𝐵) → ((dom 𝑔 ∩ dom ) ⊆ 𝐴 ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom )Pred(𝑅, 𝐴, 𝑎) ⊆ (dom 𝑔 ∩ dom )))
6362adantr 484 . . . . . . . . 9 (((𝑔𝐵𝐵) ∧ 𝑎 ∈ (dom 𝑔 ∩ dom )) → ((dom 𝑔 ∩ dom ) ⊆ 𝐴 ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom )Pred(𝑅, 𝐴, 𝑎) ⊆ (dom 𝑔 ∩ dom )))
64 preddowncl 6162 . . . . . . . . 9 (((dom 𝑔 ∩ dom ) ⊆ 𝐴 ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom )Pred(𝑅, 𝐴, 𝑎) ⊆ (dom 𝑔 ∩ dom )) → (𝑎 ∈ (dom 𝑔 ∩ dom ) → Pred(𝑅, (dom 𝑔 ∩ dom ), 𝑎) = Pred(𝑅, 𝐴, 𝑎)))
6563, 20, 64sylc 65 . . . . . . . 8 (((𝑔𝐵𝐵) ∧ 𝑎 ∈ (dom 𝑔 ∩ dom )) → Pred(𝑅, (dom 𝑔 ∩ dom ), 𝑎) = Pred(𝑅, 𝐴, 𝑎))
6625, 65syl5eq 2871 . . . . . . 7 (((𝑔𝐵𝐵) ∧ 𝑎 ∈ (dom 𝑔 ∩ dom )) → ((dom 𝑔 ∩ dom ) ∩ Pred(𝑅, (dom 𝑔 ∩ dom ), 𝑎)) = Pred(𝑅, 𝐴, 𝑎))
6766reseq2d 5840 . . . . . 6 (((𝑔𝐵𝐵) ∧ 𝑎 ∈ (dom 𝑔 ∩ dom )) → (𝑔 ↾ ((dom 𝑔 ∩ dom ) ∩ Pred(𝑅, (dom 𝑔 ∩ dom ), 𝑎))) = (𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))
6822, 67syl5eq 2871 . . . . 5 (((𝑔𝐵𝐵) ∧ 𝑎 ∈ (dom 𝑔 ∩ dom )) → ((𝑔 ↾ (dom 𝑔 ∩ dom )) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ), 𝑎)) = (𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))
6968oveq2d 7165 . . . 4 (((𝑔𝐵𝐵) ∧ 𝑎 ∈ (dom 𝑔 ∩ dom )) → (𝑎𝐺((𝑔 ↾ (dom 𝑔 ∩ dom )) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ), 𝑎))) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎))))
7019, 21, 693eqtr4d 2869 . . 3 (((𝑔𝐵𝐵) ∧ 𝑎 ∈ (dom 𝑔 ∩ dom )) → ((𝑔 ↾ (dom 𝑔 ∩ dom ))‘𝑎) = (𝑎𝐺((𝑔 ↾ (dom 𝑔 ∩ dom )) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ), 𝑎))))
7170ralrimiva 3177 . 2 ((𝑔𝐵𝐵) → ∀𝑎 ∈ (dom 𝑔 ∩ dom )((𝑔 ↾ (dom 𝑔 ∩ dom ))‘𝑎) = (𝑎𝐺((𝑔 ↾ (dom 𝑔 ∩ dom )) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ), 𝑎))))
726, 71jca 515 1 ((𝑔𝐵𝐵) → ((𝑔 ↾ (dom 𝑔 ∩ dom )) Fn (dom 𝑔 ∩ dom ) ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom )((𝑔 ↾ (dom 𝑔 ∩ dom ))‘𝑎) = (𝑎𝐺((𝑔 ↾ (dom 𝑔 ∩ dom )) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ), 𝑎)))))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538  ∃wex 1781   ∈ wcel 2115  {cab 2802  ∀wral 3133   ∩ cin 3918   ⊆ wss 3919  dom cdm 5542   ↾ cres 5544  Predcpred 6134   Fn wfn 6338  ‘cfv 6343  (class class class)co 7149 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-sep 5189  ax-nul 5196  ax-pr 5317 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ral 3138  df-rex 3139  df-rab 3142  df-v 3482  df-sbc 3759  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-nul 4277  df-if 4451  df-sn 4551  df-pr 4553  df-op 4557  df-uni 4825  df-br 5053  df-opab 5115  df-xp 5548  df-rel 5549  df-cnv 5550  df-co 5551  df-dm 5552  df-rn 5553  df-res 5554  df-ima 5555  df-pred 6135  df-iota 6302  df-fun 6345  df-fn 6346  df-fv 6351  df-ov 7152 This theorem is referenced by:  fprlem1  33197  frrlem15  33202
 Copyright terms: Public domain W3C validator