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

Theorem wfrlem5OLD 8214
Description: Lemma for well-ordered recursion. The values of two acceptable functions agree within their domains. Obsolete as of 18-Nov-2024. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by Scott Fenton, 21-Apr-2011.) (Revised by Mario Carneiro, 26-Jun-2015.)
Hypotheses
Ref Expression
wfrlem5OLD.1 𝑅 We 𝐴
wfrlem5OLD.2 𝑅 Se 𝐴
wfrlem5OLD.3 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}
Assertion
Ref Expression
wfrlem5OLD ((𝑔𝐵𝐵) → ((𝑥𝑔𝑢𝑥𝑣) → 𝑢 = 𝑣))
Distinct variable groups:   𝐴,𝑓,𝑔,,𝑥,𝑦   𝑓,𝐹,𝑔,,𝑥,𝑦   𝑅,𝑓,𝑔,,𝑥,𝑦   𝑢,𝑔,𝑣,,𝑥
Allowed substitution hints:   𝐴(𝑣,𝑢)   𝐵(𝑥,𝑦,𝑣,𝑢,𝑓,𝑔,)   𝑅(𝑣,𝑢)   𝐹(𝑣,𝑢)

Proof of Theorem wfrlem5OLD
Dummy variable 𝑎 is distinct from all other variables.
StepHypRef Expression
1 vex 3445 . . . . . 6 𝑥 ∈ V
2 vex 3445 . . . . . 6 𝑢 ∈ V
31, 2breldm 5850 . . . . 5 (𝑥𝑔𝑢𝑥 ∈ dom 𝑔)
4 vex 3445 . . . . . 6 𝑣 ∈ V
51, 4breldm 5850 . . . . 5 (𝑥𝑣𝑥 ∈ dom )
63, 5anim12i 613 . . . 4 ((𝑥𝑔𝑢𝑥𝑣) → (𝑥 ∈ dom 𝑔𝑥 ∈ dom ))
7 elin 3914 . . . 4 (𝑥 ∈ (dom 𝑔 ∩ dom ) ↔ (𝑥 ∈ dom 𝑔𝑥 ∈ dom ))
86, 7sylibr 233 . . 3 ((𝑥𝑔𝑢𝑥𝑣) → 𝑥 ∈ (dom 𝑔 ∩ dom ))
9 anandi 673 . . . 4 ((𝑥 ∈ (dom 𝑔 ∩ dom ) ∧ (𝑥𝑔𝑢𝑥𝑣)) ↔ ((𝑥 ∈ (dom 𝑔 ∩ dom ) ∧ 𝑥𝑔𝑢) ∧ (𝑥 ∈ (dom 𝑔 ∩ dom ) ∧ 𝑥𝑣)))
102brresi 5932 . . . . 5 (𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ))𝑢 ↔ (𝑥 ∈ (dom 𝑔 ∩ dom ) ∧ 𝑥𝑔𝑢))
114brresi 5932 . . . . 5 (𝑥( ↾ (dom 𝑔 ∩ dom ))𝑣 ↔ (𝑥 ∈ (dom 𝑔 ∩ dom ) ∧ 𝑥𝑣))
1210, 11anbi12i 627 . . . 4 ((𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ))𝑢𝑥( ↾ (dom 𝑔 ∩ dom ))𝑣) ↔ ((𝑥 ∈ (dom 𝑔 ∩ dom ) ∧ 𝑥𝑔𝑢) ∧ (𝑥 ∈ (dom 𝑔 ∩ dom ) ∧ 𝑥𝑣)))
139, 12sylbb2 237 . . 3 ((𝑥 ∈ (dom 𝑔 ∩ dom ) ∧ (𝑥𝑔𝑢𝑥𝑣)) → (𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ))𝑢𝑥( ↾ (dom 𝑔 ∩ dom ))𝑣))
148, 13mpancom 685 . 2 ((𝑥𝑔𝑢𝑥𝑣) → (𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ))𝑢𝑥( ↾ (dom 𝑔 ∩ dom ))𝑣))
15 wfrlem5OLD.3 . . . . . . . . 9 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}
1615wfrlem3OLD 8211 . . . . . . . 8 (𝑔𝐵 → dom 𝑔𝐴)
17 ssinss1 4184 . . . . . . . 8 (dom 𝑔𝐴 → (dom 𝑔 ∩ dom ) ⊆ 𝐴)
18 wfrlem5OLD.1 . . . . . . . . . 10 𝑅 We 𝐴
19 wess 5607 . . . . . . . . . 10 ((dom 𝑔 ∩ dom ) ⊆ 𝐴 → (𝑅 We 𝐴𝑅 We (dom 𝑔 ∩ dom )))
2018, 19mpi 20 . . . . . . . . 9 ((dom 𝑔 ∩ dom ) ⊆ 𝐴𝑅 We (dom 𝑔 ∩ dom ))
21 wfrlem5OLD.2 . . . . . . . . . 10 𝑅 Se 𝐴
22 sess2 5589 . . . . . . . . . 10 ((dom 𝑔 ∩ dom ) ⊆ 𝐴 → (𝑅 Se 𝐴𝑅 Se (dom 𝑔 ∩ dom )))
2321, 22mpi 20 . . . . . . . . 9 ((dom 𝑔 ∩ dom ) ⊆ 𝐴𝑅 Se (dom 𝑔 ∩ dom ))
2420, 23jca 512 . . . . . . . 8 ((dom 𝑔 ∩ dom ) ⊆ 𝐴 → (𝑅 We (dom 𝑔 ∩ dom ) ∧ 𝑅 Se (dom 𝑔 ∩ dom )))
2516, 17, 243syl 18 . . . . . . 7 (𝑔𝐵 → (𝑅 We (dom 𝑔 ∩ dom ) ∧ 𝑅 Se (dom 𝑔 ∩ dom )))
2625adantr 481 . . . . . 6 ((𝑔𝐵𝐵) → (𝑅 We (dom 𝑔 ∩ dom ) ∧ 𝑅 Se (dom 𝑔 ∩ dom )))
2715wfrlem4OLD 8213 . . . . . 6 ((𝑔𝐵𝐵) → ((𝑔 ↾ (dom 𝑔 ∩ dom )) Fn (dom 𝑔 ∩ dom ) ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom )((𝑔 ↾ (dom 𝑔 ∩ dom ))‘𝑎) = (𝐹‘((𝑔 ↾ (dom 𝑔 ∩ dom )) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ), 𝑎)))))
2815wfrlem4OLD 8213 . . . . . . . 8 ((𝐵𝑔𝐵) → (( ↾ (dom ∩ dom 𝑔)) Fn (dom ∩ dom 𝑔) ∧ ∀𝑎 ∈ (dom ∩ dom 𝑔)(( ↾ (dom ∩ dom 𝑔))‘𝑎) = (𝐹‘(( ↾ (dom ∩ dom 𝑔)) ↾ Pred(𝑅, (dom ∩ dom 𝑔), 𝑎)))))
2928ancoms 459 . . . . . . 7 ((𝑔𝐵𝐵) → (( ↾ (dom ∩ dom 𝑔)) Fn (dom ∩ dom 𝑔) ∧ ∀𝑎 ∈ (dom ∩ dom 𝑔)(( ↾ (dom ∩ dom 𝑔))‘𝑎) = (𝐹‘(( ↾ (dom ∩ dom 𝑔)) ↾ Pred(𝑅, (dom ∩ dom 𝑔), 𝑎)))))
30 incom 4148 . . . . . . . . . . 11 (dom 𝑔 ∩ dom ) = (dom ∩ dom 𝑔)
3130reseq2i 5920 . . . . . . . . . 10 ( ↾ (dom 𝑔 ∩ dom )) = ( ↾ (dom ∩ dom 𝑔))
3231fneq1i 6582 . . . . . . . . 9 (( ↾ (dom 𝑔 ∩ dom )) Fn (dom 𝑔 ∩ dom ) ↔ ( ↾ (dom ∩ dom 𝑔)) Fn (dom 𝑔 ∩ dom ))
3330fneq2i 6583 . . . . . . . . 9 (( ↾ (dom ∩ dom 𝑔)) Fn (dom 𝑔 ∩ dom ) ↔ ( ↾ (dom ∩ dom 𝑔)) Fn (dom ∩ dom 𝑔))
3432, 33bitri 274 . . . . . . . 8 (( ↾ (dom 𝑔 ∩ dom )) Fn (dom 𝑔 ∩ dom ) ↔ ( ↾ (dom ∩ dom 𝑔)) Fn (dom ∩ dom 𝑔))
3531fveq1i 6826 . . . . . . . . . 10 (( ↾ (dom 𝑔 ∩ dom ))‘𝑎) = (( ↾ (dom ∩ dom 𝑔))‘𝑎)
36 predeq2 6241 . . . . . . . . . . . . 13 ((dom 𝑔 ∩ dom ) = (dom ∩ dom 𝑔) → Pred(𝑅, (dom 𝑔 ∩ dom ), 𝑎) = Pred(𝑅, (dom ∩ dom 𝑔), 𝑎))
3730, 36ax-mp 5 . . . . . . . . . . . 12 Pred(𝑅, (dom 𝑔 ∩ dom ), 𝑎) = Pred(𝑅, (dom ∩ dom 𝑔), 𝑎)
3831, 37reseq12i 5921 . . . . . . . . . . 11 (( ↾ (dom 𝑔 ∩ dom )) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ), 𝑎)) = (( ↾ (dom ∩ dom 𝑔)) ↾ Pred(𝑅, (dom ∩ dom 𝑔), 𝑎))
3938fveq2i 6828 . . . . . . . . . 10 (𝐹‘(( ↾ (dom 𝑔 ∩ dom )) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ), 𝑎))) = (𝐹‘(( ↾ (dom ∩ dom 𝑔)) ↾ Pred(𝑅, (dom ∩ dom 𝑔), 𝑎)))
4035, 39eqeq12i 2754 . . . . . . . . 9 ((( ↾ (dom 𝑔 ∩ dom ))‘𝑎) = (𝐹‘(( ↾ (dom 𝑔 ∩ dom )) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ), 𝑎))) ↔ (( ↾ (dom ∩ dom 𝑔))‘𝑎) = (𝐹‘(( ↾ (dom ∩ dom 𝑔)) ↾ Pred(𝑅, (dom ∩ dom 𝑔), 𝑎))))
4130, 40raleqbii 3311 . . . . . . . 8 (∀𝑎 ∈ (dom 𝑔 ∩ dom )(( ↾ (dom 𝑔 ∩ dom ))‘𝑎) = (𝐹‘(( ↾ (dom 𝑔 ∩ dom )) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ), 𝑎))) ↔ ∀𝑎 ∈ (dom ∩ dom 𝑔)(( ↾ (dom ∩ dom 𝑔))‘𝑎) = (𝐹‘(( ↾ (dom ∩ dom 𝑔)) ↾ Pred(𝑅, (dom ∩ dom 𝑔), 𝑎))))
4234, 41anbi12i 627 . . . . . . 7 ((( ↾ (dom 𝑔 ∩ dom )) Fn (dom 𝑔 ∩ dom ) ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom )(( ↾ (dom 𝑔 ∩ dom ))‘𝑎) = (𝐹‘(( ↾ (dom 𝑔 ∩ dom )) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ), 𝑎)))) ↔ (( ↾ (dom ∩ dom 𝑔)) Fn (dom ∩ dom 𝑔) ∧ ∀𝑎 ∈ (dom ∩ dom 𝑔)(( ↾ (dom ∩ dom 𝑔))‘𝑎) = (𝐹‘(( ↾ (dom ∩ dom 𝑔)) ↾ Pred(𝑅, (dom ∩ dom 𝑔), 𝑎)))))
4329, 42sylibr 233 . . . . . 6 ((𝑔𝐵𝐵) → (( ↾ (dom 𝑔 ∩ dom )) Fn (dom 𝑔 ∩ dom ) ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom )(( ↾ (dom 𝑔 ∩ dom ))‘𝑎) = (𝐹‘(( ↾ (dom 𝑔 ∩ dom )) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ), 𝑎)))))
44 wfr3g 8208 . . . . . 6 (((𝑅 We (dom 𝑔 ∩ dom ) ∧ 𝑅 Se (dom 𝑔 ∩ dom )) ∧ ((𝑔 ↾ (dom 𝑔 ∩ dom )) Fn (dom 𝑔 ∩ dom ) ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom )((𝑔 ↾ (dom 𝑔 ∩ dom ))‘𝑎) = (𝐹‘((𝑔 ↾ (dom 𝑔 ∩ dom )) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ), 𝑎)))) ∧ (( ↾ (dom 𝑔 ∩ dom )) Fn (dom 𝑔 ∩ dom ) ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom )(( ↾ (dom 𝑔 ∩ dom ))‘𝑎) = (𝐹‘(( ↾ (dom 𝑔 ∩ dom )) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ), 𝑎))))) → (𝑔 ↾ (dom 𝑔 ∩ dom )) = ( ↾ (dom 𝑔 ∩ dom )))
4526, 27, 43, 44syl3anc 1370 . . . . 5 ((𝑔𝐵𝐵) → (𝑔 ↾ (dom 𝑔 ∩ dom )) = ( ↾ (dom 𝑔 ∩ dom )))
4645breqd 5103 . . . 4 ((𝑔𝐵𝐵) → (𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ))𝑣𝑥( ↾ (dom 𝑔 ∩ dom ))𝑣))
4746biimprd 247 . . 3 ((𝑔𝐵𝐵) → (𝑥( ↾ (dom 𝑔 ∩ dom ))𝑣𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ))𝑣))
4815wfrlem2OLD 8210 . . . . 5 (𝑔𝐵 → Fun 𝑔)
49 funres 6526 . . . . 5 (Fun 𝑔 → Fun (𝑔 ↾ (dom 𝑔 ∩ dom )))
50 dffun2 6489 . . . . . 6 (Fun (𝑔 ↾ (dom 𝑔 ∩ dom )) ↔ (Rel (𝑔 ↾ (dom 𝑔 ∩ dom )) ∧ ∀𝑥𝑢𝑣((𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ))𝑢𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ))𝑣) → 𝑢 = 𝑣)))
5150simprbi 497 . . . . 5 (Fun (𝑔 ↾ (dom 𝑔 ∩ dom )) → ∀𝑥𝑢𝑣((𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ))𝑢𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ))𝑣) → 𝑢 = 𝑣))
52 2sp 2178 . . . . . 6 (∀𝑢𝑣((𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ))𝑢𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ))𝑣) → 𝑢 = 𝑣) → ((𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ))𝑢𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ))𝑣) → 𝑢 = 𝑣))
5352sps 2177 . . . . 5 (∀𝑥𝑢𝑣((𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ))𝑢𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ))𝑣) → 𝑢 = 𝑣) → ((𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ))𝑢𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ))𝑣) → 𝑢 = 𝑣))
5448, 49, 51, 534syl 19 . . . 4 (𝑔𝐵 → ((𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ))𝑢𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ))𝑣) → 𝑢 = 𝑣))
5554adantr 481 . . 3 ((𝑔𝐵𝐵) → ((𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ))𝑢𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ))𝑣) → 𝑢 = 𝑣))
5647, 55sylan2d 605 . 2 ((𝑔𝐵𝐵) → ((𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ))𝑢𝑥( ↾ (dom 𝑔 ∩ dom ))𝑣) → 𝑢 = 𝑣))
5714, 56syl5 34 1 ((𝑔𝐵𝐵) → ((𝑥𝑔𝑢𝑥𝑣) → 𝑢 = 𝑣))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1086  wal 1538   = wceq 1540  wex 1780  wcel 2105  {cab 2713  wral 3061  cin 3897  wss 3898   class class class wbr 5092   Se wse 5573   We wwe 5574  dom cdm 5620  cres 5622  Rel wrel 5625  Predcpred 6237  Fun wfun 6473   Fn wfn 6474  cfv 6479
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-sep 5243  ax-nul 5250  ax-pr 5372
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3404  df-v 3443  df-sbc 3728  df-csb 3844  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4270  df-if 4474  df-pw 4549  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4853  df-br 5093  df-opab 5155  df-mpt 5176  df-id 5518  df-po 5532  df-so 5533  df-fr 5575  df-se 5576  df-we 5577  df-xp 5626  df-rel 5627  df-cnv 5628  df-co 5629  df-dm 5630  df-rn 5631  df-res 5632  df-ima 5633  df-pred 6238  df-iota 6431  df-fun 6481  df-fn 6482  df-fv 6487
This theorem is referenced by:  wfrfunOLD  8220
  Copyright terms: Public domain W3C validator