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

Metamath Proof Explorer

Theorem functermclem

Description: Lemma for functermc . (Contributed by Zhi Wang, 17-Oct-2025)

Ref Expression
Hypotheses functermclem.1 ⊢ ( ( 𝜑 ∧ 𝐾 𝑅 𝐿 ) → 𝐾 = 𝐹 )
functermclem.2 ⊢ ( 𝜑 → ( 𝐹 𝑅 𝐿 ↔ 𝐿 = 𝐺 ) )
Assertion functermclem ( 𝜑 → ( 𝐾 𝑅 𝐿 ↔ ( 𝐾 = 𝐹 ∧ 𝐿 = 𝐺 ) ) )

Proof

Step Hyp Ref Expression
1 functermclem.1 ⊢ ( ( 𝜑 ∧ 𝐾 𝑅 𝐿 ) → 𝐾 = 𝐹 )
2 functermclem.2 ⊢ ( 𝜑 → ( 𝐹 𝑅 𝐿 ↔ 𝐿 = 𝐺 ) )
3 simpr ⊢ ( ( 𝜑 ∧ 𝐾 𝑅 𝐿 ) → 𝐾 𝑅 𝐿 )
4 1 3 eqbrtrrd ⊢ ( ( 𝜑 ∧ 𝐾 𝑅 𝐿 ) → 𝐹 𝑅 𝐿 )
5 2 biimpa ⊢ ( ( 𝜑 ∧ 𝐹 𝑅 𝐿 ) → 𝐿 = 𝐺 )
6 4 5 syldan ⊢ ( ( 𝜑 ∧ 𝐾 𝑅 𝐿 ) → 𝐿 = 𝐺 )
7 1 6 jca ⊢ ( ( 𝜑 ∧ 𝐾 𝑅 𝐿 ) → ( 𝐾 = 𝐹 ∧ 𝐿 = 𝐺 ) )
8 simprl ⊢ ( ( 𝜑 ∧ ( 𝐾 = 𝐹 ∧ 𝐿 = 𝐺 ) ) → 𝐾 = 𝐹 )
9 2 biimpar ⊢ ( ( 𝜑 ∧ 𝐿 = 𝐺 ) → 𝐹 𝑅 𝐿 )
10 9 adantrl ⊢ ( ( 𝜑 ∧ ( 𝐾 = 𝐹 ∧ 𝐿 = 𝐺 ) ) → 𝐹 𝑅 𝐿 )
11 8 10 eqbrtrd ⊢ ( ( 𝜑 ∧ ( 𝐾 = 𝐹 ∧ 𝐿 = 𝐺 ) ) → 𝐾 𝑅 𝐿 )
12 7 11 impbida ⊢ ( 𝜑 → ( 𝐾 𝑅 𝐿 ↔ ( 𝐾 = 𝐹 ∧ 𝐿 = 𝐺 ) ) )