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

Theorem fprlem1 8310
Description: Lemma for well-founded recursion with a partial order. 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 3475 . . . . 5 𝑥 ∈ V
2 vex 3475 . . . . 5 𝑢 ∈ V
31, 2breldm 5913 . . . 4 (𝑥𝑔𝑢𝑥 ∈ dom 𝑔)
4 vex 3475 . . . . 5 𝑣 ∈ V
51, 4breldm 5913 . . . 4 (𝑥𝑣𝑥 ∈ dom )
6 elin 3963 . . . . 5 (𝑥 ∈ (dom 𝑔 ∩ dom ) ↔ (𝑥 ∈ dom 𝑔𝑥 ∈ dom ))
76biimpri 227 . . . 4 ((𝑥 ∈ dom 𝑔𝑥 ∈ dom ) → 𝑥 ∈ (dom 𝑔 ∩ dom ))
83, 5, 7syl2an 594 . . 3 ((𝑥𝑔𝑢𝑥𝑣) → 𝑥 ∈ (dom 𝑔 ∩ dom ))
9 id 22 . . 3 ((𝑥𝑔𝑢𝑥𝑣) → (𝑥𝑔𝑢𝑥𝑣))
102brresi 5996 . . . . 5 (𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ))𝑢 ↔ (𝑥 ∈ (dom 𝑔 ∩ dom ) ∧ 𝑥𝑔𝑢))
114brresi 5996 . . . . 5 (𝑥( ↾ (dom 𝑔 ∩ dom ))𝑣 ↔ (𝑥 ∈ (dom 𝑔 ∩ dom ) ∧ 𝑥𝑣))
1210, 11anbi12i 626 . . . 4 ((𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ))𝑢𝑥( ↾ (dom 𝑔 ∩ dom ))𝑣) ↔ ((𝑥 ∈ (dom 𝑔 ∩ dom ) ∧ 𝑥𝑔𝑢) ∧ (𝑥 ∈ (dom 𝑔 ∩ dom ) ∧ 𝑥𝑣)))
13 an4 654 . . . 4 (((𝑥 ∈ (dom 𝑔 ∩ dom ) ∧ 𝑥𝑔𝑢) ∧ (𝑥 ∈ (dom 𝑔 ∩ dom ) ∧ 𝑥𝑣)) ↔ ((𝑥 ∈ (dom 𝑔 ∩ dom ) ∧ 𝑥 ∈ (dom 𝑔 ∩ dom )) ∧ (𝑥𝑔𝑢𝑥𝑣)))
1412, 13bitri 274 . . 3 ((𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ))𝑢𝑥( ↾ (dom 𝑔 ∩ dom ))𝑣) ↔ ((𝑥 ∈ (dom 𝑔 ∩ dom ) ∧ 𝑥 ∈ (dom 𝑔 ∩ dom )) ∧ (𝑥𝑔𝑢𝑥𝑣)))
158, 8, 9, 14syl21anbrc 1341 . 2 ((𝑥𝑔𝑢𝑥𝑣) → (𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ))𝑢𝑥( ↾ (dom 𝑔 ∩ dom ))𝑣))
16 inss2 4230 . . . . . . . . . 10 (dom 𝑔 ∩ dom ) ⊆ dom
17 fprlem.1 . . . . . . . . . . 11 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}
1817frrlem3 8298 . . . . . . . . . 10 (𝐵 → dom 𝐴)
1916, 18sstrid 3991 . . . . . . . . 9 (𝐵 → (dom 𝑔 ∩ dom ) ⊆ 𝐴)
2019adantl 480 . . . . . . . 8 ((𝑔𝐵𝐵) → (dom 𝑔 ∩ dom ) ⊆ 𝐴)
2120adantl 480 . . . . . . 7 (((𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴) ∧ (𝑔𝐵𝐵)) → (dom 𝑔 ∩ dom ) ⊆ 𝐴)
22 simpl1 1188 . . . . . . 7 (((𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴) ∧ (𝑔𝐵𝐵)) → 𝑅 Fr 𝐴)
23 frss 5647 . . . . . . 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 5594 . . . . . . 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 5649 . . . . . . 7 ((dom 𝑔 ∩ dom ) ⊆ 𝐴 → (𝑅 Se 𝐴𝑅 Se (dom 𝑔 ∩ dom )))
3021, 28, 29sylc 65 . . . . . 6 (((𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴) ∧ (𝑔𝐵𝐵)) → 𝑅 Se (dom 𝑔 ∩ dom ))
3117frrlem4 8299 . . . . . . 7 ((𝑔𝐵𝐵) → ((𝑔 ↾ (dom 𝑔 ∩ dom )) Fn (dom 𝑔 ∩ dom ) ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom )((𝑔 ↾ (dom 𝑔 ∩ dom ))‘𝑎) = (𝑎𝐺((𝑔 ↾ (dom 𝑔 ∩ dom )) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ), 𝑎)))))
3231adantl 480 . . . . . 6 (((𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴) ∧ (𝑔𝐵𝐵)) → ((𝑔 ↾ (dom 𝑔 ∩ dom )) Fn (dom 𝑔 ∩ dom ) ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom )((𝑔 ↾ (dom 𝑔 ∩ dom ))‘𝑎) = (𝑎𝐺((𝑔 ↾ (dom 𝑔 ∩ dom )) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ), 𝑎)))))
3317frrlem4 8299 . . . . . . . . 9 ((𝐵𝑔𝐵) → (( ↾ (dom ∩ dom 𝑔)) Fn (dom ∩ dom 𝑔) ∧ ∀𝑎 ∈ (dom ∩ dom 𝑔)(( ↾ (dom ∩ dom 𝑔))‘𝑎) = (𝑎𝐺(( ↾ (dom ∩ dom 𝑔)) ↾ Pred(𝑅, (dom ∩ dom 𝑔), 𝑎)))))
34 incom 4201 . . . . . . . . . . . 12 (dom 𝑔 ∩ dom ) = (dom ∩ dom 𝑔)
3534reseq2i 5984 . . . . . . . . . . 11 ( ↾ (dom 𝑔 ∩ dom )) = ( ↾ (dom ∩ dom 𝑔))
36 fneq12 6653 . . . . . . . . . . 11 ((( ↾ (dom 𝑔 ∩ dom )) = ( ↾ (dom ∩ dom 𝑔)) ∧ (dom 𝑔 ∩ dom ) = (dom ∩ dom 𝑔)) → (( ↾ (dom 𝑔 ∩ dom )) Fn (dom 𝑔 ∩ dom ) ↔ ( ↾ (dom ∩ dom 𝑔)) Fn (dom ∩ dom 𝑔)))
3735, 34, 36mp2an 690 . . . . . . . . . 10 (( ↾ (dom 𝑔 ∩ dom )) Fn (dom 𝑔 ∩ dom ) ↔ ( ↾ (dom ∩ dom 𝑔)) Fn (dom ∩ dom 𝑔))
3835fveq1i 6901 . . . . . . . . . . . 12 (( ↾ (dom 𝑔 ∩ dom ))‘𝑎) = (( ↾ (dom ∩ dom 𝑔))‘𝑎)
39 predeq2 6311 . . . . . . . . . . . . . . 15 ((dom 𝑔 ∩ dom ) = (dom ∩ dom 𝑔) → Pred(𝑅, (dom 𝑔 ∩ dom ), 𝑎) = Pred(𝑅, (dom ∩ dom 𝑔), 𝑎))
4034, 39ax-mp 5 . . . . . . . . . . . . . 14 Pred(𝑅, (dom 𝑔 ∩ dom ), 𝑎) = Pred(𝑅, (dom ∩ dom 𝑔), 𝑎)
4135, 40reseq12i 5985 . . . . . . . . . . . . 13 (( ↾ (dom 𝑔 ∩ dom )) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ), 𝑎)) = (( ↾ (dom ∩ dom 𝑔)) ↾ Pred(𝑅, (dom ∩ dom 𝑔), 𝑎))
4241oveq2i 7435 . . . . . . . . . . . 12 (𝑎𝐺(( ↾ (dom 𝑔 ∩ dom )) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ), 𝑎))) = (𝑎𝐺(( ↾ (dom ∩ dom 𝑔)) ↾ Pred(𝑅, (dom ∩ dom 𝑔), 𝑎)))
4338, 42eqeq12i 2745 . . . . . . . . . . 11 ((( ↾ (dom 𝑔 ∩ dom ))‘𝑎) = (𝑎𝐺(( ↾ (dom 𝑔 ∩ dom )) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ), 𝑎))) ↔ (( ↾ (dom ∩ dom 𝑔))‘𝑎) = (𝑎𝐺(( ↾ (dom ∩ dom 𝑔)) ↾ Pred(𝑅, (dom ∩ dom 𝑔), 𝑎))))
4434, 43raleqbii 3334 . . . . . . . . . 10 (∀𝑎 ∈ (dom 𝑔 ∩ dom )(( ↾ (dom 𝑔 ∩ dom ))‘𝑎) = (𝑎𝐺(( ↾ (dom 𝑔 ∩ dom )) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ), 𝑎))) ↔ ∀𝑎 ∈ (dom ∩ dom 𝑔)(( ↾ (dom ∩ dom 𝑔))‘𝑎) = (𝑎𝐺(( ↾ (dom ∩ dom 𝑔)) ↾ Pred(𝑅, (dom ∩ dom 𝑔), 𝑎))))
4537, 44anbi12i 626 . . . . . . . . 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 233 . . . . . . . 8 ((𝐵𝑔𝐵) → (( ↾ (dom 𝑔 ∩ dom )) Fn (dom 𝑔 ∩ dom ) ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom )(( ↾ (dom 𝑔 ∩ dom ))‘𝑎) = (𝑎𝐺(( ↾ (dom 𝑔 ∩ dom )) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ), 𝑎)))))
4746ancoms 457 . . . . . . 7 ((𝑔𝐵𝐵) → (( ↾ (dom 𝑔 ∩ dom )) Fn (dom 𝑔 ∩ dom ) ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom )(( ↾ (dom 𝑔 ∩ dom ))‘𝑎) = (𝑎𝐺(( ↾ (dom 𝑔 ∩ dom )) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ), 𝑎)))))
4847adantl 480 . . . . . 6 (((𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴) ∧ (𝑔𝐵𝐵)) → (( ↾ (dom 𝑔 ∩ dom )) Fn (dom 𝑔 ∩ dom ) ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom )(( ↾ (dom 𝑔 ∩ dom ))‘𝑎) = (𝑎𝐺(( ↾ (dom 𝑔 ∩ dom )) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ), 𝑎)))))
49 fpr3g 8295 . . . . . 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 5161 . . . 4 (((𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴) ∧ (𝑔𝐵𝐵)) → (𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ))𝑣𝑥( ↾ (dom 𝑔 ∩ dom ))𝑣))
5251biimprd 247 . . 3 (((𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴) ∧ (𝑔𝐵𝐵)) → (𝑥( ↾ (dom 𝑔 ∩ dom ))𝑣𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ))𝑣))
5317frrlem2 8297 . . . . 5 (𝑔𝐵 → Fun 𝑔)
5453ad2antrl 726 . . . 4 (((𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴) ∧ (𝑔𝐵𝐵)) → Fun 𝑔)
55 funres 6598 . . . 4 (Fun 𝑔 → Fun (𝑔 ↾ (dom 𝑔 ∩ dom )))
56 dffun2 6561 . . . . 5 (Fun (𝑔 ↾ (dom 𝑔 ∩ dom )) ↔ (Rel (𝑔 ↾ (dom 𝑔 ∩ dom )) ∧ ∀𝑥𝑢𝑣((𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ))𝑢𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ))𝑣) → 𝑢 = 𝑣)))
57 2sp 2174 . . . . . 6 (∀𝑢𝑣((𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ))𝑢𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ))𝑣) → 𝑢 = 𝑣) → ((𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ))𝑢𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ))𝑣) → 𝑢 = 𝑣))
5857sps 2173 . . . . 5 (∀𝑥𝑢𝑣((𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ))𝑢𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ))𝑣) → 𝑢 = 𝑣) → ((𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ))𝑢𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ))𝑣) → 𝑢 = 𝑣))
5956, 58simplbiim 503 . . . 4 (Fun (𝑔 ↾ (dom 𝑔 ∩ dom )) → ((𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ))𝑢𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ))𝑣) → 𝑢 = 𝑣))
6054, 55, 593syl 18 . . 3 (((𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴) ∧ (𝑔𝐵𝐵)) → ((𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ))𝑢𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ))𝑣) → 𝑢 = 𝑣))
6152, 60sylan2d 603 . 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 205  wa 394  w3a 1084  wal 1531   = wceq 1533  wex 1773  wcel 2098  {cab 2704  wral 3057  cin 3946  wss 3947   class class class wbr 5150   Po wpo 5590   Fr wfr 5632   Se wse 5633  dom cdm 5680  cres 5682  Rel wrel 5685  Predcpred 6307  Fun wfun 6545   Fn wfn 6546  cfv 6551  (class class class)co 7424  frecscfrecs 8290
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2698  ax-sep 5301  ax-nul 5308  ax-pr 5431
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2937  df-ral 3058  df-rex 3067  df-rab 3429  df-v 3473  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4325  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4911  df-br 5151  df-opab 5213  df-mpt 5234  df-id 5578  df-po 5592  df-fr 5635  df-se 5636  df-xp 5686  df-rel 5687  df-cnv 5688  df-co 5689  df-dm 5690  df-rn 5691  df-res 5692  df-ima 5693  df-pred 6308  df-iota 6503  df-fun 6553  df-fn 6554  df-fv 6559  df-ov 7427
This theorem is referenced by:  fpr2a  8312  fpr1  8313  fprfung  8319
  Copyright terms: Public domain W3C validator