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 syl5eq ( 𝜑 = { ⟨ 𝑒 , 𝑓 ⟩ ∣ ∃ 𝑥𝑃𝑦𝑃 ( 𝑓 = ( 𝑥 𝑦 ) ∧ ∃ 𝑧𝑃 ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∧ 𝑒 = ( 𝑥 𝑧 ) ) ) } )