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

Theorem frrlem4 31908
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 31906 . . . . 5 (𝑔𝐵 → Fun 𝑔)
3 funfn 5956 . . . . 5 (Fun 𝑔𝑔 Fn dom 𝑔)
42, 3sylib 208 . . . 4 (𝑔𝐵𝑔 Fn dom 𝑔)
5 fnresin1 6043 . . . 4 (𝑔 Fn dom 𝑔 → (𝑔 ↾ (dom 𝑔 ∩ dom )) Fn (dom 𝑔 ∩ dom ))
64, 5syl 17 . . 3 (𝑔𝐵 → (𝑔 ↾ (dom 𝑔 ∩ dom )) Fn (dom 𝑔 ∩ dom ))
76adantr 480 . 2 ((𝑔𝐵𝐵) → (𝑔 ↾ (dom 𝑔 ∩ dom )) Fn (dom 𝑔 ∩ dom ))
81frrlem1 31905 . . . . . . . 8 𝐵 = {𝑔 ∣ ∃𝑏(𝑔 Fn 𝑏 ∧ (𝑏𝐴 ∧ ∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎𝑏 (𝑔𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎))))}
98abeq2i 2764 . . . . . . 7 (𝑔𝐵 ↔ ∃𝑏(𝑔 Fn 𝑏 ∧ (𝑏𝐴 ∧ ∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎𝑏 (𝑔𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))))
10 fndm 6028 . . . . . . . . . . . 12 (𝑔 Fn 𝑏 → dom 𝑔 = 𝑏)
1110adantr 480 . . . . . . . . . . 11 ((𝑔 Fn 𝑏 ∧ (𝑏𝐴 ∧ ∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏)) → dom 𝑔 = 𝑏)
1211raleqdv 3174 . . . . . . . . . 10 ((𝑔 Fn 𝑏 ∧ (𝑏𝐴 ∧ ∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏)) → (∀𝑎 ∈ dom 𝑔(𝑔𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎))) ↔ ∀𝑎𝑏 (𝑔𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))))
1312biimp3ar 1473 . . . . . . . . 9 ((𝑔 Fn 𝑏 ∧ (𝑏𝐴 ∧ ∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎𝑏 (𝑔𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) → ∀𝑎 ∈ dom 𝑔(𝑔𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎))))
14 rsp 2958 . . . . . . . . 9 (∀𝑎 ∈ dom 𝑔(𝑔𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎))) → (𝑎 ∈ dom 𝑔 → (𝑔𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))))
1513, 14syl 17 . . . . . . . 8 ((𝑔 Fn 𝑏 ∧ (𝑏𝐴 ∧ ∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎𝑏 (𝑔𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) → (𝑎 ∈ dom 𝑔 → (𝑔𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))))
1615exlimiv 1898 . . . . . . 7 (∃𝑏(𝑔 Fn 𝑏 ∧ (𝑏𝐴 ∧ ∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎𝑏 (𝑔𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) → (𝑎 ∈ dom 𝑔 → (𝑔𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))))
179, 16sylbi 207 . . . . . 6 (𝑔𝐵 → (𝑎 ∈ dom 𝑔 → (𝑔𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))))
18 elinel1 3832 . . . . . 6 (𝑎 ∈ (dom 𝑔 ∩ dom ) → 𝑎 ∈ dom 𝑔)
1917, 18impel 484 . . . . 5 ((𝑔𝐵𝑎 ∈ (dom 𝑔 ∩ dom )) → (𝑔𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎))))
2019adantlr 751 . . . 4 (((𝑔𝐵𝐵) ∧ 𝑎 ∈ (dom 𝑔 ∩ dom )) → (𝑔𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎))))
21 simpr 476 . . . . 5 (((𝑔𝐵𝐵) ∧ 𝑎 ∈ (dom 𝑔 ∩ dom )) → 𝑎 ∈ (dom 𝑔 ∩ dom ))
2221fvresd 6246 . . . 4 (((𝑔𝐵𝐵) ∧ 𝑎 ∈ (dom 𝑔 ∩ dom )) → ((𝑔 ↾ (dom 𝑔 ∩ dom ))‘𝑎) = (𝑔𝑎))
23 resres 5444 . . . . . 6 ((𝑔 ↾ (dom 𝑔 ∩ dom )) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ), 𝑎)) = (𝑔 ↾ ((dom 𝑔 ∩ dom ) ∩ Pred(𝑅, (dom 𝑔 ∩ dom ), 𝑎)))
24 predss 5725 . . . . . . . . 9 Pred(𝑅, (dom 𝑔 ∩ dom ), 𝑎) ⊆ (dom 𝑔 ∩ dom )
25 sseqin2 3850 . . . . . . . . 9 (Pred(𝑅, (dom 𝑔 ∩ dom ), 𝑎) ⊆ (dom 𝑔 ∩ dom ) ↔ ((dom 𝑔 ∩ dom ) ∩ Pred(𝑅, (dom 𝑔 ∩ dom ), 𝑎)) = Pred(𝑅, (dom 𝑔 ∩ dom ), 𝑎))
2624, 25mpbi 220 . . . . . . . 8 ((dom 𝑔 ∩ dom ) ∩ Pred(𝑅, (dom 𝑔 ∩ dom ), 𝑎)) = Pred(𝑅, (dom 𝑔 ∩ dom ), 𝑎)
271frrlem1 31905 . . . . . . . . . . . 12 𝐵 = { ∣ ∃𝑐( Fn 𝑐 ∧ (𝑐𝐴 ∧ ∀𝑎𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) ∧ ∀𝑎𝑐 (𝑎) = (𝑎𝐺( ↾ Pred(𝑅, 𝐴, 𝑎))))}
2827abeq2i 2764 . . . . . . . . . . 11 (𝐵 ↔ ∃𝑐( Fn 𝑐 ∧ (𝑐𝐴 ∧ ∀𝑎𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) ∧ ∀𝑎𝑐 (𝑎) = (𝑎𝐺( ↾ Pred(𝑅, 𝐴, 𝑎)))))
29 eeanv 2218 . . . . . . . . . . . 12 (∃𝑏𝑐((𝑔 Fn 𝑏 ∧ (𝑏𝐴 ∧ ∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎𝑏 (𝑔𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) ∧ ( Fn 𝑐 ∧ (𝑐𝐴 ∧ ∀𝑎𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) ∧ ∀𝑎𝑐 (𝑎) = (𝑎𝐺( ↾ Pred(𝑅, 𝐴, 𝑎))))) ↔ (∃𝑏(𝑔 Fn 𝑏 ∧ (𝑏𝐴 ∧ ∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎𝑏 (𝑔𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) ∧ ∃𝑐( Fn 𝑐 ∧ (𝑐𝐴 ∧ ∀𝑎𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) ∧ ∀𝑎𝑐 (𝑎) = (𝑎𝐺( ↾ Pred(𝑅, 𝐴, 𝑎))))))
30 inss1 3866 . . . . . . . . . . . . . . 15 (𝑏𝑐) ⊆ 𝑏
31 simpl2l 1134 . . . . . . . . . . . . . . 15 (((𝑔 Fn 𝑏 ∧ (𝑏𝐴 ∧ ∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎𝑏 (𝑔𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) ∧ ( Fn 𝑐 ∧ (𝑐𝐴 ∧ ∀𝑎𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) ∧ ∀𝑎𝑐 (𝑎) = (𝑎𝐺( ↾ Pred(𝑅, 𝐴, 𝑎))))) → 𝑏𝐴)
3230, 31syl5ss 3647 . . . . . . . . . . . . . 14 (((𝑔 Fn 𝑏 ∧ (𝑏𝐴 ∧ ∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎𝑏 (𝑔𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) ∧ ( Fn 𝑐 ∧ (𝑐𝐴 ∧ ∀𝑎𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) ∧ ∀𝑎𝑐 (𝑎) = (𝑎𝐺( ↾ Pred(𝑅, 𝐴, 𝑎))))) → (𝑏𝑐) ⊆ 𝐴)
33 simp2r 1108 . . . . . . . . . . . . . . 15 ((𝑔 Fn 𝑏 ∧ (𝑏𝐴 ∧ ∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎𝑏 (𝑔𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) → ∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏)
34 simp2r 1108 . . . . . . . . . . . . . . 15 (( Fn 𝑐 ∧ (𝑐𝐴 ∧ ∀𝑎𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) ∧ ∀𝑎𝑐 (𝑎) = (𝑎𝐺( ↾ Pred(𝑅, 𝐴, 𝑎)))) → ∀𝑎𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐)
35 nfra1 2970 . . . . . . . . . . . . . . . . 17 𝑎𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏
36 nfra1 2970 . . . . . . . . . . . . . . . . 17 𝑎𝑎𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐
3735, 36nfan 1868 . . . . . . . . . . . . . . . 16 𝑎(∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏 ∧ ∀𝑎𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐)
38 elinel1 3832 . . . . . . . . . . . . . . . . . . 19 (𝑎 ∈ (𝑏𝑐) → 𝑎𝑏)
39 rsp 2958 . . . . . . . . . . . . . . . . . . 19 (∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏 → (𝑎𝑏 → Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏))
4038, 39syl5com 31 . . . . . . . . . . . . . . . . . 18 (𝑎 ∈ (𝑏𝑐) → (∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏 → Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏))
41 elinel2 3833 . . . . . . . . . . . . . . . . . . 19 (𝑎 ∈ (𝑏𝑐) → 𝑎𝑐)
42 rsp 2958 . . . . . . . . . . . . . . . . . . 19 (∀𝑎𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐 → (𝑎𝑐 → Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐))
4341, 42syl5com 31 . . . . . . . . . . . . . . . . . 18 (𝑎 ∈ (𝑏𝑐) → (∀𝑎𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐 → Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐))
4440, 43anim12d 585 . . . . . . . . . . . . . . . . 17 (𝑎 ∈ (𝑏𝑐) → ((∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏 ∧ ∀𝑎𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) → (Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏 ∧ Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐)))
45 ssin 3868 . . . . . . . . . . . . . . . . . 18 ((Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏 ∧ Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) ↔ Pred(𝑅, 𝐴, 𝑎) ⊆ (𝑏𝑐))
4645biimpi 206 . . . . . . . . . . . . . . . . 17 ((Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏 ∧ Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) → Pred(𝑅, 𝐴, 𝑎) ⊆ (𝑏𝑐))
4744, 46syl6com 37 . . . . . . . . . . . . . . . 16 ((∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏 ∧ ∀𝑎𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) → (𝑎 ∈ (𝑏𝑐) → Pred(𝑅, 𝐴, 𝑎) ⊆ (𝑏𝑐)))
4837, 47ralrimi 2986 . . . . . . . . . . . . . . 15 ((∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏 ∧ ∀𝑎𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) → ∀𝑎 ∈ (𝑏𝑐)Pred(𝑅, 𝐴, 𝑎) ⊆ (𝑏𝑐))
4933, 34, 48syl2an 493 . . . . . . . . . . . . . 14 (((𝑔 Fn 𝑏 ∧ (𝑏𝐴 ∧ ∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎𝑏 (𝑔𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) ∧ ( Fn 𝑐 ∧ (𝑐𝐴 ∧ ∀𝑎𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) ∧ ∀𝑎𝑐 (𝑎) = (𝑎𝐺( ↾ Pred(𝑅, 𝐴, 𝑎))))) → ∀𝑎 ∈ (𝑏𝑐)Pred(𝑅, 𝐴, 𝑎) ⊆ (𝑏𝑐))
50 simpl1 1084 . . . . . . . . . . . . . . . 16 (((𝑔 Fn 𝑏 ∧ (𝑏𝐴 ∧ ∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎𝑏 (𝑔𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) ∧ ( Fn 𝑐 ∧ (𝑐𝐴 ∧ ∀𝑎𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) ∧ ∀𝑎𝑐 (𝑎) = (𝑎𝐺( ↾ Pred(𝑅, 𝐴, 𝑎))))) → 𝑔 Fn 𝑏)
5150, 10syl 17 . . . . . . . . . . . . . . 15 (((𝑔 Fn 𝑏 ∧ (𝑏𝐴 ∧ ∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎𝑏 (𝑔𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) ∧ ( Fn 𝑐 ∧ (𝑐𝐴 ∧ ∀𝑎𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) ∧ ∀𝑎𝑐 (𝑎) = (𝑎𝐺( ↾ Pred(𝑅, 𝐴, 𝑎))))) → dom 𝑔 = 𝑏)
52 simpr1 1087 . . . . . . . . . . . . . . . 16 (((𝑔 Fn 𝑏 ∧ (𝑏𝐴 ∧ ∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎𝑏 (𝑔𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) ∧ ( Fn 𝑐 ∧ (𝑐𝐴 ∧ ∀𝑎𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) ∧ ∀𝑎𝑐 (𝑎) = (𝑎𝐺( ↾ Pred(𝑅, 𝐴, 𝑎))))) → Fn 𝑐)
53 fndm 6028 . . . . . . . . . . . . . . . 16 ( Fn 𝑐 → dom = 𝑐)
5452, 53syl 17 . . . . . . . . . . . . . . 15 (((𝑔 Fn 𝑏 ∧ (𝑏𝐴 ∧ ∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎𝑏 (𝑔𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) ∧ ( Fn 𝑐 ∧ (𝑐𝐴 ∧ ∀𝑎𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) ∧ ∀𝑎𝑐 (𝑎) = (𝑎𝐺( ↾ Pred(𝑅, 𝐴, 𝑎))))) → dom = 𝑐)
55 ineq12 3842 . . . . . . . . . . . . . . . . 17 ((dom 𝑔 = 𝑏 ∧ dom = 𝑐) → (dom 𝑔 ∩ dom ) = (𝑏𝑐))
5655sseq1d 3665 . . . . . . . . . . . . . . . 16 ((dom 𝑔 = 𝑏 ∧ dom = 𝑐) → ((dom 𝑔 ∩ dom ) ⊆ 𝐴 ↔ (𝑏𝑐) ⊆ 𝐴))
5755sseq2d 3666 . . . . . . . . . . . . . . . . 17 ((dom 𝑔 = 𝑏 ∧ dom = 𝑐) → (Pred(𝑅, 𝐴, 𝑎) ⊆ (dom 𝑔 ∩ dom ) ↔ Pred(𝑅, 𝐴, 𝑎) ⊆ (𝑏𝑐)))
5855, 57raleqbidv 3182 . . . . . . . . . . . . . . . 16 ((dom 𝑔 = 𝑏 ∧ dom = 𝑐) → (∀𝑎 ∈ (dom 𝑔 ∩ dom )Pred(𝑅, 𝐴, 𝑎) ⊆ (dom 𝑔 ∩ dom ) ↔ ∀𝑎 ∈ (𝑏𝑐)Pred(𝑅, 𝐴, 𝑎) ⊆ (𝑏𝑐)))
5956, 58anbi12d 747 . . . . . . . . . . . . . . 15 ((dom 𝑔 = 𝑏 ∧ dom = 𝑐) → (((dom 𝑔 ∩ dom ) ⊆ 𝐴 ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom )Pred(𝑅, 𝐴, 𝑎) ⊆ (dom 𝑔 ∩ dom )) ↔ ((𝑏𝑐) ⊆ 𝐴 ∧ ∀𝑎 ∈ (𝑏𝑐)Pred(𝑅, 𝐴, 𝑎) ⊆ (𝑏𝑐))))
6051, 54, 59syl2anc 694 . . . . . . . . . . . . . 14 (((𝑔 Fn 𝑏 ∧ (𝑏𝐴 ∧ ∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎𝑏 (𝑔𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) ∧ ( Fn 𝑐 ∧ (𝑐𝐴 ∧ ∀𝑎𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) ∧ ∀𝑎𝑐 (𝑎) = (𝑎𝐺( ↾ Pred(𝑅, 𝐴, 𝑎))))) → (((dom 𝑔 ∩ dom ) ⊆ 𝐴 ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom )Pred(𝑅, 𝐴, 𝑎) ⊆ (dom 𝑔 ∩ dom )) ↔ ((𝑏𝑐) ⊆ 𝐴 ∧ ∀𝑎 ∈ (𝑏𝑐)Pred(𝑅, 𝐴, 𝑎) ⊆ (𝑏𝑐))))
6132, 49, 60mpbir2and 977 . . . . . . . . . . . . 13 (((𝑔 Fn 𝑏 ∧ (𝑏𝐴 ∧ ∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎𝑏 (𝑔𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) ∧ ( Fn 𝑐 ∧ (𝑐𝐴 ∧ ∀𝑎𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) ∧ ∀𝑎𝑐 (𝑎) = (𝑎𝐺( ↾ Pred(𝑅, 𝐴, 𝑎))))) → ((dom 𝑔 ∩ dom ) ⊆ 𝐴 ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom )Pred(𝑅, 𝐴, 𝑎) ⊆ (dom 𝑔 ∩ dom )))
6261exlimivv 1900 . . . . . . . . . . . 12 (∃𝑏𝑐((𝑔 Fn 𝑏 ∧ (𝑏𝐴 ∧ ∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎𝑏 (𝑔𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) ∧ ( Fn 𝑐 ∧ (𝑐𝐴 ∧ ∀𝑎𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) ∧ ∀𝑎𝑐 (𝑎) = (𝑎𝐺( ↾ Pred(𝑅, 𝐴, 𝑎))))) → ((dom 𝑔 ∩ dom ) ⊆ 𝐴 ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom )Pred(𝑅, 𝐴, 𝑎) ⊆ (dom 𝑔 ∩ dom )))
6329, 62sylbir 225 . . . . . . . . . . 11 ((∃𝑏(𝑔 Fn 𝑏 ∧ (𝑏𝐴 ∧ ∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎𝑏 (𝑔𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) ∧ ∃𝑐( Fn 𝑐 ∧ (𝑐𝐴 ∧ ∀𝑎𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) ∧ ∀𝑎𝑐 (𝑎) = (𝑎𝐺( ↾ Pred(𝑅, 𝐴, 𝑎))))) → ((dom 𝑔 ∩ dom ) ⊆ 𝐴 ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom )Pred(𝑅, 𝐴, 𝑎) ⊆ (dom 𝑔 ∩ dom )))
649, 28, 63syl2anb 495 . . . . . . . . . 10 ((𝑔𝐵𝐵) → ((dom 𝑔 ∩ dom ) ⊆ 𝐴 ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom )Pred(𝑅, 𝐴, 𝑎) ⊆ (dom 𝑔 ∩ dom )))
6564adantr 480 . . . . . . . . 9 (((𝑔𝐵𝐵) ∧ 𝑎 ∈ (dom 𝑔 ∩ dom )) → ((dom 𝑔 ∩ dom ) ⊆ 𝐴 ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom )Pred(𝑅, 𝐴, 𝑎) ⊆ (dom 𝑔 ∩ dom )))
66 preddowncl 5745 . . . . . . . . 9 (((dom 𝑔 ∩ dom ) ⊆ 𝐴 ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom )Pred(𝑅, 𝐴, 𝑎) ⊆ (dom 𝑔 ∩ dom )) → (𝑎 ∈ (dom 𝑔 ∩ dom ) → Pred(𝑅, (dom 𝑔 ∩ dom ), 𝑎) = Pred(𝑅, 𝐴, 𝑎)))
6765, 21, 66sylc 65 . . . . . . . 8 (((𝑔𝐵𝐵) ∧ 𝑎 ∈ (dom 𝑔 ∩ dom )) → Pred(𝑅, (dom 𝑔 ∩ dom ), 𝑎) = Pred(𝑅, 𝐴, 𝑎))
6826, 67syl5eq 2697 . . . . . . 7 (((𝑔𝐵𝐵) ∧ 𝑎 ∈ (dom 𝑔 ∩ dom )) → ((dom 𝑔 ∩ dom ) ∩ Pred(𝑅, (dom 𝑔 ∩ dom ), 𝑎)) = Pred(𝑅, 𝐴, 𝑎))
6968reseq2d 5428 . . . . . 6 (((𝑔𝐵𝐵) ∧ 𝑎 ∈ (dom 𝑔 ∩ dom )) → (𝑔 ↾ ((dom 𝑔 ∩ dom ) ∩ Pred(𝑅, (dom 𝑔 ∩ dom ), 𝑎))) = (𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))
7023, 69syl5eq 2697 . . . . 5 (((𝑔𝐵𝐵) ∧ 𝑎 ∈ (dom 𝑔 ∩ dom )) → ((𝑔 ↾ (dom 𝑔 ∩ dom )) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ), 𝑎)) = (𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))
7170oveq2d 6706 . . . 4 (((𝑔𝐵𝐵) ∧ 𝑎 ∈ (dom 𝑔 ∩ dom )) → (𝑎𝐺((𝑔 ↾ (dom 𝑔 ∩ dom )) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ), 𝑎))) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎))))
7220, 22, 713eqtr4d 2695 . . 3 (((𝑔𝐵𝐵) ∧ 𝑎 ∈ (dom 𝑔 ∩ dom )) → ((𝑔 ↾ (dom 𝑔 ∩ dom ))‘𝑎) = (𝑎𝐺((𝑔 ↾ (dom 𝑔 ∩ dom )) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ), 𝑎))))
7372ralrimiva 2995 . 2 ((𝑔𝐵𝐵) → ∀𝑎 ∈ (dom 𝑔 ∩ dom )((𝑔 ↾ (dom 𝑔 ∩ dom ))‘𝑎) = (𝑎𝐺((𝑔 ↾ (dom 𝑔 ∩ dom )) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ), 𝑎))))
747, 73jca 553 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 196  wa 383  w3a 1054   = wceq 1523  wex 1744  wcel 2030  {cab 2637  wral 2941  cin 3606  wss 3607  dom cdm 5143  cres 5145  Predcpred 5717  Fun wfun 5920   Fn wfn 5921  cfv 5926  (class class class)co 6690
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pr 4936
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-sbc 3469  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-opab 4746  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-iota 5889  df-fun 5928  df-fn 5929  df-fv 5934  df-ov 6693
This theorem is referenced by:  frrlem5  31909
  Copyright terms: Public domain W3C validator