Metamath Proof Explorer


Theorem legid

Description: Reflexivity of the less-than relationship. Proposition 5.7 of Schwabhauser p. 42. (Contributed by Thierry Arnoux, 27-Jun-2019)

Ref Expression
Hypotheses legval.p 𝑃 = ( Base ‘ 𝐺 )
legval.d = ( dist ‘ 𝐺 )
legval.i 𝐼 = ( Itv ‘ 𝐺 )
legval.l = ( ≤G ‘ 𝐺 )
legval.g ( 𝜑𝐺 ∈ TarskiG )
legid.a ( 𝜑𝐴𝑃 )
legid.b ( 𝜑𝐵𝑃 )
Assertion legid ( 𝜑 → ( 𝐴 𝐵 ) ( 𝐴 𝐵 ) )

Proof

Step Hyp Ref Expression
1 legval.p 𝑃 = ( Base ‘ 𝐺 )
2 legval.d = ( dist ‘ 𝐺 )
3 legval.i 𝐼 = ( Itv ‘ 𝐺 )
4 legval.l = ( ≤G ‘ 𝐺 )
5 legval.g ( 𝜑𝐺 ∈ TarskiG )
6 legid.a ( 𝜑𝐴𝑃 )
7 legid.b ( 𝜑𝐵𝑃 )
8 1 2 3 5 6 7 tgbtwntriv2 ( 𝜑𝐵 ∈ ( 𝐴 𝐼 𝐵 ) )
9 eqidd ( 𝜑 → ( 𝐴 𝐵 ) = ( 𝐴 𝐵 ) )
10 eleq1 ( 𝑥 = 𝐵 → ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ↔ 𝐵 ∈ ( 𝐴 𝐼 𝐵 ) ) )
11 oveq2 ( 𝑥 = 𝐵 → ( 𝐴 𝑥 ) = ( 𝐴 𝐵 ) )
12 11 eqeq2d ( 𝑥 = 𝐵 → ( ( 𝐴 𝐵 ) = ( 𝐴 𝑥 ) ↔ ( 𝐴 𝐵 ) = ( 𝐴 𝐵 ) ) )
13 10 12 anbi12d ( 𝑥 = 𝐵 → ( ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ ( 𝐴 𝐵 ) = ( 𝐴 𝑥 ) ) ↔ ( 𝐵 ∈ ( 𝐴 𝐼 𝐵 ) ∧ ( 𝐴 𝐵 ) = ( 𝐴 𝐵 ) ) ) )
14 13 rspcev ( ( 𝐵𝑃 ∧ ( 𝐵 ∈ ( 𝐴 𝐼 𝐵 ) ∧ ( 𝐴 𝐵 ) = ( 𝐴 𝐵 ) ) ) → ∃ 𝑥𝑃 ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ ( 𝐴 𝐵 ) = ( 𝐴 𝑥 ) ) )
15 7 8 9 14 syl12anc ( 𝜑 → ∃ 𝑥𝑃 ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ ( 𝐴 𝐵 ) = ( 𝐴 𝑥 ) ) )
16 1 2 3 4 5 6 7 6 7 legov ( 𝜑 → ( ( 𝐴 𝐵 ) ( 𝐴 𝐵 ) ↔ ∃ 𝑥𝑃 ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ ( 𝐴 𝐵 ) = ( 𝐴 𝑥 ) ) ) )
17 15 16 mpbird ( 𝜑 → ( 𝐴 𝐵 ) ( 𝐴 𝐵 ) )