This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem uptposlem

Description: Lemma for uptpos . (Contributed by Zhi Wang, 4-Nov-2025)

Ref Expression
Hypotheses oppcuprcl2.x ⊢ ( 𝜑 → 𝑋 ( ⟨ 𝐹 , 𝐺 ⟩ ( 𝑂 UP 𝑃 ) 𝑊 ) 𝑀 )
uptpos.h ⊢ ( 𝜑 → tpos 𝐺 = 𝐻 )
Assertion uptposlem ( 𝜑 → tpos 𝐻 = 𝐺 )

Proof

Step Hyp Ref Expression
1 oppcuprcl2.x ⊢ ( 𝜑 → 𝑋 ( ⟨ 𝐹 , 𝐺 ⟩ ( 𝑂 UP 𝑃 ) 𝑊 ) 𝑀 )
2 uptpos.h ⊢ ( 𝜑 → tpos 𝐺 = 𝐻 )
3 2 tposeqd ⊢ ( 𝜑 → tpos tpos 𝐺 = tpos 𝐻 )
4 eqid ⊢ ( Base ‘ 𝑂 ) = ( Base ‘ 𝑂 )
5 1 uprcl2 ⊢ ( 𝜑 → 𝐹 ( 𝑂 Func 𝑃 ) 𝐺 )
6 4 5 funcfn2 ⊢ ( 𝜑 → 𝐺 Fn ( ( Base ‘ 𝑂 ) × ( Base ‘ 𝑂 ) ) )
7 fnrel ⊢ ( 𝐺 Fn ( ( Base ‘ 𝑂 ) × ( Base ‘ 𝑂 ) ) → Rel 𝐺 )
8 6 7 syl ⊢ ( 𝜑 → Rel 𝐺 )
9 relxp ⊢ Rel ( ( Base ‘ 𝑂 ) × ( Base ‘ 𝑂 ) )
10 6 fndmd ⊢ ( 𝜑 → dom 𝐺 = ( ( Base ‘ 𝑂 ) × ( Base ‘ 𝑂 ) ) )
11 10 releqd ⊢ ( 𝜑 → ( Rel dom 𝐺 ↔ Rel ( ( Base ‘ 𝑂 ) × ( Base ‘ 𝑂 ) ) ) )
12 9 11 mpbiri ⊢ ( 𝜑 → Rel dom 𝐺 )
13 tpostpos2 ⊢ ( ( Rel 𝐺 ∧ Rel dom 𝐺 ) → tpos tpos 𝐺 = 𝐺 )
14 8 12 13 syl2anc ⊢ ( 𝜑 → tpos tpos 𝐺 = 𝐺 )
15 3 14 eqtr3d ⊢ ( 𝜑 → tpos 𝐻 = 𝐺 )