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

Theorem fprlem1 33245
 Description: Lemma for founded partial recursion. Two acceptable functions are compatible. (Contributed by Scott Fenton, 11-Sep-2023.)
Hypotheses
Ref Expression
fprlem.1 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}
fprlem.2 𝐹 = frecs(𝑅, 𝐴, 𝐺)
Assertion
Ref Expression
fprlem1 (((𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴) ∧ (𝑔𝐵𝐵)) → ((𝑥𝑔𝑢𝑥𝑣) → 𝑢 = 𝑣))
Distinct variable groups:   𝐴,𝑓,𝑥,𝑦,𝑔,,𝑢,𝑣   𝑅,𝑓,𝑥,𝑦,𝑔,,𝑢,𝑣   𝑓,𝐺,𝑥,𝑦,𝑔,,𝑢,𝑣
Allowed substitution hints:   𝐵(𝑥,𝑦,𝑣,𝑢,𝑓,𝑔,)   𝐹(𝑥,𝑦,𝑣,𝑢,𝑓,𝑔,)

Proof of Theorem fprlem1
Dummy variable 𝑎 is distinct from all other variables.
StepHypRef Expression
1 vex 3447 . . . . 5 𝑥 ∈ V
2 vex 3447 . . . . 5 𝑢 ∈ V
31, 2breldm 5745 . . . 4 (𝑥𝑔𝑢𝑥 ∈ dom 𝑔)
4 vex 3447 . . . . 5 𝑣 ∈ V
51, 4breldm 5745 . . . 4 (𝑥𝑣𝑥 ∈ dom )
6 elin 3900 . . . . 5 (𝑥 ∈ (dom 𝑔 ∩ dom ) ↔ (𝑥 ∈ dom 𝑔𝑥 ∈ dom ))
76biimpri 231 . . . 4 ((𝑥 ∈ dom 𝑔𝑥 ∈ dom ) → 𝑥 ∈ (dom 𝑔 ∩ dom ))
83, 5, 7syl2an 598 . . 3 ((𝑥𝑔𝑢𝑥𝑣) → 𝑥 ∈ (dom 𝑔 ∩ dom ))
9 id 22 . . 3 ((𝑥𝑔𝑢𝑥𝑣) → (𝑥𝑔𝑢𝑥𝑣))
102brresi 5831 . . . . 5 (𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ))𝑢 ↔ (𝑥 ∈ (dom 𝑔 ∩ dom ) ∧ 𝑥𝑔𝑢))
114brresi 5831 . . . . 5 (𝑥( ↾ (dom 𝑔 ∩ dom ))𝑣 ↔ (𝑥 ∈ (dom 𝑔 ∩ dom ) ∧ 𝑥𝑣))
1210, 11anbi12i 629 . . . 4 ((𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ))𝑢𝑥( ↾ (dom 𝑔 ∩ dom ))𝑣) ↔ ((𝑥 ∈ (dom 𝑔 ∩ dom ) ∧ 𝑥𝑔𝑢) ∧ (𝑥 ∈ (dom 𝑔 ∩ dom ) ∧ 𝑥𝑣)))
13 an4 655 . . . 4 (((𝑥 ∈ (dom 𝑔 ∩ dom ) ∧ 𝑥𝑔𝑢) ∧ (𝑥 ∈ (dom 𝑔 ∩ dom ) ∧ 𝑥𝑣)) ↔ ((𝑥 ∈ (dom 𝑔 ∩ dom ) ∧ 𝑥 ∈ (dom 𝑔 ∩ dom )) ∧ (𝑥𝑔𝑢𝑥𝑣)))
1412, 13bitri 278 . . 3 ((𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ))𝑢𝑥( ↾ (dom 𝑔 ∩ dom ))𝑣) ↔ ((𝑥 ∈ (dom 𝑔 ∩ dom ) ∧ 𝑥 ∈ (dom 𝑔 ∩ dom )) ∧ (𝑥𝑔𝑢𝑥𝑣)))
158, 8, 9, 14syl21anbrc 1341 . 2 ((𝑥𝑔𝑢𝑥𝑣) → (𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ))𝑢𝑥( ↾ (dom 𝑔 ∩ dom ))𝑣))
16 inss2 4159 . . . . . . . . . 10 (dom 𝑔 ∩ dom ) ⊆ dom
17 fprlem.1 . . . . . . . . . . 11 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}
1817frrlem3 33233 . . . . . . . . . 10 (𝐵 → dom 𝐴)
1916, 18sstrid 3929 . . . . . . . . 9 (𝐵 → (dom 𝑔 ∩ dom ) ⊆ 𝐴)
2019adantl 485 . . . . . . . 8 ((𝑔𝐵𝐵) → (dom 𝑔 ∩ dom ) ⊆ 𝐴)
2120adantl 485 . . . . . . 7 (((𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴) ∧ (𝑔𝐵𝐵)) → (dom 𝑔 ∩ dom ) ⊆ 𝐴)
22 simpl1 1188 . . . . . . 7 (((𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴) ∧ (𝑔𝐵𝐵)) → 𝑅 Fr 𝐴)
23 frss 5490 . . . . . . 7 ((dom 𝑔 ∩ dom ) ⊆ 𝐴 → (𝑅 Fr 𝐴𝑅 Fr (dom 𝑔 ∩ dom )))
2421, 22, 23sylc 65 . . . . . 6 (((𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴) ∧ (𝑔𝐵𝐵)) → 𝑅 Fr (dom 𝑔 ∩ dom ))
25 simpl2 1189 . . . . . . 7 (((𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴) ∧ (𝑔𝐵𝐵)) → 𝑅 Po 𝐴)
26 poss 5444 . . . . . . 7 ((dom 𝑔 ∩ dom ) ⊆ 𝐴 → (𝑅 Po 𝐴𝑅 Po (dom 𝑔 ∩ dom )))
2721, 25, 26sylc 65 . . . . . 6 (((𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴) ∧ (𝑔𝐵𝐵)) → 𝑅 Po (dom 𝑔 ∩ dom ))
28 simpl3 1190 . . . . . . 7 (((𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴) ∧ (𝑔𝐵𝐵)) → 𝑅 Se 𝐴)
29 sess2 5492 . . . . . . 7 ((dom 𝑔 ∩ dom ) ⊆ 𝐴 → (𝑅 Se 𝐴𝑅 Se (dom 𝑔 ∩ dom )))
3021, 28, 29sylc 65 . . . . . 6 (((𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴) ∧ (𝑔𝐵𝐵)) → 𝑅 Se (dom 𝑔 ∩ dom ))
3117frrlem4 33234 . . . . . . 7 ((𝑔𝐵𝐵) → ((𝑔 ↾ (dom 𝑔 ∩ dom )) Fn (dom 𝑔 ∩ dom ) ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom )((𝑔 ↾ (dom 𝑔 ∩ dom ))‘𝑎) = (𝑎𝐺((𝑔 ↾ (dom 𝑔 ∩ dom )) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ), 𝑎)))))
3231adantl 485 . . . . . 6 (((𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴) ∧ (𝑔𝐵𝐵)) → ((𝑔 ↾ (dom 𝑔 ∩ dom )) Fn (dom 𝑔 ∩ dom ) ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom )((𝑔 ↾ (dom 𝑔 ∩ dom ))‘𝑎) = (𝑎𝐺((𝑔 ↾ (dom 𝑔 ∩ dom )) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ), 𝑎)))))
3317frrlem4 33234 . . . . . . . . 9 ((𝐵𝑔𝐵) → (( ↾ (dom ∩ dom 𝑔)) Fn (dom ∩ dom 𝑔) ∧ ∀𝑎 ∈ (dom ∩ dom 𝑔)(( ↾ (dom ∩ dom 𝑔))‘𝑎) = (𝑎𝐺(( ↾ (dom ∩ dom 𝑔)) ↾ Pred(𝑅, (dom ∩ dom 𝑔), 𝑎)))))
34 incom 4131 . . . . . . . . . . . 12 (dom 𝑔 ∩ dom ) = (dom ∩ dom 𝑔)
3534reseq2i 5819 . . . . . . . . . . 11 ( ↾ (dom 𝑔 ∩ dom )) = ( ↾ (dom ∩ dom 𝑔))
36 fneq12 6423 . . . . . . . . . . 11 ((( ↾ (dom 𝑔 ∩ dom )) = ( ↾ (dom ∩ dom 𝑔)) ∧ (dom 𝑔 ∩ dom ) = (dom ∩ dom 𝑔)) → (( ↾ (dom 𝑔 ∩ dom )) Fn (dom 𝑔 ∩ dom ) ↔ ( ↾ (dom ∩ dom 𝑔)) Fn (dom ∩ dom 𝑔)))
3735, 34, 36mp2an 691 . . . . . . . . . 10 (( ↾ (dom 𝑔 ∩ dom )) Fn (dom 𝑔 ∩ dom ) ↔ ( ↾ (dom ∩ dom 𝑔)) Fn (dom ∩ dom 𝑔))
3835fveq1i 6650 . . . . . . . . . . . 12 (( ↾ (dom 𝑔 ∩ dom ))‘𝑎) = (( ↾ (dom ∩ dom 𝑔))‘𝑎)
39 predeq2 6123 . . . . . . . . . . . . . . 15 ((dom 𝑔 ∩ dom ) = (dom ∩ dom 𝑔) → Pred(𝑅, (dom 𝑔 ∩ dom ), 𝑎) = Pred(𝑅, (dom ∩ dom 𝑔), 𝑎))
4034, 39ax-mp 5 . . . . . . . . . . . . . 14 Pred(𝑅, (dom 𝑔 ∩ dom ), 𝑎) = Pred(𝑅, (dom ∩ dom 𝑔), 𝑎)
4135, 40reseq12i 5820 . . . . . . . . . . . . 13 (( ↾ (dom 𝑔 ∩ dom )) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ), 𝑎)) = (( ↾ (dom ∩ dom 𝑔)) ↾ Pred(𝑅, (dom ∩ dom 𝑔), 𝑎))
4241oveq2i 7150 . . . . . . . . . . . 12 (𝑎𝐺(( ↾ (dom 𝑔 ∩ dom )) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ), 𝑎))) = (𝑎𝐺(( ↾ (dom ∩ dom 𝑔)) ↾ Pred(𝑅, (dom ∩ dom 𝑔), 𝑎)))
4338, 42eqeq12i 2816 . . . . . . . . . . 11 ((( ↾ (dom 𝑔 ∩ dom ))‘𝑎) = (𝑎𝐺(( ↾ (dom 𝑔 ∩ dom )) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ), 𝑎))) ↔ (( ↾ (dom ∩ dom 𝑔))‘𝑎) = (𝑎𝐺(( ↾ (dom ∩ dom 𝑔)) ↾ Pred(𝑅, (dom ∩ dom 𝑔), 𝑎))))
4434, 43raleqbii 3200 . . . . . . . . . 10 (∀𝑎 ∈ (dom 𝑔 ∩ dom )(( ↾ (dom 𝑔 ∩ dom ))‘𝑎) = (𝑎𝐺(( ↾ (dom 𝑔 ∩ dom )) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ), 𝑎))) ↔ ∀𝑎 ∈ (dom ∩ dom 𝑔)(( ↾ (dom ∩ dom 𝑔))‘𝑎) = (𝑎𝐺(( ↾ (dom ∩ dom 𝑔)) ↾ Pred(𝑅, (dom ∩ dom 𝑔), 𝑎))))
4537, 44anbi12i 629 . . . . . . . . 9 ((( ↾ (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 𝑔), 𝑎)))))
4633, 45sylibr 237 . . . . . . . 8 ((𝐵𝑔𝐵) → (( ↾ (dom 𝑔 ∩ dom )) Fn (dom 𝑔 ∩ dom ) ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom )(( ↾ (dom 𝑔 ∩ dom ))‘𝑎) = (𝑎𝐺(( ↾ (dom 𝑔 ∩ dom )) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ), 𝑎)))))
4746ancoms 462 . . . . . . 7 ((𝑔𝐵𝐵) → (( ↾ (dom 𝑔 ∩ dom )) Fn (dom 𝑔 ∩ dom ) ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom )(( ↾ (dom 𝑔 ∩ dom ))‘𝑎) = (𝑎𝐺(( ↾ (dom 𝑔 ∩ dom )) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ), 𝑎)))))
4847adantl 485 . . . . . 6 (((𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴) ∧ (𝑔𝐵𝐵)) → (( ↾ (dom 𝑔 ∩ dom )) Fn (dom 𝑔 ∩ dom ) ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom )(( ↾ (dom 𝑔 ∩ dom ))‘𝑎) = (𝑎𝐺(( ↾ (dom 𝑔 ∩ dom )) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ), 𝑎)))))
49 fpr3g 33230 . . . . . 6 (((𝑅 Fr (dom 𝑔 ∩ dom ) ∧ 𝑅 Po (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 )))
5024, 27, 30, 32, 48, 49syl311anc 1381 . . . . 5 (((𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴) ∧ (𝑔𝐵𝐵)) → (𝑔 ↾ (dom 𝑔 ∩ dom )) = ( ↾ (dom 𝑔 ∩ dom )))
5150breqd 5044 . . . 4 (((𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴) ∧ (𝑔𝐵𝐵)) → (𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ))𝑣𝑥( ↾ (dom 𝑔 ∩ dom ))𝑣))
5251biimprd 251 . . 3 (((𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴) ∧ (𝑔𝐵𝐵)) → (𝑥( ↾ (dom 𝑔 ∩ dom ))𝑣𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ))𝑣))
5317frrlem2 33232 . . . . 5 (𝑔𝐵 → Fun 𝑔)
5453ad2antrl 727 . . . 4 (((𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴) ∧ (𝑔𝐵𝐵)) → Fun 𝑔)
55 funres 6370 . . . 4 (Fun 𝑔 → Fun (𝑔 ↾ (dom 𝑔 ∩ dom )))
56 dffun2 6338 . . . . 5 (Fun (𝑔 ↾ (dom 𝑔 ∩ dom )) ↔ (Rel (𝑔 ↾ (dom 𝑔 ∩ dom )) ∧ ∀𝑥𝑢𝑣((𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ))𝑢𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ))𝑣) → 𝑢 = 𝑣)))
57 2sp 2184 . . . . . 6 (∀𝑢𝑣((𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ))𝑢𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ))𝑣) → 𝑢 = 𝑣) → ((𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ))𝑢𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ))𝑣) → 𝑢 = 𝑣))
5857sps 2183 . . . . 5 (∀𝑥𝑢𝑣((𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ))𝑢𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ))𝑣) → 𝑢 = 𝑣) → ((𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ))𝑢𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ))𝑣) → 𝑢 = 𝑣))
5956, 58simplbiim 508 . . . 4 (Fun (𝑔 ↾ (dom 𝑔 ∩ dom )) → ((𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ))𝑢𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ))𝑣) → 𝑢 = 𝑣))
6054, 55, 593syl 18 . . 3 (((𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴) ∧ (𝑔𝐵𝐵)) → ((𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ))𝑢𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ))𝑣) → 𝑢 = 𝑣))
6152, 60sylan2d 607 . 2 (((𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴) ∧ (𝑔𝐵𝐵)) → ((𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ))𝑢𝑥( ↾ (dom 𝑔 ∩ dom ))𝑣) → 𝑢 = 𝑣))
6215, 61syl5 34 1 (((𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴) ∧ (𝑔𝐵𝐵)) → ((𝑥𝑔𝑢𝑥𝑣) → 𝑢 = 𝑣))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084  ∀wal 1536   = wceq 1538  ∃wex 1781   ∈ wcel 2112  {cab 2779  ∀wral 3109   ∩ cin 3883   ⊆ wss 3884   class class class wbr 5033   Po wpo 5440   Fr wfr 5479   Se wse 5480  dom cdm 5523   ↾ cres 5525  Rel wrel 5528  Predcpred 6119  Fun wfun 6322   Fn wfn 6323  ‘cfv 6328  (class class class)co 7139  frecscfrecs 33225 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 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298 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 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-ral 3114  df-rex 3115  df-rab 3118  df-v 3446  df-sbc 3724  df-csb 3832  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4247  df-if 4429  df-sn 4529  df-pr 4531  df-op 4535  df-uni 4804  df-br 5034  df-opab 5096  df-mpt 5114  df-id 5428  df-po 5442  df-fr 5482  df-se 5483  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-pred 6120  df-iota 6287  df-fun 6330  df-fn 6331  df-fv 6336  df-ov 7142 This theorem is referenced by:  fpr1  33247  fpr2  33248
 Copyright terms: Public domain W3C validator