Metamath Proof Explorer


Theorem ltgseg

Description: The set E denotes the possible values of the congruence. (Contributed by Thierry Arnoux, 15-Dec-2019)

Ref Expression
Hypotheses legval.p 𝑃 = ( Base ‘ 𝐺 )
legval.d = ( dist ‘ 𝐺 )
legval.i 𝐼 = ( Itv ‘ 𝐺 )
legval.l = ( ≤G ‘ 𝐺 )
legval.g ( 𝜑𝐺 ∈ TarskiG )
legso.a 𝐸 = ( “ ( 𝑃 × 𝑃 ) )
legso.f ( 𝜑 → Fun )
ltgseg.p ( 𝜑𝐴𝐸 )
Assertion ltgseg ( 𝜑 → ∃ 𝑥𝑃𝑦𝑃 𝐴 = ( 𝑥 𝑦 ) )

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 legso.a 𝐸 = ( “ ( 𝑃 × 𝑃 ) )
7 legso.f ( 𝜑 → Fun )
8 ltgseg.p ( 𝜑𝐴𝐸 )
9 simp-4r ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝑃 × 𝑃 ) ) ∧ ( 𝑎 ) = 𝐴 ) ∧ 𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ 𝑎 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( 𝑎 ) = 𝐴 )
10 simpr ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝑃 × 𝑃 ) ) ∧ ( 𝑎 ) = 𝐴 ) ∧ 𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ 𝑎 = ⟨ 𝑥 , 𝑦 ⟩ ) → 𝑎 = ⟨ 𝑥 , 𝑦 ⟩ )
11 10 fveq2d ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝑃 × 𝑃 ) ) ∧ ( 𝑎 ) = 𝐴 ) ∧ 𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ 𝑎 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( 𝑎 ) = ( ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
12 9 11 eqtr3d ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝑃 × 𝑃 ) ) ∧ ( 𝑎 ) = 𝐴 ) ∧ 𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ 𝑎 = ⟨ 𝑥 , 𝑦 ⟩ ) → 𝐴 = ( ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
13 df-ov ( 𝑥 𝑦 ) = ( ‘ ⟨ 𝑥 , 𝑦 ⟩ )
14 12 13 eqtr4di ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝑃 × 𝑃 ) ) ∧ ( 𝑎 ) = 𝐴 ) ∧ 𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ 𝑎 = ⟨ 𝑥 , 𝑦 ⟩ ) → 𝐴 = ( 𝑥 𝑦 ) )
15 simplr ( ( ( 𝜑𝑎 ∈ ( 𝑃 × 𝑃 ) ) ∧ ( 𝑎 ) = 𝐴 ) → 𝑎 ∈ ( 𝑃 × 𝑃 ) )
16 elxp2 ( 𝑎 ∈ ( 𝑃 × 𝑃 ) ↔ ∃ 𝑥𝑃𝑦𝑃 𝑎 = ⟨ 𝑥 , 𝑦 ⟩ )
17 15 16 sylib ( ( ( 𝜑𝑎 ∈ ( 𝑃 × 𝑃 ) ) ∧ ( 𝑎 ) = 𝐴 ) → ∃ 𝑥𝑃𝑦𝑃 𝑎 = ⟨ 𝑥 , 𝑦 ⟩ )
18 14 17 reximddv2 ( ( ( 𝜑𝑎 ∈ ( 𝑃 × 𝑃 ) ) ∧ ( 𝑎 ) = 𝐴 ) → ∃ 𝑥𝑃𝑦𝑃 𝐴 = ( 𝑥 𝑦 ) )
19 8 6 eleqtrdi ( 𝜑𝐴 ∈ ( “ ( 𝑃 × 𝑃 ) ) )
20 fvelima ( ( Fun 𝐴 ∈ ( “ ( 𝑃 × 𝑃 ) ) ) → ∃ 𝑎 ∈ ( 𝑃 × 𝑃 ) ( 𝑎 ) = 𝐴 )
21 7 19 20 syl2anc ( 𝜑 → ∃ 𝑎 ∈ ( 𝑃 × 𝑃 ) ( 𝑎 ) = 𝐴 )
22 18 21 r19.29a ( 𝜑 → ∃ 𝑥𝑃𝑦𝑃 𝐴 = ( 𝑥 𝑦 ) )