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 31027
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 31025 . . . . 5 (𝑔𝐵 → Fun 𝑔)
3 funfn 5833 . . . . 5 (Fun 𝑔𝑔 Fn dom 𝑔)
42, 3sylib 207 . . . 4 (𝑔𝐵𝑔 Fn dom 𝑔)
5 fnresin1 5919 . . . 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 ))
8 inss1 3795 . . . . . . . 8 (dom 𝑔 ∩ dom ) ⊆ dom 𝑔
98sseli 3564 . . . . . . 7 (𝑎 ∈ (dom 𝑔 ∩ dom ) → 𝑎 ∈ dom 𝑔)
101frrlem1 31024 . . . . . . . . 9 𝐵 = {𝑔 ∣ ∃𝑏(𝑔 Fn 𝑏 ∧ (𝑏𝐴 ∧ ∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏 ∧ ∀𝑎𝑏 (𝑔𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))))}
1110abeq2i 2722 . . . . . . . 8 (𝑔𝐵 ↔ ∃𝑏(𝑔 Fn 𝑏 ∧ (𝑏𝐴 ∧ ∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏 ∧ ∀𝑎𝑏 (𝑔𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎))))))
12 fndm 5904 . . . . . . . . . 10 (𝑔 Fn 𝑏 → dom 𝑔 = 𝑏)
13 rsp 2913 . . . . . . . . . . . 12 (∀𝑎𝑏 (𝑔𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎))) → (𝑎𝑏 → (𝑔𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))))
14133ad2ant3 1077 . . . . . . . . . . 11 ((𝑏𝐴 ∧ ∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏 ∧ ∀𝑎𝑏 (𝑔𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) → (𝑎𝑏 → (𝑔𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))))
15 eleq2 2677 . . . . . . . . . . . 12 (dom 𝑔 = 𝑏 → (𝑎 ∈ dom 𝑔𝑎𝑏))
1615imbi1d 330 . . . . . . . . . . 11 (dom 𝑔 = 𝑏 → ((𝑎 ∈ dom 𝑔 → (𝑔𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) ↔ (𝑎𝑏 → (𝑔𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎))))))
1714, 16syl5ibrcom 236 . . . . . . . . . 10 ((𝑏𝐴 ∧ ∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏 ∧ ∀𝑎𝑏 (𝑔𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) → (dom 𝑔 = 𝑏 → (𝑎 ∈ dom 𝑔 → (𝑔𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎))))))
1812, 17mpan9 485 . . . . . . . . 9 ((𝑔 Fn 𝑏 ∧ (𝑏𝐴 ∧ ∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏 ∧ ∀𝑎𝑏 (𝑔𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎))))) → (𝑎 ∈ dom 𝑔 → (𝑔𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))))
1918exlimiv 1845 . . . . . . . 8 (∃𝑏(𝑔 Fn 𝑏 ∧ (𝑏𝐴 ∧ ∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏 ∧ ∀𝑎𝑏 (𝑔𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎))))) → (𝑎 ∈ dom 𝑔 → (𝑔𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))))
2011, 19sylbi 206 . . . . . . 7 (𝑔𝐵 → (𝑎 ∈ dom 𝑔 → (𝑔𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))))
219, 20syl5 33 . . . . . 6 (𝑔𝐵 → (𝑎 ∈ (dom 𝑔 ∩ dom ) → (𝑔𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))))
2221imp 444 . . . . 5 ((𝑔𝐵𝑎 ∈ (dom 𝑔 ∩ dom )) → (𝑔𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎))))
2322adantlr 747 . . . 4 (((𝑔𝐵𝐵) ∧ 𝑎 ∈ (dom 𝑔 ∩ dom )) → (𝑔𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎))))
24 fvres 6117 . . . . 5 (𝑎 ∈ (dom 𝑔 ∩ dom ) → ((𝑔 ↾ (dom 𝑔 ∩ dom ))‘𝑎) = (𝑔𝑎))
2524adantl 481 . . . 4 (((𝑔𝐵𝐵) ∧ 𝑎 ∈ (dom 𝑔 ∩ dom )) → ((𝑔 ↾ (dom 𝑔 ∩ dom ))‘𝑎) = (𝑔𝑎))
26 resres 5329 . . . . . 6 ((𝑔 ↾ (dom 𝑔 ∩ dom )) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ), 𝑎)) = (𝑔 ↾ ((dom 𝑔 ∩ dom ) ∩ Pred(𝑅, (dom 𝑔 ∩ dom ), 𝑎)))
27 predss 5604 . . . . . . . . 9 Pred(𝑅, (dom 𝑔 ∩ dom ), 𝑎) ⊆ (dom 𝑔 ∩ dom )
28 sseqin2 3779 . . . . . . . . 9 (Pred(𝑅, (dom 𝑔 ∩ dom ), 𝑎) ⊆ (dom 𝑔 ∩ dom ) ↔ ((dom 𝑔 ∩ dom ) ∩ Pred(𝑅, (dom 𝑔 ∩ dom ), 𝑎)) = Pred(𝑅, (dom 𝑔 ∩ dom ), 𝑎))
2927, 28mpbi 219 . . . . . . . 8 ((dom 𝑔 ∩ dom ) ∩ Pred(𝑅, (dom 𝑔 ∩ dom ), 𝑎)) = Pred(𝑅, (dom 𝑔 ∩ dom ), 𝑎)
301frrlem1 31024 . . . . . . . . . . . 12 𝐵 = { ∣ ∃𝑐( Fn 𝑐 ∧ (𝑐𝐴 ∧ ∀𝑎𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐 ∧ ∀𝑎𝑐 (𝑎) = (𝑎𝐺( ↾ Pred(𝑅, 𝐴, 𝑎)))))}
3130abeq2i 2722 . . . . . . . . . . 11 (𝐵 ↔ ∃𝑐( Fn 𝑐 ∧ (𝑐𝐴 ∧ ∀𝑎𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐 ∧ ∀𝑎𝑐 (𝑎) = (𝑎𝐺( ↾ Pred(𝑅, 𝐴, 𝑎))))))
32 eeanv 2170 . . . . . . . . . . . 12 (∃𝑏𝑐((𝑔 Fn 𝑏 ∧ (𝑏𝐴 ∧ ∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏 ∧ ∀𝑎𝑏 (𝑔𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎))))) ∧ ( Fn 𝑐 ∧ (𝑐𝐴 ∧ ∀𝑎𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐 ∧ ∀𝑎𝑐 (𝑎) = (𝑎𝐺( ↾ Pred(𝑅, 𝐴, 𝑎)))))) ↔ (∃𝑏(𝑔 Fn 𝑏 ∧ (𝑏𝐴 ∧ ∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏 ∧ ∀𝑎𝑏 (𝑔𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎))))) ∧ ∃𝑐( Fn 𝑐 ∧ (𝑐𝐴 ∧ ∀𝑎𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐 ∧ ∀𝑎𝑐 (𝑎) = (𝑎𝐺( ↾ Pred(𝑅, 𝐴, 𝑎)))))))
33 simpl1 1057 . . . . . . . . . . . . . . . . 17 (((𝑏𝐴 ∧ ∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏 ∧ ∀𝑎𝑏 (𝑔𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) ∧ (𝑐𝐴 ∧ ∀𝑎𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐 ∧ ∀𝑎𝑐 (𝑎) = (𝑎𝐺( ↾ Pred(𝑅, 𝐴, 𝑎))))) → 𝑏𝐴)
34 ssinss1 3803 . . . . . . . . . . . . . . . . 17 (𝑏𝐴 → (𝑏𝑐) ⊆ 𝐴)
3533, 34syl 17 . . . . . . . . . . . . . . . 16 (((𝑏𝐴 ∧ ∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏 ∧ ∀𝑎𝑏 (𝑔𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) ∧ (𝑐𝐴 ∧ ∀𝑎𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐 ∧ ∀𝑎𝑐 (𝑎) = (𝑎𝐺( ↾ Pred(𝑅, 𝐴, 𝑎))))) → (𝑏𝑐) ⊆ 𝐴)
36 simpl2 1058 . . . . . . . . . . . . . . . . 17 (((𝑏𝐴 ∧ ∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏 ∧ ∀𝑎𝑏 (𝑔𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) ∧ (𝑐𝐴 ∧ ∀𝑎𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐 ∧ ∀𝑎𝑐 (𝑎) = (𝑎𝐺( ↾ Pred(𝑅, 𝐴, 𝑎))))) → ∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏)
37 simpr2 1061 . . . . . . . . . . . . . . . . 17 (((𝑏𝐴 ∧ ∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏 ∧ ∀𝑎𝑏 (𝑔𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) ∧ (𝑐𝐴 ∧ ∀𝑎𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐 ∧ ∀𝑎𝑐 (𝑎) = (𝑎𝐺( ↾ Pred(𝑅, 𝐴, 𝑎))))) → ∀𝑎𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐)
38 nfra1 2925 . . . . . . . . . . . . . . . . . . 19 𝑎𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏
39 nfra1 2925 . . . . . . . . . . . . . . . . . . 19 𝑎𝑎𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐
4038, 39nfan 1816 . . . . . . . . . . . . . . . . . 18 𝑎(∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏 ∧ ∀𝑎𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐)
41 inss1 3795 . . . . . . . . . . . . . . . . . . . . . 22 (𝑏𝑐) ⊆ 𝑏
4241sseli 3564 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 ∈ (𝑏𝑐) → 𝑎𝑏)
43 rsp 2913 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏 → (𝑎𝑏 → Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏))
4442, 43syl5com 31 . . . . . . . . . . . . . . . . . . . 20 (𝑎 ∈ (𝑏𝑐) → (∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏 → Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏))
45 inss2 3796 . . . . . . . . . . . . . . . . . . . . . 22 (𝑏𝑐) ⊆ 𝑐
4645sseli 3564 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 ∈ (𝑏𝑐) → 𝑎𝑐)
47 rsp 2913 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑎𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐 → (𝑎𝑐 → Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐))
4846, 47syl5com 31 . . . . . . . . . . . . . . . . . . . 20 (𝑎 ∈ (𝑏𝑐) → (∀𝑎𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐 → Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐))
4944, 48anim12d 584 . . . . . . . . . . . . . . . . . . 19 (𝑎 ∈ (𝑏𝑐) → ((∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏 ∧ ∀𝑎𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) → (Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏 ∧ Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐)))
50 ssin 3797 . . . . . . . . . . . . . . . . . . . 20 ((Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏 ∧ Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) ↔ Pred(𝑅, 𝐴, 𝑎) ⊆ (𝑏𝑐))
5150biimpi 205 . . . . . . . . . . . . . . . . . . 19 ((Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏 ∧ Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) → Pred(𝑅, 𝐴, 𝑎) ⊆ (𝑏𝑐))
5249, 51syl6com 36 . . . . . . . . . . . . . . . . . 18 ((∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏 ∧ ∀𝑎𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) → (𝑎 ∈ (𝑏𝑐) → Pred(𝑅, 𝐴, 𝑎) ⊆ (𝑏𝑐)))
5340, 52ralrimi 2940 . . . . . . . . . . . . . . . . 17 ((∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏 ∧ ∀𝑎𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) → ∀𝑎 ∈ (𝑏𝑐)Pred(𝑅, 𝐴, 𝑎) ⊆ (𝑏𝑐))
5436, 37, 53syl2anc 691 . . . . . . . . . . . . . . . 16 (((𝑏𝐴 ∧ ∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏 ∧ ∀𝑎𝑏 (𝑔𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) ∧ (𝑐𝐴 ∧ ∀𝑎𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐 ∧ ∀𝑎𝑐 (𝑎) = (𝑎𝐺( ↾ Pred(𝑅, 𝐴, 𝑎))))) → ∀𝑎 ∈ (𝑏𝑐)Pred(𝑅, 𝐴, 𝑎) ⊆ (𝑏𝑐))
55 fndm 5904 . . . . . . . . . . . . . . . . . 18 ( Fn 𝑐 → dom = 𝑐)
56 ineq12 3771 . . . . . . . . . . . . . . . . . . . 20 ((dom 𝑔 = 𝑏 ∧ dom = 𝑐) → (dom 𝑔 ∩ dom ) = (𝑏𝑐))
5756sseq1d 3595 . . . . . . . . . . . . . . . . . . 19 ((dom 𝑔 = 𝑏 ∧ dom = 𝑐) → ((dom 𝑔 ∩ dom ) ⊆ 𝐴 ↔ (𝑏𝑐) ⊆ 𝐴))
58 sseq2 3590 . . . . . . . . . . . . . . . . . . . . 21 ((dom 𝑔 ∩ dom ) = (𝑏𝑐) → (Pred(𝑅, 𝐴, 𝑎) ⊆ (dom 𝑔 ∩ dom ) ↔ Pred(𝑅, 𝐴, 𝑎) ⊆ (𝑏𝑐)))
5958raleqbi1dv 3123 . . . . . . . . . . . . . . . . . . . 20 ((dom 𝑔 ∩ dom ) = (𝑏𝑐) → (∀𝑎 ∈ (dom 𝑔 ∩ dom )Pred(𝑅, 𝐴, 𝑎) ⊆ (dom 𝑔 ∩ dom ) ↔ ∀𝑎 ∈ (𝑏𝑐)Pred(𝑅, 𝐴, 𝑎) ⊆ (𝑏𝑐)))
6056, 59syl 17 . . . . . . . . . . . . . . . . . . 19 ((dom 𝑔 = 𝑏 ∧ dom = 𝑐) → (∀𝑎 ∈ (dom 𝑔 ∩ dom )Pred(𝑅, 𝐴, 𝑎) ⊆ (dom 𝑔 ∩ dom ) ↔ ∀𝑎 ∈ (𝑏𝑐)Pred(𝑅, 𝐴, 𝑎) ⊆ (𝑏𝑐)))
6157, 60anbi12d 743 . . . . . . . . . . . . . . . . . 18 ((dom 𝑔 = 𝑏 ∧ dom = 𝑐) → (((dom 𝑔 ∩ dom ) ⊆ 𝐴 ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom )Pred(𝑅, 𝐴, 𝑎) ⊆ (dom 𝑔 ∩ dom )) ↔ ((𝑏𝑐) ⊆ 𝐴 ∧ ∀𝑎 ∈ (𝑏𝑐)Pred(𝑅, 𝐴, 𝑎) ⊆ (𝑏𝑐))))
6212, 55, 61syl2an 493 . . . . . . . . . . . . . . . . 17 ((𝑔 Fn 𝑏 Fn 𝑐) → (((dom 𝑔 ∩ dom ) ⊆ 𝐴 ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom )Pred(𝑅, 𝐴, 𝑎) ⊆ (dom 𝑔 ∩ dom )) ↔ ((𝑏𝑐) ⊆ 𝐴 ∧ ∀𝑎 ∈ (𝑏𝑐)Pred(𝑅, 𝐴, 𝑎) ⊆ (𝑏𝑐))))
6362biimprcd 239 . . . . . . . . . . . . . . . 16 (((𝑏𝑐) ⊆ 𝐴 ∧ ∀𝑎 ∈ (𝑏𝑐)Pred(𝑅, 𝐴, 𝑎) ⊆ (𝑏𝑐)) → ((𝑔 Fn 𝑏 Fn 𝑐) → ((dom 𝑔 ∩ dom ) ⊆ 𝐴 ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom )Pred(𝑅, 𝐴, 𝑎) ⊆ (dom 𝑔 ∩ dom ))))
6435, 54, 63syl2anc 691 . . . . . . . . . . . . . . 15 (((𝑏𝐴 ∧ ∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏 ∧ ∀𝑎𝑏 (𝑔𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) ∧ (𝑐𝐴 ∧ ∀𝑎𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐 ∧ ∀𝑎𝑐 (𝑎) = (𝑎𝐺( ↾ Pred(𝑅, 𝐴, 𝑎))))) → ((𝑔 Fn 𝑏 Fn 𝑐) → ((dom 𝑔 ∩ dom ) ⊆ 𝐴 ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom )Pred(𝑅, 𝐴, 𝑎) ⊆ (dom 𝑔 ∩ dom ))))
6564impcom 445 . . . . . . . . . . . . . 14 (((𝑔 Fn 𝑏 Fn 𝑐) ∧ ((𝑏𝐴 ∧ ∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏 ∧ ∀𝑎𝑏 (𝑔𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) ∧ (𝑐𝐴 ∧ ∀𝑎𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐 ∧ ∀𝑎𝑐 (𝑎) = (𝑎𝐺( ↾ Pred(𝑅, 𝐴, 𝑎)))))) → ((dom 𝑔 ∩ dom ) ⊆ 𝐴 ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom )Pred(𝑅, 𝐴, 𝑎) ⊆ (dom 𝑔 ∩ dom )))
6665an4s 865 . . . . . . . . . . . . 13 (((𝑔 Fn 𝑏 ∧ (𝑏𝐴 ∧ ∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏 ∧ ∀𝑎𝑏 (𝑔𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎))))) ∧ ( Fn 𝑐 ∧ (𝑐𝐴 ∧ ∀𝑎𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐 ∧ ∀𝑎𝑐 (𝑎) = (𝑎𝐺( ↾ Pred(𝑅, 𝐴, 𝑎)))))) → ((dom 𝑔 ∩ dom ) ⊆ 𝐴 ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom )Pred(𝑅, 𝐴, 𝑎) ⊆ (dom 𝑔 ∩ dom )))
6766exlimivv 1847 . . . . . . . . . . . 12 (∃𝑏𝑐((𝑔 Fn 𝑏 ∧ (𝑏𝐴 ∧ ∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏 ∧ ∀𝑎𝑏 (𝑔𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎))))) ∧ ( Fn 𝑐 ∧ (𝑐𝐴 ∧ ∀𝑎𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐 ∧ ∀𝑎𝑐 (𝑎) = (𝑎𝐺( ↾ Pred(𝑅, 𝐴, 𝑎)))))) → ((dom 𝑔 ∩ dom ) ⊆ 𝐴 ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom )Pred(𝑅, 𝐴, 𝑎) ⊆ (dom 𝑔 ∩ dom )))
6832, 67sylbir 224 . . . . . . . . . . 11 ((∃𝑏(𝑔 Fn 𝑏 ∧ (𝑏𝐴 ∧ ∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏 ∧ ∀𝑎𝑏 (𝑔𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎))))) ∧ ∃𝑐( Fn 𝑐 ∧ (𝑐𝐴 ∧ ∀𝑎𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐 ∧ ∀𝑎𝑐 (𝑎) = (𝑎𝐺( ↾ Pred(𝑅, 𝐴, 𝑎)))))) → ((dom 𝑔 ∩ dom ) ⊆ 𝐴 ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom )Pred(𝑅, 𝐴, 𝑎) ⊆ (dom 𝑔 ∩ dom )))
6911, 31, 68syl2anb 495 . . . . . . . . . 10 ((𝑔𝐵𝐵) → ((dom 𝑔 ∩ dom ) ⊆ 𝐴 ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom )Pred(𝑅, 𝐴, 𝑎) ⊆ (dom 𝑔 ∩ dom )))
7069adantr 480 . . . . . . . . 9 (((𝑔𝐵𝐵) ∧ 𝑎 ∈ (dom 𝑔 ∩ dom )) → ((dom 𝑔 ∩ dom ) ⊆ 𝐴 ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom )Pred(𝑅, 𝐴, 𝑎) ⊆ (dom 𝑔 ∩ dom )))
71 simpr 476 . . . . . . . . 9 (((𝑔𝐵𝐵) ∧ 𝑎 ∈ (dom 𝑔 ∩ dom )) → 𝑎 ∈ (dom 𝑔 ∩ dom ))
72 preddowncl 5624 . . . . . . . . 9 (((dom 𝑔 ∩ dom ) ⊆ 𝐴 ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom )Pred(𝑅, 𝐴, 𝑎) ⊆ (dom 𝑔 ∩ dom )) → (𝑎 ∈ (dom 𝑔 ∩ dom ) → Pred(𝑅, (dom 𝑔 ∩ dom ), 𝑎) = Pred(𝑅, 𝐴, 𝑎)))
7370, 71, 72sylc 63 . . . . . . . 8 (((𝑔𝐵𝐵) ∧ 𝑎 ∈ (dom 𝑔 ∩ dom )) → Pred(𝑅, (dom 𝑔 ∩ dom ), 𝑎) = Pred(𝑅, 𝐴, 𝑎))
7429, 73syl5eq 2656 . . . . . . 7 (((𝑔𝐵𝐵) ∧ 𝑎 ∈ (dom 𝑔 ∩ dom )) → ((dom 𝑔 ∩ dom ) ∩ Pred(𝑅, (dom 𝑔 ∩ dom ), 𝑎)) = Pred(𝑅, 𝐴, 𝑎))
7574reseq2d 5317 . . . . . 6 (((𝑔𝐵𝐵) ∧ 𝑎 ∈ (dom 𝑔 ∩ dom )) → (𝑔 ↾ ((dom 𝑔 ∩ dom ) ∩ Pred(𝑅, (dom 𝑔 ∩ dom ), 𝑎))) = (𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))
7626, 75syl5eq 2656 . . . . 5 (((𝑔𝐵𝐵) ∧ 𝑎 ∈ (dom 𝑔 ∩ dom )) → ((𝑔 ↾ (dom 𝑔 ∩ dom )) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ), 𝑎)) = (𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))
7776oveq2d 6565 . . . 4 (((𝑔𝐵𝐵) ∧ 𝑎 ∈ (dom 𝑔 ∩ dom )) → (𝑎𝐺((𝑔 ↾ (dom 𝑔 ∩ dom )) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ), 𝑎))) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎))))
7823, 25, 773eqtr4d 2654 . . 3 (((𝑔𝐵𝐵) ∧ 𝑎 ∈ (dom 𝑔 ∩ dom )) → ((𝑔 ↾ (dom 𝑔 ∩ dom ))‘𝑎) = (𝑎𝐺((𝑔 ↾ (dom 𝑔 ∩ dom )) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ), 𝑎))))
7978ralrimiva 2949 . 2 ((𝑔𝐵𝐵) → ∀𝑎 ∈ (dom 𝑔 ∩ dom )((𝑔 ↾ (dom 𝑔 ∩ dom ))‘𝑎) = (𝑎𝐺((𝑔 ↾ (dom 𝑔 ∩ dom )) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ), 𝑎))))
807, 79jca 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 195  wa 383  w3a 1031   = wceq 1475  wex 1695  wcel 1977  {cab 2596  wral 2896  cin 3539  wss 3540  dom cdm 5038  cres 5040  Predcpred 5596  Fun wfun 5798   Fn wfn 5799  cfv 5804  (class class class)co 6549
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pr 4833
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-iota 5768  df-fun 5806  df-fn 5807  df-fv 5812  df-ov 6552
This theorem is referenced by:  frrlem5  31028
  Copyright terms: Public domain W3C validator