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

Metamath Proof Explorer

Theorem ajmoi

Description: Every operator has at most one adjoint. (Contributed by NM, 25-Jan-2008) (New usage is discouraged.)

Ref Expression
Hypotheses ip2eqi.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
ip2eqi.7 ⊢ 𝑃 = ( ·𝑖OLD ‘ 𝑈 )
ip2eqi.u ⊢ 𝑈 ∈ CPreHilOLD
Assertion ajmoi ∃* 𝑠 ( 𝑠 : 𝑌 ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ( ( 𝑇 ‘ 𝑥 ) 𝑄 𝑦 ) = ( 𝑥 𝑃 ( 𝑠 ‘ 𝑦 ) ) )

Proof

Step Hyp Ref Expression
1 ip2eqi.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2 ip2eqi.7 ⊢ 𝑃 = ( ·𝑖OLD ‘ 𝑈 )
3 ip2eqi.u ⊢ 𝑈 ∈ CPreHilOLD
4 r19.26-2 ⊢ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ( ( ( 𝑇 ‘ 𝑥 ) 𝑄 𝑦 ) = ( 𝑥 𝑃 ( 𝑠 ‘ 𝑦 ) ) ∧ ( ( 𝑇 ‘ 𝑥 ) 𝑄 𝑦 ) = ( 𝑥 𝑃 ( 𝑡 ‘ 𝑦 ) ) ) ↔ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ( ( 𝑇 ‘ 𝑥 ) 𝑄 𝑦 ) = ( 𝑥 𝑃 ( 𝑠 ‘ 𝑦 ) ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ( ( 𝑇 ‘ 𝑥 ) 𝑄 𝑦 ) = ( 𝑥 𝑃 ( 𝑡 ‘ 𝑦 ) ) ) )
5 eqtr2 ⊢ ( ( ( ( 𝑇 ‘ 𝑥 ) 𝑄 𝑦 ) = ( 𝑥 𝑃 ( 𝑠 ‘ 𝑦 ) ) ∧ ( ( 𝑇 ‘ 𝑥 ) 𝑄 𝑦 ) = ( 𝑥 𝑃 ( 𝑡 ‘ 𝑦 ) ) ) → ( 𝑥 𝑃 ( 𝑠 ‘ 𝑦 ) ) = ( 𝑥 𝑃 ( 𝑡 ‘ 𝑦 ) ) )
6 5 2ralimi ⊢ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ( ( ( 𝑇 ‘ 𝑥 ) 𝑄 𝑦 ) = ( 𝑥 𝑃 ( 𝑠 ‘ 𝑦 ) ) ∧ ( ( 𝑇 ‘ 𝑥 ) 𝑄 𝑦 ) = ( 𝑥 𝑃 ( 𝑡 ‘ 𝑦 ) ) ) → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ( 𝑥 𝑃 ( 𝑠 ‘ 𝑦 ) ) = ( 𝑥 𝑃 ( 𝑡 ‘ 𝑦 ) ) )
7 4 6 sylbir ⊢ ( ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ( ( 𝑇 ‘ 𝑥 ) 𝑄 𝑦 ) = ( 𝑥 𝑃 ( 𝑠 ‘ 𝑦 ) ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ( ( 𝑇 ‘ 𝑥 ) 𝑄 𝑦 ) = ( 𝑥 𝑃 ( 𝑡 ‘ 𝑦 ) ) ) → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ( 𝑥 𝑃 ( 𝑠 ‘ 𝑦 ) ) = ( 𝑥 𝑃 ( 𝑡 ‘ 𝑦 ) ) )
8 1 2 3 phoeqi ⊢ ( ( 𝑠 : 𝑌 ⟶ 𝑋 ∧ 𝑡 : 𝑌 ⟶ 𝑋 ) → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ( 𝑥 𝑃 ( 𝑠 ‘ 𝑦 ) ) = ( 𝑥 𝑃 ( 𝑡 ‘ 𝑦 ) ) ↔ 𝑠 = 𝑡 ) )
9 8 biimpa ⊢ ( ( ( 𝑠 : 𝑌 ⟶ 𝑋 ∧ 𝑡 : 𝑌 ⟶ 𝑋 ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ( 𝑥 𝑃 ( 𝑠 ‘ 𝑦 ) ) = ( 𝑥 𝑃 ( 𝑡 ‘ 𝑦 ) ) ) → 𝑠 = 𝑡 )
10 7 9 sylan2 ⊢ ( ( ( 𝑠 : 𝑌 ⟶ 𝑋 ∧ 𝑡 : 𝑌 ⟶ 𝑋 ) ∧ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ( ( 𝑇 ‘ 𝑥 ) 𝑄 𝑦 ) = ( 𝑥 𝑃 ( 𝑠 ‘ 𝑦 ) ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ( ( 𝑇 ‘ 𝑥 ) 𝑄 𝑦 ) = ( 𝑥 𝑃 ( 𝑡 ‘ 𝑦 ) ) ) ) → 𝑠 = 𝑡 )
11 10 an4s ⊢ ( ( ( 𝑠 : 𝑌 ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ( ( 𝑇 ‘ 𝑥 ) 𝑄 𝑦 ) = ( 𝑥 𝑃 ( 𝑠 ‘ 𝑦 ) ) ) ∧ ( 𝑡 : 𝑌 ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ( ( 𝑇 ‘ 𝑥 ) 𝑄 𝑦 ) = ( 𝑥 𝑃 ( 𝑡 ‘ 𝑦 ) ) ) ) → 𝑠 = 𝑡 )
12 11 gen2 ⊢ ∀ 𝑠 ∀ 𝑡 ( ( ( 𝑠 : 𝑌 ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ( ( 𝑇 ‘ 𝑥 ) 𝑄 𝑦 ) = ( 𝑥 𝑃 ( 𝑠 ‘ 𝑦 ) ) ) ∧ ( 𝑡 : 𝑌 ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ( ( 𝑇 ‘ 𝑥 ) 𝑄 𝑦 ) = ( 𝑥 𝑃 ( 𝑡 ‘ 𝑦 ) ) ) ) → 𝑠 = 𝑡 )
13 feq1 ⊢ ( 𝑠 = 𝑡 → ( 𝑠 : 𝑌 ⟶ 𝑋 ↔ 𝑡 : 𝑌 ⟶ 𝑋 ) )
14 fveq1 ⊢ ( 𝑠 = 𝑡 → ( 𝑠 ‘ 𝑦 ) = ( 𝑡 ‘ 𝑦 ) )
15 14 oveq2d ⊢ ( 𝑠 = 𝑡 → ( 𝑥 𝑃 ( 𝑠 ‘ 𝑦 ) ) = ( 𝑥 𝑃 ( 𝑡 ‘ 𝑦 ) ) )
16 15 eqeq2d ⊢ ( 𝑠 = 𝑡 → ( ( ( 𝑇 ‘ 𝑥 ) 𝑄 𝑦 ) = ( 𝑥 𝑃 ( 𝑠 ‘ 𝑦 ) ) ↔ ( ( 𝑇 ‘ 𝑥 ) 𝑄 𝑦 ) = ( 𝑥 𝑃 ( 𝑡 ‘ 𝑦 ) ) ) )
17 16 2ralbidv ⊢ ( 𝑠 = 𝑡 → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ( ( 𝑇 ‘ 𝑥 ) 𝑄 𝑦 ) = ( 𝑥 𝑃 ( 𝑠 ‘ 𝑦 ) ) ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ( ( 𝑇 ‘ 𝑥 ) 𝑄 𝑦 ) = ( 𝑥 𝑃 ( 𝑡 ‘ 𝑦 ) ) ) )
18 13 17 anbi12d ⊢ ( 𝑠 = 𝑡 → ( ( 𝑠 : 𝑌 ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ( ( 𝑇 ‘ 𝑥 ) 𝑄 𝑦 ) = ( 𝑥 𝑃 ( 𝑠 ‘ 𝑦 ) ) ) ↔ ( 𝑡 : 𝑌 ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ( ( 𝑇 ‘ 𝑥 ) 𝑄 𝑦 ) = ( 𝑥 𝑃 ( 𝑡 ‘ 𝑦 ) ) ) ) )
19 18 mo4 ⊢ ( ∃* 𝑠 ( 𝑠 : 𝑌 ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ( ( 𝑇 ‘ 𝑥 ) 𝑄 𝑦 ) = ( 𝑥 𝑃 ( 𝑠 ‘ 𝑦 ) ) ) ↔ ∀ 𝑠 ∀ 𝑡 ( ( ( 𝑠 : 𝑌 ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ( ( 𝑇 ‘ 𝑥 ) 𝑄 𝑦 ) = ( 𝑥 𝑃 ( 𝑠 ‘ 𝑦 ) ) ) ∧ ( 𝑡 : 𝑌 ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ( ( 𝑇 ‘ 𝑥 ) 𝑄 𝑦 ) = ( 𝑥 𝑃 ( 𝑡 ‘ 𝑦 ) ) ) ) → 𝑠 = 𝑡 ) )
20 12 19 mpbir ⊢ ∃* 𝑠 ( 𝑠 : 𝑌 ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ( ( 𝑇 ‘ 𝑥 ) 𝑄 𝑦 ) = ( 𝑥 𝑃 ( 𝑠 ‘ 𝑦 ) ) )