Metamath Proof Explorer

Theorem legval

Description: Value of the less-than relationship. (Contributed by Thierry Arnoux, 21-Jun-2019)

Ref Expression
Hypotheses legval.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
legval.d ⊢ − = ( dist ‘ 𝐺 )
legval.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
legval.l ⊢ ≤ = ( ≤G ‘ 𝐺 )
legval.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
Assertion legval ( 𝜑 → ≤ = { ⟨ 𝑒 , 𝑓 ⟩ ∣ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( 𝑓 = ( 𝑥 − 𝑦 ) ∧ ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∧ 𝑒 = ( 𝑥 − 𝑧 ) ) ) } )

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 elex ⊢ ( 𝐺 ∈ TarskiG → 𝐺 ∈ V )
7 simp1 ⊢ ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) → 𝑝 = 𝑃 )
8 7 eqcomd ⊢ ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) → 𝑃 = 𝑝 )
9 simp2 ⊢ ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) → 𝑑 = − )
10 9 eqcomd ⊢ ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) → − = 𝑑 )
11 10 oveqd ⊢ ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) → ( 𝑥 − 𝑦 ) = ( 𝑥 𝑑 𝑦 ) )
12 11 eqeq2d ⊢ ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) → ( 𝑓 = ( 𝑥 − 𝑦 ) ↔ 𝑓 = ( 𝑥 𝑑 𝑦 ) ) )
13 simp3 ⊢ ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) → 𝑖 = 𝐼 )
14 13 eqcomd ⊢ ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) → 𝐼 = 𝑖 )
15 14 oveqd ⊢ ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) → ( 𝑥 𝐼 𝑦 ) = ( 𝑥 𝑖 𝑦 ) )
16 15 eleq2d ⊢ ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) → ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ↔ 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ) )
17 10 oveqd ⊢ ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) → ( 𝑥 − 𝑧 ) = ( 𝑥 𝑑 𝑧 ) )
18 17 eqeq2d ⊢ ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) → ( 𝑒 = ( 𝑥 − 𝑧 ) ↔ 𝑒 = ( 𝑥 𝑑 𝑧 ) ) )
19 16 18 anbi12d ⊢ ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) → ( ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∧ 𝑒 = ( 𝑥 − 𝑧 ) ) ↔ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∧ 𝑒 = ( 𝑥 𝑑 𝑧 ) ) ) )
20 8 19 rexeqbidv ⊢ ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) → ( ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∧ 𝑒 = ( 𝑥 − 𝑧 ) ) ↔ ∃ 𝑧 ∈ 𝑝 ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∧ 𝑒 = ( 𝑥 𝑑 𝑧 ) ) ) )
21 12 20 anbi12d ⊢ ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) → ( ( 𝑓 = ( 𝑥 − 𝑦 ) ∧ ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∧ 𝑒 = ( 𝑥 − 𝑧 ) ) ) ↔ ( 𝑓 = ( 𝑥 𝑑 𝑦 ) ∧ ∃ 𝑧 ∈ 𝑝 ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∧ 𝑒 = ( 𝑥 𝑑 𝑧 ) ) ) ) )
22 8 21 rexeqbidv ⊢ ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) → ( ∃ 𝑦 ∈ 𝑃 ( 𝑓 = ( 𝑥 − 𝑦 ) ∧ ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∧ 𝑒 = ( 𝑥 − 𝑧 ) ) ) ↔ ∃ 𝑦 ∈ 𝑝 ( 𝑓 = ( 𝑥 𝑑 𝑦 ) ∧ ∃ 𝑧 ∈ 𝑝 ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∧ 𝑒 = ( 𝑥 𝑑 𝑧 ) ) ) ) )
23 8 22 rexeqbidv ⊢ ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼 ) → ( ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( 𝑓 = ( 𝑥 − 𝑦 ) ∧ ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∧ 𝑒 = ( 𝑥 − 𝑧 ) ) ) ↔ ∃ 𝑥 ∈ 𝑝 ∃ 𝑦 ∈ 𝑝 ( 𝑓 = ( 𝑥 𝑑 𝑦 ) ∧ ∃ 𝑧 ∈ 𝑝 ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∧ 𝑒 = ( 𝑥 𝑑 𝑧 ) ) ) ) )
24 1 2 3 23 sbcie3s ⊢ ( 𝑔 = 𝐺 → ( [ ( Base ‘ 𝑔 ) / 𝑝 ] [ ( dist ‘ 𝑔 ) / 𝑑 ] [ ( Itv ‘ 𝑔 ) / 𝑖 ] ∃ 𝑥 ∈ 𝑝 ∃ 𝑦 ∈ 𝑝 ( 𝑓 = ( 𝑥 𝑑 𝑦 ) ∧ ∃ 𝑧 ∈ 𝑝 ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∧ 𝑒 = ( 𝑥 𝑑 𝑧 ) ) ) ↔ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( 𝑓 = ( 𝑥 − 𝑦 ) ∧ ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∧ 𝑒 = ( 𝑥 − 𝑧 ) ) ) ) )
25 24 opabbidv ⊢ ( 𝑔 = 𝐺 → { ⟨ 𝑒 , 𝑓 ⟩ ∣ [ ( Base ‘ 𝑔 ) / 𝑝 ] [ ( dist ‘ 𝑔 ) / 𝑑 ] [ ( Itv ‘ 𝑔 ) / 𝑖 ] ∃ 𝑥 ∈ 𝑝 ∃ 𝑦 ∈ 𝑝 ( 𝑓 = ( 𝑥 𝑑 𝑦 ) ∧ ∃ 𝑧 ∈ 𝑝 ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∧ 𝑒 = ( 𝑥 𝑑 𝑧 ) ) ) } = { ⟨ 𝑒 , 𝑓 ⟩ ∣ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( 𝑓 = ( 𝑥 − 𝑦 ) ∧ ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∧ 𝑒 = ( 𝑥 − 𝑧 ) ) ) } )
26 df-leg ⊢ ≤G = ( 𝑔 ∈ V ↦ { ⟨ 𝑒 , 𝑓 ⟩ ∣ [ ( Base ‘ 𝑔 ) / 𝑝 ] [ ( dist ‘ 𝑔 ) / 𝑑 ] [ ( Itv ‘ 𝑔 ) / 𝑖 ] ∃ 𝑥 ∈ 𝑝 ∃ 𝑦 ∈ 𝑝 ( 𝑓 = ( 𝑥 𝑑 𝑦 ) ∧ ∃ 𝑧 ∈ 𝑝 ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∧ 𝑒 = ( 𝑥 𝑑 𝑧 ) ) ) } )
27 2 fvexi ⊢ − ∈ V
28 27 imaex ⊢ ( − “ ( 𝑃 × 𝑃 ) ) ∈ V
29 p0ex ⊢ { ∅ } ∈ V
30 28 29 unex ⊢ ( ( − “ ( 𝑃 × 𝑃 ) ) ∪ { ∅ } ) ∈ V
31 30 a1i ⊢ ( ⊤ → ( ( − “ ( 𝑃 × 𝑃 ) ) ∪ { ∅ } ) ∈ V )
32 simprr ⊢ ( ( ( ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑓 = ( 𝑥 − 𝑦 ) ∧ ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∧ 𝑒 = ( 𝑥 − 𝑧 ) ) ) ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ∈ ( 𝑥 𝐼 𝑦 ) ∧ 𝑒 = ( 𝑥 − 𝑑 ) ) ) → 𝑒 = ( 𝑥 − 𝑑 ) )
33 ovima0 ⊢ ( ( 𝑥 ∈ 𝑃 ∧ 𝑑 ∈ 𝑃 ) → ( 𝑥 − 𝑑 ) ∈ ( ( − “ ( 𝑃 × 𝑃 ) ) ∪ { ∅ } ) )
34 33 ad5ant14 ⊢ ( ( ( ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑓 = ( 𝑥 − 𝑦 ) ∧ ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∧ 𝑒 = ( 𝑥 − 𝑧 ) ) ) ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ∈ ( 𝑥 𝐼 𝑦 ) ∧ 𝑒 = ( 𝑥 − 𝑑 ) ) ) → ( 𝑥 − 𝑑 ) ∈ ( ( − “ ( 𝑃 × 𝑃 ) ) ∪ { ∅ } ) )
35 32 34 eqeltrd ⊢ ( ( ( ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑓 = ( 𝑥 − 𝑦 ) ∧ ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∧ 𝑒 = ( 𝑥 − 𝑧 ) ) ) ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ∈ ( 𝑥 𝐼 𝑦 ) ∧ 𝑒 = ( 𝑥 − 𝑑 ) ) ) → 𝑒 ∈ ( ( − “ ( 𝑃 × 𝑃 ) ) ∪ { ∅ } ) )
36 simpllr ⊢ ( ( ( ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑓 = ( 𝑥 − 𝑦 ) ∧ ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∧ 𝑒 = ( 𝑥 − 𝑧 ) ) ) ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ∈ ( 𝑥 𝐼 𝑦 ) ∧ 𝑒 = ( 𝑥 − 𝑑 ) ) ) → ( 𝑓 = ( 𝑥 − 𝑦 ) ∧ ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∧ 𝑒 = ( 𝑥 − 𝑧 ) ) ) )
37 36 simpld ⊢ ( ( ( ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑓 = ( 𝑥 − 𝑦 ) ∧ ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∧ 𝑒 = ( 𝑥 − 𝑧 ) ) ) ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ∈ ( 𝑥 𝐼 𝑦 ) ∧ 𝑒 = ( 𝑥 − 𝑑 ) ) ) → 𝑓 = ( 𝑥 − 𝑦 ) )
38 ovima0 ⊢ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃 ) → ( 𝑥 − 𝑦 ) ∈ ( ( − “ ( 𝑃 × 𝑃 ) ) ∪ { ∅ } ) )
39 38 ad3antrrr ⊢ ( ( ( ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑓 = ( 𝑥 − 𝑦 ) ∧ ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∧ 𝑒 = ( 𝑥 − 𝑧 ) ) ) ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ∈ ( 𝑥 𝐼 𝑦 ) ∧ 𝑒 = ( 𝑥 − 𝑑 ) ) ) → ( 𝑥 − 𝑦 ) ∈ ( ( − “ ( 𝑃 × 𝑃 ) ) ∪ { ∅ } ) )
40 37 39 eqeltrd ⊢ ( ( ( ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑓 = ( 𝑥 − 𝑦 ) ∧ ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∧ 𝑒 = ( 𝑥 − 𝑧 ) ) ) ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ∈ ( 𝑥 𝐼 𝑦 ) ∧ 𝑒 = ( 𝑥 − 𝑑 ) ) ) → 𝑓 ∈ ( ( − “ ( 𝑃 × 𝑃 ) ) ∪ { ∅ } ) )
41 35 40 jca ⊢ ( ( ( ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑓 = ( 𝑥 − 𝑦 ) ∧ ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∧ 𝑒 = ( 𝑥 − 𝑧 ) ) ) ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ∈ ( 𝑥 𝐼 𝑦 ) ∧ 𝑒 = ( 𝑥 − 𝑑 ) ) ) → ( 𝑒 ∈ ( ( − “ ( 𝑃 × 𝑃 ) ) ∪ { ∅ } ) ∧ 𝑓 ∈ ( ( − “ ( 𝑃 × 𝑃 ) ) ∪ { ∅ } ) ) )
42 simprr ⊢ ( ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑓 = ( 𝑥 − 𝑦 ) ∧ ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∧ 𝑒 = ( 𝑥 − 𝑧 ) ) ) ) → ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∧ 𝑒 = ( 𝑥 − 𝑧 ) ) )
43 eleq1w ⊢ ( 𝑧 = 𝑑 → ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ↔ 𝑑 ∈ ( 𝑥 𝐼 𝑦 ) ) )
44 oveq2 ⊢ ( 𝑧 = 𝑑 → ( 𝑥 − 𝑧 ) = ( 𝑥 − 𝑑 ) )
45 44 eqeq2d ⊢ ( 𝑧 = 𝑑 → ( 𝑒 = ( 𝑥 − 𝑧 ) ↔ 𝑒 = ( 𝑥 − 𝑑 ) ) )
46 43 45 anbi12d ⊢ ( 𝑧 = 𝑑 → ( ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∧ 𝑒 = ( 𝑥 − 𝑧 ) ) ↔ ( 𝑑 ∈ ( 𝑥 𝐼 𝑦 ) ∧ 𝑒 = ( 𝑥 − 𝑑 ) ) ) )
47 46 cbvrexvw ⊢ ( ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∧ 𝑒 = ( 𝑥 − 𝑧 ) ) ↔ ∃ 𝑑 ∈ 𝑃 ( 𝑑 ∈ ( 𝑥 𝐼 𝑦 ) ∧ 𝑒 = ( 𝑥 − 𝑑 ) ) )
48 42 47 sylib ⊢ ( ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑓 = ( 𝑥 − 𝑦 ) ∧ ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∧ 𝑒 = ( 𝑥 − 𝑧 ) ) ) ) → ∃ 𝑑 ∈ 𝑃 ( 𝑑 ∈ ( 𝑥 𝐼 𝑦 ) ∧ 𝑒 = ( 𝑥 − 𝑑 ) ) )
49 41 48 r19.29a ⊢ ( ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑓 = ( 𝑥 − 𝑦 ) ∧ ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∧ 𝑒 = ( 𝑥 − 𝑧 ) ) ) ) → ( 𝑒 ∈ ( ( − “ ( 𝑃 × 𝑃 ) ) ∪ { ∅ } ) ∧ 𝑓 ∈ ( ( − “ ( 𝑃 × 𝑃 ) ) ∪ { ∅ } ) ) )
50 49 ex ⊢ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃 ) → ( ( 𝑓 = ( 𝑥 − 𝑦 ) ∧ ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∧ 𝑒 = ( 𝑥 − 𝑧 ) ) ) → ( 𝑒 ∈ ( ( − “ ( 𝑃 × 𝑃 ) ) ∪ { ∅ } ) ∧ 𝑓 ∈ ( ( − “ ( 𝑃 × 𝑃 ) ) ∪ { ∅ } ) ) ) )
51 50 rexlimivv ⊢ ( ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( 𝑓 = ( 𝑥 − 𝑦 ) ∧ ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∧ 𝑒 = ( 𝑥 − 𝑧 ) ) ) → ( 𝑒 ∈ ( ( − “ ( 𝑃 × 𝑃 ) ) ∪ { ∅ } ) ∧ 𝑓 ∈ ( ( − “ ( 𝑃 × 𝑃 ) ) ∪ { ∅ } ) ) )
52 51 adantl ⊢ ( ( ⊤ ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( 𝑓 = ( 𝑥 − 𝑦 ) ∧ ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∧ 𝑒 = ( 𝑥 − 𝑧 ) ) ) ) → ( 𝑒 ∈ ( ( − “ ( 𝑃 × 𝑃 ) ) ∪ { ∅ } ) ∧ 𝑓 ∈ ( ( − “ ( 𝑃 × 𝑃 ) ) ∪ { ∅ } ) ) )
53 52 simpld ⊢ ( ( ⊤ ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( 𝑓 = ( 𝑥 − 𝑦 ) ∧ ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∧ 𝑒 = ( 𝑥 − 𝑧 ) ) ) ) → 𝑒 ∈ ( ( − “ ( 𝑃 × 𝑃 ) ) ∪ { ∅ } ) )
54 52 simprd ⊢ ( ( ⊤ ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( 𝑓 = ( 𝑥 − 𝑦 ) ∧ ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∧ 𝑒 = ( 𝑥 − 𝑧 ) ) ) ) → 𝑓 ∈ ( ( − “ ( 𝑃 × 𝑃 ) ) ∪ { ∅ } ) )
55 31 31 53 54 opabex2 ⊢ ( ⊤ → { ⟨ 𝑒 , 𝑓 ⟩ ∣ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( 𝑓 = ( 𝑥 − 𝑦 ) ∧ ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∧ 𝑒 = ( 𝑥 − 𝑧 ) ) ) } ∈ V )
56 55 mptru ⊢ { ⟨ 𝑒 , 𝑓 ⟩ ∣ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( 𝑓 = ( 𝑥 − 𝑦 ) ∧ ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∧ 𝑒 = ( 𝑥 − 𝑧 ) ) ) } ∈ V
57 25 26 56 fvmpt ⊢ ( 𝐺 ∈ V → ( ≤G ‘ 𝐺 ) = { ⟨ 𝑒 , 𝑓 ⟩ ∣ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( 𝑓 = ( 𝑥 − 𝑦 ) ∧ ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∧ 𝑒 = ( 𝑥 − 𝑧 ) ) ) } )
58 5 6 57 3syl ⊢ ( 𝜑 → ( ≤G ‘ 𝐺 ) = { ⟨ 𝑒 , 𝑓 ⟩ ∣ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( 𝑓 = ( 𝑥 − 𝑦 ) ∧ ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∧ 𝑒 = ( 𝑥 − 𝑧 ) ) ) } )
59 4 58 eqtrid ⊢ ( 𝜑 → ≤ = { ⟨ 𝑒 , 𝑓 ⟩ ∣ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( 𝑓 = ( 𝑥 − 𝑦 ) ∧ ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∧ 𝑒 = ( 𝑥 − 𝑧 ) ) ) } )