Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  wfrlem4OLD Structured version   Visualization version   GIF version

Theorem wfrlem4OLD 7759
 Description: Obsolete version of wfrlem4 7758 as of 18-Jul-2022. (Contributed by Scott Fenton, 21-Apr-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
Hypotheses
Ref Expression
wfrlem4OLD.1 𝑅 We 𝐴
wfrlem4OLD.2 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}
Assertion
Ref Expression
wfrlem4OLD ((𝑔𝐵𝐵) → ((𝑔 ↾ (dom 𝑔 ∩ dom )) Fn (dom 𝑔 ∩ dom ) ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom )((𝑔 ↾ (dom 𝑔 ∩ dom ))‘𝑎) = (𝐹‘((𝑔 ↾ (dom 𝑔 ∩ dom )) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ), 𝑎)))))
Distinct variable groups:   𝐴,𝑎,𝑓,𝑔,,𝑥,𝑦   𝐵,𝑎   𝐹,𝑎,𝑓,𝑔,,𝑥,𝑦   𝑅,𝑎,𝑓,𝑔,,𝑥,𝑦
Allowed substitution hints:   𝐵(𝑥,𝑦,𝑓,𝑔,)

Proof of Theorem wfrlem4OLD
Dummy variables 𝑏 𝑐 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 wfrlem4OLD.2 . . . . . 6 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}
21wfrlem2 7755 . . . . 5 (𝑔𝐵 → Fun 𝑔)
3 funfn 6216 . . . . 5 (Fun 𝑔𝑔 Fn dom 𝑔)
42, 3sylib 210 . . . 4 (𝑔𝐵𝑔 Fn dom 𝑔)
5 fnresin1 6302 . . . 4 (𝑔 Fn dom 𝑔 → (𝑔 ↾ (dom 𝑔 ∩ dom )) Fn (dom 𝑔 ∩ dom ))
64, 5syl 17 . . 3 (𝑔𝐵 → (𝑔 ↾ (dom 𝑔 ∩ dom )) Fn (dom 𝑔 ∩ dom ))
76adantr 473 . 2 ((𝑔𝐵𝐵) → (𝑔 ↾ (dom 𝑔 ∩ dom )) Fn (dom 𝑔 ∩ dom ))
8 inss1 4091 . . . . . . . 8 (dom 𝑔 ∩ dom ) ⊆ dom 𝑔
98sseli 3853 . . . . . . 7 (𝑎 ∈ (dom 𝑔 ∩ dom ) → 𝑎 ∈ dom 𝑔)
101wfrlem1 7754 . . . . . . . . 9 𝐵 = {𝑔 ∣ ∃𝑏(𝑔 Fn 𝑏 ∧ (𝑏𝐴 ∧ ∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎𝑏 (𝑔𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎))))}
1110abeq2i 2897 . . . . . . . 8 (𝑔𝐵 ↔ ∃𝑏(𝑔 Fn 𝑏 ∧ (𝑏𝐴 ∧ ∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎𝑏 (𝑔𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))))
12 fndm 6286 . . . . . . . . . . . . 13 (𝑔 Fn 𝑏 → dom 𝑔 = 𝑏)
1312raleqdv 3352 . . . . . . . . . . . 12 (𝑔 Fn 𝑏 → (∀𝑎 ∈ dom 𝑔(𝑔𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎))) ↔ ∀𝑎𝑏 (𝑔𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))))
1413biimpar 470 . . . . . . . . . . 11 ((𝑔 Fn 𝑏 ∧ ∀𝑎𝑏 (𝑔𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) → ∀𝑎 ∈ dom 𝑔(𝑔𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎))))
15 rsp 3152 . . . . . . . . . . 11 (∀𝑎 ∈ dom 𝑔(𝑔𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎))) → (𝑎 ∈ dom 𝑔 → (𝑔𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))))
1614, 15syl 17 . . . . . . . . . 10 ((𝑔 Fn 𝑏 ∧ ∀𝑎𝑏 (𝑔𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) → (𝑎 ∈ dom 𝑔 → (𝑔𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))))
17163adant2 1111 . . . . . . . . 9 ((𝑔 Fn 𝑏 ∧ (𝑏𝐴 ∧ ∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎𝑏 (𝑔𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) → (𝑎 ∈ dom 𝑔 → (𝑔𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))))
1817exlimiv 1889 . . . . . . . 8 (∃𝑏(𝑔 Fn 𝑏 ∧ (𝑏𝐴 ∧ ∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎𝑏 (𝑔𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) → (𝑎 ∈ dom 𝑔 → (𝑔𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))))
1911, 18sylbi 209 . . . . . . 7 (𝑔𝐵 → (𝑎 ∈ dom 𝑔 → (𝑔𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))))
209, 19syl5 34 . . . . . 6 (𝑔𝐵 → (𝑎 ∈ (dom 𝑔 ∩ dom ) → (𝑔𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))))
2120imp 398 . . . . 5 ((𝑔𝐵𝑎 ∈ (dom 𝑔 ∩ dom )) → (𝑔𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎))))
2221adantlr 702 . . . 4 (((𝑔𝐵𝐵) ∧ 𝑎 ∈ (dom 𝑔 ∩ dom )) → (𝑔𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎))))
23 fvres 6516 . . . . 5 (𝑎 ∈ (dom 𝑔 ∩ dom ) → ((𝑔 ↾ (dom 𝑔 ∩ dom ))‘𝑎) = (𝑔𝑎))
2423adantl 474 . . . 4 (((𝑔𝐵𝐵) ∧ 𝑎 ∈ (dom 𝑔 ∩ dom )) → ((𝑔 ↾ (dom 𝑔 ∩ dom ))‘𝑎) = (𝑔𝑎))
25 resres 5709 . . . . . 6 ((𝑔 ↾ (dom 𝑔 ∩ dom )) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ), 𝑎)) = (𝑔 ↾ ((dom 𝑔 ∩ dom ) ∩ Pred(𝑅, (dom 𝑔 ∩ dom ), 𝑎)))
26 predss 5991 . . . . . . . . 9 Pred(𝑅, (dom 𝑔 ∩ dom ), 𝑎) ⊆ (dom 𝑔 ∩ dom )
27 sseqin2 4078 . . . . . . . . 9 (Pred(𝑅, (dom 𝑔 ∩ dom ), 𝑎) ⊆ (dom 𝑔 ∩ dom ) ↔ ((dom 𝑔 ∩ dom ) ∩ Pred(𝑅, (dom 𝑔 ∩ dom ), 𝑎)) = Pred(𝑅, (dom 𝑔 ∩ dom ), 𝑎))
2826, 27mpbi 222 . . . . . . . 8 ((dom 𝑔 ∩ dom ) ∩ Pred(𝑅, (dom 𝑔 ∩ dom ), 𝑎)) = Pred(𝑅, (dom 𝑔 ∩ dom ), 𝑎)
291wfrlem1 7754 . . . . . . . . . . . 12 𝐵 = { ∣ ∃𝑐( Fn 𝑐 ∧ (𝑐𝐴 ∧ ∀𝑎𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) ∧ ∀𝑎𝑐 (𝑎) = (𝐹‘( ↾ Pred(𝑅, 𝐴, 𝑎))))}
3029abeq2i 2897 . . . . . . . . . . 11 (𝐵 ↔ ∃𝑐( Fn 𝑐 ∧ (𝑐𝐴 ∧ ∀𝑎𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) ∧ ∀𝑎𝑐 (𝑎) = (𝐹‘( ↾ Pred(𝑅, 𝐴, 𝑎)))))
31 3an6 1425 . . . . . . . . . . . . . 14 (((𝑔 Fn 𝑏 Fn 𝑐) ∧ ((𝑏𝐴 ∧ ∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ (𝑐𝐴 ∧ ∀𝑎𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐)) ∧ (∀𝑎𝑏 (𝑔𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎))) ∧ ∀𝑎𝑐 (𝑎) = (𝐹‘( ↾ Pred(𝑅, 𝐴, 𝑎))))) ↔ ((𝑔 Fn 𝑏 ∧ (𝑏𝐴 ∧ ∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎𝑏 (𝑔𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) ∧ ( Fn 𝑐 ∧ (𝑐𝐴 ∧ ∀𝑎𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) ∧ ∀𝑎𝑐 (𝑎) = (𝐹‘( ↾ Pred(𝑅, 𝐴, 𝑎))))))
32312exbii 1811 . . . . . . . . . . . . 13 (∃𝑏𝑐((𝑔 Fn 𝑏 Fn 𝑐) ∧ ((𝑏𝐴 ∧ ∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ (𝑐𝐴 ∧ ∀𝑎𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐)) ∧ (∀𝑎𝑏 (𝑔𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎))) ∧ ∀𝑎𝑐 (𝑎) = (𝐹‘( ↾ Pred(𝑅, 𝐴, 𝑎))))) ↔ ∃𝑏𝑐((𝑔 Fn 𝑏 ∧ (𝑏𝐴 ∧ ∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎𝑏 (𝑔𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) ∧ ( Fn 𝑐 ∧ (𝑐𝐴 ∧ ∀𝑎𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) ∧ ∀𝑎𝑐 (𝑎) = (𝐹‘( ↾ Pred(𝑅, 𝐴, 𝑎))))))
33 eeanv 2281 . . . . . . . . . . . . 13 (∃𝑏𝑐((𝑔 Fn 𝑏 ∧ (𝑏𝐴 ∧ ∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎𝑏 (𝑔𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) ∧ ( Fn 𝑐 ∧ (𝑐𝐴 ∧ ∀𝑎𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) ∧ ∀𝑎𝑐 (𝑎) = (𝐹‘( ↾ Pred(𝑅, 𝐴, 𝑎))))) ↔ (∃𝑏(𝑔 Fn 𝑏 ∧ (𝑏𝐴 ∧ ∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎𝑏 (𝑔𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) ∧ ∃𝑐( Fn 𝑐 ∧ (𝑐𝐴 ∧ ∀𝑎𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) ∧ ∀𝑎𝑐 (𝑎) = (𝐹‘( ↾ Pred(𝑅, 𝐴, 𝑎))))))
3432, 33bitri 267 . . . . . . . . . . . 12 (∃𝑏𝑐((𝑔 Fn 𝑏 Fn 𝑐) ∧ ((𝑏𝐴 ∧ ∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ (𝑐𝐴 ∧ ∀𝑎𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐)) ∧ (∀𝑎𝑏 (𝑔𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎))) ∧ ∀𝑎𝑐 (𝑎) = (𝐹‘( ↾ Pred(𝑅, 𝐴, 𝑎))))) ↔ (∃𝑏(𝑔 Fn 𝑏 ∧ (𝑏𝐴 ∧ ∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎𝑏 (𝑔𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) ∧ ∃𝑐( Fn 𝑐 ∧ (𝑐𝐴 ∧ ∀𝑎𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) ∧ ∀𝑎𝑐 (𝑎) = (𝐹‘( ↾ Pred(𝑅, 𝐴, 𝑎))))))
35 ssinss1 4100 . . . . . . . . . . . . . . . . . 18 (𝑏𝐴 → (𝑏𝑐) ⊆ 𝐴)
3635ad2antrr 713 . . . . . . . . . . . . . . . . 17 (((𝑏𝐴 ∧ ∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ (𝑐𝐴 ∧ ∀𝑎𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐)) → (𝑏𝑐) ⊆ 𝐴)
37 nfra1 3166 . . . . . . . . . . . . . . . . . . . 20 𝑎𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏
38 nfra1 3166 . . . . . . . . . . . . . . . . . . . 20 𝑎𝑎𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐
3937, 38nfan 1862 . . . . . . . . . . . . . . . . . . 19 𝑎(∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏 ∧ ∀𝑎𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐)
40 inss1 4091 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑏𝑐) ⊆ 𝑏
4140sseli 3853 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 ∈ (𝑏𝑐) → 𝑎𝑏)
42 rsp 3152 . . . . . . . . . . . . . . . . . . . . . 22 (∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏 → (𝑎𝑏 → Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏))
4341, 42syl5com 31 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 ∈ (𝑏𝑐) → (∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏 → Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏))
44 inss2 4092 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑏𝑐) ⊆ 𝑐
4544sseli 3853 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 ∈ (𝑏𝑐) → 𝑎𝑐)
46 rsp 3152 . . . . . . . . . . . . . . . . . . . . . 22 (∀𝑎𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐 → (𝑎𝑐 → Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐))
4745, 46syl5com 31 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 ∈ (𝑏𝑐) → (∀𝑎𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐 → Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐))
4843, 47anim12d 599 . . . . . . . . . . . . . . . . . . . 20 (𝑎 ∈ (𝑏𝑐) → ((∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏 ∧ ∀𝑎𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) → (Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏 ∧ Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐)))
49 ssin 4093 . . . . . . . . . . . . . . . . . . . . 21 ((Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏 ∧ Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) ↔ Pred(𝑅, 𝐴, 𝑎) ⊆ (𝑏𝑐))
5049biimpi 208 . . . . . . . . . . . . . . . . . . . 20 ((Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏 ∧ Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) → Pred(𝑅, 𝐴, 𝑎) ⊆ (𝑏𝑐))
5148, 50syl6com 37 . . . . . . . . . . . . . . . . . . 19 ((∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏 ∧ ∀𝑎𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) → (𝑎 ∈ (𝑏𝑐) → Pred(𝑅, 𝐴, 𝑎) ⊆ (𝑏𝑐)))
5239, 51ralrimi 3163 . . . . . . . . . . . . . . . . . 18 ((∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏 ∧ ∀𝑎𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) → ∀𝑎 ∈ (𝑏𝑐)Pred(𝑅, 𝐴, 𝑎) ⊆ (𝑏𝑐))
5352ad2ant2l 733 . . . . . . . . . . . . . . . . 17 (((𝑏𝐴 ∧ ∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ (𝑐𝐴 ∧ ∀𝑎𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐)) → ∀𝑎 ∈ (𝑏𝑐)Pred(𝑅, 𝐴, 𝑎) ⊆ (𝑏𝑐))
5436, 53jca 504 . . . . . . . . . . . . . . . 16 (((𝑏𝐴 ∧ ∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ (𝑐𝐴 ∧ ∀𝑎𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐)) → ((𝑏𝑐) ⊆ 𝐴 ∧ ∀𝑎 ∈ (𝑏𝑐)Pred(𝑅, 𝐴, 𝑎) ⊆ (𝑏𝑐)))
55 fndm 6286 . . . . . . . . . . . . . . . . . 18 ( Fn 𝑐 → dom = 𝑐)
5612, 55ineqan12d 4077 . . . . . . . . . . . . . . . . 17 ((𝑔 Fn 𝑏 Fn 𝑐) → (dom 𝑔 ∩ dom ) = (𝑏𝑐))
57 sseq1 3881 . . . . . . . . . . . . . . . . . . 19 ((dom 𝑔 ∩ dom ) = (𝑏𝑐) → ((dom 𝑔 ∩ dom ) ⊆ 𝐴 ↔ (𝑏𝑐) ⊆ 𝐴))
58 sseq2 3882 . . . . . . . . . . . . . . . . . . . 20 ((dom 𝑔 ∩ dom ) = (𝑏𝑐) → (Pred(𝑅, 𝐴, 𝑎) ⊆ (dom 𝑔 ∩ dom ) ↔ Pred(𝑅, 𝐴, 𝑎) ⊆ (𝑏𝑐)))
5958raleqbi1dv 3340 . . . . . . . . . . . . . . . . . . 19 ((dom 𝑔 ∩ dom ) = (𝑏𝑐) → (∀𝑎 ∈ (dom 𝑔 ∩ dom )Pred(𝑅, 𝐴, 𝑎) ⊆ (dom 𝑔 ∩ dom ) ↔ ∀𝑎 ∈ (𝑏𝑐)Pred(𝑅, 𝐴, 𝑎) ⊆ (𝑏𝑐)))
6057, 59anbi12d 621 . . . . . . . . . . . . . . . . . 18 ((dom 𝑔 ∩ dom ) = (𝑏𝑐) → (((dom 𝑔 ∩ dom ) ⊆ 𝐴 ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom )Pred(𝑅, 𝐴, 𝑎) ⊆ (dom 𝑔 ∩ dom )) ↔ ((𝑏𝑐) ⊆ 𝐴 ∧ ∀𝑎 ∈ (𝑏𝑐)Pred(𝑅, 𝐴, 𝑎) ⊆ (𝑏𝑐))))
6160imbi2d 333 . . . . . . . . . . . . . . . . 17 ((dom 𝑔 ∩ dom ) = (𝑏𝑐) → ((((𝑏𝐴 ∧ ∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ (𝑐𝐴 ∧ ∀𝑎𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐)) → ((dom 𝑔 ∩ dom ) ⊆ 𝐴 ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom )Pred(𝑅, 𝐴, 𝑎) ⊆ (dom 𝑔 ∩ dom ))) ↔ (((𝑏𝐴 ∧ ∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ (𝑐𝐴 ∧ ∀𝑎𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐)) → ((𝑏𝑐) ⊆ 𝐴 ∧ ∀𝑎 ∈ (𝑏𝑐)Pred(𝑅, 𝐴, 𝑎) ⊆ (𝑏𝑐)))))
6256, 61syl 17 . . . . . . . . . . . . . . . 16 ((𝑔 Fn 𝑏 Fn 𝑐) → ((((𝑏𝐴 ∧ ∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ (𝑐𝐴 ∧ ∀𝑎𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐)) → ((dom 𝑔 ∩ dom ) ⊆ 𝐴 ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom )Pred(𝑅, 𝐴, 𝑎) ⊆ (dom 𝑔 ∩ dom ))) ↔ (((𝑏𝐴 ∧ ∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ (𝑐𝐴 ∧ ∀𝑎𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐)) → ((𝑏𝑐) ⊆ 𝐴 ∧ ∀𝑎 ∈ (𝑏𝑐)Pred(𝑅, 𝐴, 𝑎) ⊆ (𝑏𝑐)))))
6354, 62mpbiri 250 . . . . . . . . . . . . . . 15 ((𝑔 Fn 𝑏 Fn 𝑐) → (((𝑏𝐴 ∧ ∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ (𝑐𝐴 ∧ ∀𝑎𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐)) → ((dom 𝑔 ∩ dom ) ⊆ 𝐴 ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom )Pred(𝑅, 𝐴, 𝑎) ⊆ (dom 𝑔 ∩ dom ))))
6463imp 398 . . . . . . . . . . . . . 14 (((𝑔 Fn 𝑏 Fn 𝑐) ∧ ((𝑏𝐴 ∧ ∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ (𝑐𝐴 ∧ ∀𝑎𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐))) → ((dom 𝑔 ∩ dom ) ⊆ 𝐴 ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom )Pred(𝑅, 𝐴, 𝑎) ⊆ (dom 𝑔 ∩ dom )))
65643adant3 1112 . . . . . . . . . . . . 13 (((𝑔 Fn 𝑏 Fn 𝑐) ∧ ((𝑏𝐴 ∧ ∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ (𝑐𝐴 ∧ ∀𝑎𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐)) ∧ (∀𝑎𝑏 (𝑔𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎))) ∧ ∀𝑎𝑐 (𝑎) = (𝐹‘( ↾ Pred(𝑅, 𝐴, 𝑎))))) → ((dom 𝑔 ∩ dom ) ⊆ 𝐴 ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom )Pred(𝑅, 𝐴, 𝑎) ⊆ (dom 𝑔 ∩ dom )))
6665exlimivv 1891 . . . . . . . . . . . 12 (∃𝑏𝑐((𝑔 Fn 𝑏 Fn 𝑐) ∧ ((𝑏𝐴 ∧ ∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ (𝑐𝐴 ∧ ∀𝑎𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐)) ∧ (∀𝑎𝑏 (𝑔𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎))) ∧ ∀𝑎𝑐 (𝑎) = (𝐹‘( ↾ Pred(𝑅, 𝐴, 𝑎))))) → ((dom 𝑔 ∩ dom ) ⊆ 𝐴 ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom )Pred(𝑅, 𝐴, 𝑎) ⊆ (dom 𝑔 ∩ dom )))
6734, 66sylbir 227 . . . . . . . . . . 11 ((∃𝑏(𝑔 Fn 𝑏 ∧ (𝑏𝐴 ∧ ∀𝑎𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎𝑏 (𝑔𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) ∧ ∃𝑐( Fn 𝑐 ∧ (𝑐𝐴 ∧ ∀𝑎𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) ∧ ∀𝑎𝑐 (𝑎) = (𝐹‘( ↾ Pred(𝑅, 𝐴, 𝑎))))) → ((dom 𝑔 ∩ dom ) ⊆ 𝐴 ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom )Pred(𝑅, 𝐴, 𝑎) ⊆ (dom 𝑔 ∩ dom )))
6811, 30, 67syl2anb 588 . . . . . . . . . 10 ((𝑔𝐵𝐵) → ((dom 𝑔 ∩ dom ) ⊆ 𝐴 ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom )Pred(𝑅, 𝐴, 𝑎) ⊆ (dom 𝑔 ∩ dom )))
6968adantr 473 . . . . . . . . 9 (((𝑔𝐵𝐵) ∧ 𝑎 ∈ (dom 𝑔 ∩ dom )) → ((dom 𝑔 ∩ dom ) ⊆ 𝐴 ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom )Pred(𝑅, 𝐴, 𝑎) ⊆ (dom 𝑔 ∩ dom )))
70 simpr 477 . . . . . . . . 9 (((𝑔𝐵𝐵) ∧ 𝑎 ∈ (dom 𝑔 ∩ dom )) → 𝑎 ∈ (dom 𝑔 ∩ dom ))
71 preddowncl 6011 . . . . . . . . 9 (((dom 𝑔 ∩ dom ) ⊆ 𝐴 ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom )Pred(𝑅, 𝐴, 𝑎) ⊆ (dom 𝑔 ∩ dom )) → (𝑎 ∈ (dom 𝑔 ∩ dom ) → Pred(𝑅, (dom 𝑔 ∩ dom ), 𝑎) = Pred(𝑅, 𝐴, 𝑎)))
7269, 70, 71sylc 65 . . . . . . . 8 (((𝑔𝐵𝐵) ∧ 𝑎 ∈ (dom 𝑔 ∩ dom )) → Pred(𝑅, (dom 𝑔 ∩ dom ), 𝑎) = Pred(𝑅, 𝐴, 𝑎))
7328, 72syl5eq 2823 . . . . . . 7 (((𝑔𝐵𝐵) ∧ 𝑎 ∈ (dom 𝑔 ∩ dom )) → ((dom 𝑔 ∩ dom ) ∩ Pred(𝑅, (dom 𝑔 ∩ dom ), 𝑎)) = Pred(𝑅, 𝐴, 𝑎))
7473reseq2d 5692 . . . . . 6 (((𝑔𝐵𝐵) ∧ 𝑎 ∈ (dom 𝑔 ∩ dom )) → (𝑔 ↾ ((dom 𝑔 ∩ dom ) ∩ Pred(𝑅, (dom 𝑔 ∩ dom ), 𝑎))) = (𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))
7525, 74syl5eq 2823 . . . . 5 (((𝑔𝐵𝐵) ∧ 𝑎 ∈ (dom 𝑔 ∩ dom )) → ((𝑔 ↾ (dom 𝑔 ∩ dom )) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ), 𝑎)) = (𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))
7675fveq2d 6501 . . . 4 (((𝑔𝐵𝐵) ∧ 𝑎 ∈ (dom 𝑔 ∩ dom )) → (𝐹‘((𝑔 ↾ (dom 𝑔 ∩ dom )) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ), 𝑎))) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎))))
7722, 24, 763eqtr4d 2821 . . 3 (((𝑔𝐵𝐵) ∧ 𝑎 ∈ (dom 𝑔 ∩ dom )) → ((𝑔 ↾ (dom 𝑔 ∩ dom ))‘𝑎) = (𝐹‘((𝑔 ↾ (dom 𝑔 ∩ dom )) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ), 𝑎))))
7877ralrimiva 3129 . 2 ((𝑔𝐵𝐵) → ∀𝑎 ∈ (dom 𝑔 ∩ dom )((𝑔 ↾ (dom 𝑔 ∩ dom ))‘𝑎) = (𝐹‘((𝑔 ↾ (dom 𝑔 ∩ dom )) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ), 𝑎))))
797, 78jca 504 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 198   ∧ wa 387   ∧ w3a 1068   = wceq 1507  ∃wex 1742   ∈ wcel 2048  {cab 2755  ∀wral 3085   ∩ cin 3827   ⊆ wss 3828   We wwe 5362  dom cdm 5404   ↾ cres 5406  Predcpred 5983  Fun wfun 6180   Fn wfn 6181  ‘cfv 6186 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-10 2077  ax-11 2091  ax-12 2104  ax-13 2299  ax-ext 2747  ax-sep 5058  ax-nul 5065  ax-pr 5184 This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2014  df-mo 2544  df-eu 2580  df-clab 2756  df-cleq 2768  df-clel 2843  df-nfc 2915  df-ral 3090  df-rex 3091  df-rab 3094  df-v 3414  df-sbc 3681  df-dif 3831  df-un 3833  df-in 3835  df-ss 3842  df-nul 4178  df-if 4349  df-sn 4440  df-pr 4442  df-op 4446  df-uni 4711  df-br 4928  df-opab 4990  df-xp 5410  df-rel 5411  df-cnv 5412  df-co 5413  df-dm 5414  df-rn 5415  df-res 5416  df-ima 5417  df-pred 5984  df-iota 6150  df-fun 6188  df-fn 6189  df-fv 6194 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator