Metamath Proof Explorer


Theorem legtrd

Description: Transitivity of the less-than relationship. Proposition 5.8 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 ( 𝜑𝐵𝑃 )
legtrd.c ( 𝜑𝐶𝑃 )
legtrd.d ( 𝜑𝐷𝑃 )
legtrd.e ( 𝜑𝐸𝑃 )
legtrd.f ( 𝜑𝐹𝑃 )
legtrd.1 ( 𝜑 → ( 𝐴 𝐵 ) ( 𝐶 𝐷 ) )
legtrd.2 ( 𝜑 → ( 𝐶 𝐷 ) ( 𝐸 𝐹 ) )
Assertion legtrd ( 𝜑 → ( 𝐴 𝐵 ) ( 𝐸 𝐹 ) )

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 legtrd.c ( 𝜑𝐶𝑃 )
9 legtrd.d ( 𝜑𝐷𝑃 )
10 legtrd.e ( 𝜑𝐸𝑃 )
11 legtrd.f ( 𝜑𝐹𝑃 )
12 legtrd.1 ( 𝜑 → ( 𝐴 𝐵 ) ( 𝐶 𝐷 ) )
13 legtrd.2 ( 𝜑 → ( 𝐶 𝐷 ) ( 𝐸 𝐹 ) )
14 eqid ( LineG ‘ 𝐺 ) = ( LineG ‘ 𝐺 )
15 5 ad4antr ( ( ( ( ( 𝜑𝑥𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 𝐵 ) = ( 𝐶 𝑥 ) ) ) ∧ 𝑦𝑃 ) ∧ ( 𝑦 ∈ ( 𝐸 𝐼 𝐹 ) ∧ ( 𝐶 𝐷 ) = ( 𝐸 𝑦 ) ) ) → 𝐺 ∈ TarskiG )
16 8 ad4antr ( ( ( ( ( 𝜑𝑥𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 𝐵 ) = ( 𝐶 𝑥 ) ) ) ∧ 𝑦𝑃 ) ∧ ( 𝑦 ∈ ( 𝐸 𝐼 𝐹 ) ∧ ( 𝐶 𝐷 ) = ( 𝐸 𝑦 ) ) ) → 𝐶𝑃 )
17 9 ad4antr ( ( ( ( ( 𝜑𝑥𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 𝐵 ) = ( 𝐶 𝑥 ) ) ) ∧ 𝑦𝑃 ) ∧ ( 𝑦 ∈ ( 𝐸 𝐼 𝐹 ) ∧ ( 𝐶 𝐷 ) = ( 𝐸 𝑦 ) ) ) → 𝐷𝑃 )
18 simp-4r ( ( ( ( ( 𝜑𝑥𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 𝐵 ) = ( 𝐶 𝑥 ) ) ) ∧ 𝑦𝑃 ) ∧ ( 𝑦 ∈ ( 𝐸 𝐼 𝐹 ) ∧ ( 𝐶 𝐷 ) = ( 𝐸 𝑦 ) ) ) → 𝑥𝑃 )
19 eqid ( cgrG ‘ 𝐺 ) = ( cgrG ‘ 𝐺 )
20 10 ad4antr ( ( ( ( ( 𝜑𝑥𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 𝐵 ) = ( 𝐶 𝑥 ) ) ) ∧ 𝑦𝑃 ) ∧ ( 𝑦 ∈ ( 𝐸 𝐼 𝐹 ) ∧ ( 𝐶 𝐷 ) = ( 𝐸 𝑦 ) ) ) → 𝐸𝑃 )
21 simplr ( ( ( ( ( 𝜑𝑥𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 𝐵 ) = ( 𝐶 𝑥 ) ) ) ∧ 𝑦𝑃 ) ∧ ( 𝑦 ∈ ( 𝐸 𝐼 𝐹 ) ∧ ( 𝐶 𝐷 ) = ( 𝐸 𝑦 ) ) ) → 𝑦𝑃 )
22 simpllr ( ( ( ( ( 𝜑𝑥𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 𝐵 ) = ( 𝐶 𝑥 ) ) ) ∧ 𝑦𝑃 ) ∧ ( 𝑦 ∈ ( 𝐸 𝐼 𝐹 ) ∧ ( 𝐶 𝐷 ) = ( 𝐸 𝑦 ) ) ) → ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 𝐵 ) = ( 𝐶 𝑥 ) ) )
23 22 simpld ( ( ( ( ( 𝜑𝑥𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 𝐵 ) = ( 𝐶 𝑥 ) ) ) ∧ 𝑦𝑃 ) ∧ ( 𝑦 ∈ ( 𝐸 𝐼 𝐹 ) ∧ ( 𝐶 𝐷 ) = ( 𝐸 𝑦 ) ) ) → 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) )
24 1 14 3 15 16 18 17 23 btwncolg3 ( ( ( ( ( 𝜑𝑥𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 𝐵 ) = ( 𝐶 𝑥 ) ) ) ∧ 𝑦𝑃 ) ∧ ( 𝑦 ∈ ( 𝐸 𝐼 𝐹 ) ∧ ( 𝐶 𝐷 ) = ( 𝐸 𝑦 ) ) ) → ( 𝐷 ∈ ( 𝐶 ( LineG ‘ 𝐺 ) 𝑥 ) ∨ 𝐶 = 𝑥 ) )
25 simprr ( ( ( ( ( 𝜑𝑥𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 𝐵 ) = ( 𝐶 𝑥 ) ) ) ∧ 𝑦𝑃 ) ∧ ( 𝑦 ∈ ( 𝐸 𝐼 𝐹 ) ∧ ( 𝐶 𝐷 ) = ( 𝐸 𝑦 ) ) ) → ( 𝐶 𝐷 ) = ( 𝐸 𝑦 ) )
26 1 14 3 15 16 17 18 19 20 21 2 24 25 lnext ( ( ( ( ( 𝜑𝑥𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 𝐵 ) = ( 𝐶 𝑥 ) ) ) ∧ 𝑦𝑃 ) ∧ ( 𝑦 ∈ ( 𝐸 𝐼 𝐹 ) ∧ ( 𝐶 𝐷 ) = ( 𝐸 𝑦 ) ) ) → ∃ 𝑧𝑃 ⟨“ 𝐶 𝐷 𝑥 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝑦 𝑧 ”⟩ )
27 15 ad2antrr ( ( ( ( ( ( ( 𝜑𝑥𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 𝐵 ) = ( 𝐶 𝑥 ) ) ) ∧ 𝑦𝑃 ) ∧ ( 𝑦 ∈ ( 𝐸 𝐼 𝐹 ) ∧ ( 𝐶 𝐷 ) = ( 𝐸 𝑦 ) ) ) ∧ 𝑧𝑃 ) ∧ ⟨“ 𝐶 𝐷 𝑥 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝑦 𝑧 ”⟩ ) → 𝐺 ∈ TarskiG )
28 20 ad2antrr ( ( ( ( ( ( ( 𝜑𝑥𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 𝐵 ) = ( 𝐶 𝑥 ) ) ) ∧ 𝑦𝑃 ) ∧ ( 𝑦 ∈ ( 𝐸 𝐼 𝐹 ) ∧ ( 𝐶 𝐷 ) = ( 𝐸 𝑦 ) ) ) ∧ 𝑧𝑃 ) ∧ ⟨“ 𝐶 𝐷 𝑥 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝑦 𝑧 ”⟩ ) → 𝐸𝑃 )
29 simplr ( ( ( ( ( ( ( 𝜑𝑥𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 𝐵 ) = ( 𝐶 𝑥 ) ) ) ∧ 𝑦𝑃 ) ∧ ( 𝑦 ∈ ( 𝐸 𝐼 𝐹 ) ∧ ( 𝐶 𝐷 ) = ( 𝐸 𝑦 ) ) ) ∧ 𝑧𝑃 ) ∧ ⟨“ 𝐶 𝐷 𝑥 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝑦 𝑧 ”⟩ ) → 𝑧𝑃 )
30 simp-4r ( ( ( ( ( ( ( 𝜑𝑥𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 𝐵 ) = ( 𝐶 𝑥 ) ) ) ∧ 𝑦𝑃 ) ∧ ( 𝑦 ∈ ( 𝐸 𝐼 𝐹 ) ∧ ( 𝐶 𝐷 ) = ( 𝐸 𝑦 ) ) ) ∧ 𝑧𝑃 ) ∧ ⟨“ 𝐶 𝐷 𝑥 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝑦 𝑧 ”⟩ ) → 𝑦𝑃 )
31 11 ad6antr ( ( ( ( ( ( ( 𝜑𝑥𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 𝐵 ) = ( 𝐶 𝑥 ) ) ) ∧ 𝑦𝑃 ) ∧ ( 𝑦 ∈ ( 𝐸 𝐼 𝐹 ) ∧ ( 𝐶 𝐷 ) = ( 𝐸 𝑦 ) ) ) ∧ 𝑧𝑃 ) ∧ ⟨“ 𝐶 𝐷 𝑥 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝑦 𝑧 ”⟩ ) → 𝐹𝑃 )
32 16 ad2antrr ( ( ( ( ( ( ( 𝜑𝑥𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 𝐵 ) = ( 𝐶 𝑥 ) ) ) ∧ 𝑦𝑃 ) ∧ ( 𝑦 ∈ ( 𝐸 𝐼 𝐹 ) ∧ ( 𝐶 𝐷 ) = ( 𝐸 𝑦 ) ) ) ∧ 𝑧𝑃 ) ∧ ⟨“ 𝐶 𝐷 𝑥 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝑦 𝑧 ”⟩ ) → 𝐶𝑃 )
33 18 ad2antrr ( ( ( ( ( ( ( 𝜑𝑥𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 𝐵 ) = ( 𝐶 𝑥 ) ) ) ∧ 𝑦𝑃 ) ∧ ( 𝑦 ∈ ( 𝐸 𝐼 𝐹 ) ∧ ( 𝐶 𝐷 ) = ( 𝐸 𝑦 ) ) ) ∧ 𝑧𝑃 ) ∧ ⟨“ 𝐶 𝐷 𝑥 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝑦 𝑧 ”⟩ ) → 𝑥𝑃 )
34 17 ad2antrr ( ( ( ( ( ( ( 𝜑𝑥𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 𝐵 ) = ( 𝐶 𝑥 ) ) ) ∧ 𝑦𝑃 ) ∧ ( 𝑦 ∈ ( 𝐸 𝐼 𝐹 ) ∧ ( 𝐶 𝐷 ) = ( 𝐸 𝑦 ) ) ) ∧ 𝑧𝑃 ) ∧ ⟨“ 𝐶 𝐷 𝑥 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝑦 𝑧 ”⟩ ) → 𝐷𝑃 )
35 simpr ( ( ( ( ( ( ( 𝜑𝑥𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 𝐵 ) = ( 𝐶 𝑥 ) ) ) ∧ 𝑦𝑃 ) ∧ ( 𝑦 ∈ ( 𝐸 𝐼 𝐹 ) ∧ ( 𝐶 𝐷 ) = ( 𝐸 𝑦 ) ) ) ∧ 𝑧𝑃 ) ∧ ⟨“ 𝐶 𝐷 𝑥 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝑦 𝑧 ”⟩ ) → ⟨“ 𝐶 𝐷 𝑥 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝑦 𝑧 ”⟩ )
36 1 2 3 19 27 32 34 33 28 30 29 35 cgr3swap23 ( ( ( ( ( ( ( 𝜑𝑥𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 𝐵 ) = ( 𝐶 𝑥 ) ) ) ∧ 𝑦𝑃 ) ∧ ( 𝑦 ∈ ( 𝐸 𝐼 𝐹 ) ∧ ( 𝐶 𝐷 ) = ( 𝐸 𝑦 ) ) ) ∧ 𝑧𝑃 ) ∧ ⟨“ 𝐶 𝐷 𝑥 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝑦 𝑧 ”⟩ ) → ⟨“ 𝐶 𝑥 𝐷 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝑧 𝑦 ”⟩ )
37 23 ad2antrr ( ( ( ( ( ( ( 𝜑𝑥𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 𝐵 ) = ( 𝐶 𝑥 ) ) ) ∧ 𝑦𝑃 ) ∧ ( 𝑦 ∈ ( 𝐸 𝐼 𝐹 ) ∧ ( 𝐶 𝐷 ) = ( 𝐸 𝑦 ) ) ) ∧ 𝑧𝑃 ) ∧ ⟨“ 𝐶 𝐷 𝑥 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝑦 𝑧 ”⟩ ) → 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) )
38 1 2 3 19 27 32 33 34 28 29 30 36 37 tgbtwnxfr ( ( ( ( ( ( ( 𝜑𝑥𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 𝐵 ) = ( 𝐶 𝑥 ) ) ) ∧ 𝑦𝑃 ) ∧ ( 𝑦 ∈ ( 𝐸 𝐼 𝐹 ) ∧ ( 𝐶 𝐷 ) = ( 𝐸 𝑦 ) ) ) ∧ 𝑧𝑃 ) ∧ ⟨“ 𝐶 𝐷 𝑥 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝑦 𝑧 ”⟩ ) → 𝑧 ∈ ( 𝐸 𝐼 𝑦 ) )
39 simpllr ( ( ( ( ( ( ( 𝜑𝑥𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 𝐵 ) = ( 𝐶 𝑥 ) ) ) ∧ 𝑦𝑃 ) ∧ ( 𝑦 ∈ ( 𝐸 𝐼 𝐹 ) ∧ ( 𝐶 𝐷 ) = ( 𝐸 𝑦 ) ) ) ∧ 𝑧𝑃 ) ∧ ⟨“ 𝐶 𝐷 𝑥 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝑦 𝑧 ”⟩ ) → ( 𝑦 ∈ ( 𝐸 𝐼 𝐹 ) ∧ ( 𝐶 𝐷 ) = ( 𝐸 𝑦 ) ) )
40 39 simpld ( ( ( ( ( ( ( 𝜑𝑥𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 𝐵 ) = ( 𝐶 𝑥 ) ) ) ∧ 𝑦𝑃 ) ∧ ( 𝑦 ∈ ( 𝐸 𝐼 𝐹 ) ∧ ( 𝐶 𝐷 ) = ( 𝐸 𝑦 ) ) ) ∧ 𝑧𝑃 ) ∧ ⟨“ 𝐶 𝐷 𝑥 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝑦 𝑧 ”⟩ ) → 𝑦 ∈ ( 𝐸 𝐼 𝐹 ) )
41 1 2 3 27 28 29 30 31 38 40 tgbtwnexch ( ( ( ( ( ( ( 𝜑𝑥𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 𝐵 ) = ( 𝐶 𝑥 ) ) ) ∧ 𝑦𝑃 ) ∧ ( 𝑦 ∈ ( 𝐸 𝐼 𝐹 ) ∧ ( 𝐶 𝐷 ) = ( 𝐸 𝑦 ) ) ) ∧ 𝑧𝑃 ) ∧ ⟨“ 𝐶 𝐷 𝑥 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝑦 𝑧 ”⟩ ) → 𝑧 ∈ ( 𝐸 𝐼 𝐹 ) )
42 simp-5r ( ( ( ( ( ( ( 𝜑𝑥𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 𝐵 ) = ( 𝐶 𝑥 ) ) ) ∧ 𝑦𝑃 ) ∧ ( 𝑦 ∈ ( 𝐸 𝐼 𝐹 ) ∧ ( 𝐶 𝐷 ) = ( 𝐸 𝑦 ) ) ) ∧ 𝑧𝑃 ) ∧ ⟨“ 𝐶 𝐷 𝑥 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝑦 𝑧 ”⟩ ) → ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 𝐵 ) = ( 𝐶 𝑥 ) ) )
43 42 simprd ( ( ( ( ( ( ( 𝜑𝑥𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 𝐵 ) = ( 𝐶 𝑥 ) ) ) ∧ 𝑦𝑃 ) ∧ ( 𝑦 ∈ ( 𝐸 𝐼 𝐹 ) ∧ ( 𝐶 𝐷 ) = ( 𝐸 𝑦 ) ) ) ∧ 𝑧𝑃 ) ∧ ⟨“ 𝐶 𝐷 𝑥 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝑦 𝑧 ”⟩ ) → ( 𝐴 𝐵 ) = ( 𝐶 𝑥 ) )
44 1 2 3 19 27 32 33 34 28 29 30 36 cgr3simp1 ( ( ( ( ( ( ( 𝜑𝑥𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 𝐵 ) = ( 𝐶 𝑥 ) ) ) ∧ 𝑦𝑃 ) ∧ ( 𝑦 ∈ ( 𝐸 𝐼 𝐹 ) ∧ ( 𝐶 𝐷 ) = ( 𝐸 𝑦 ) ) ) ∧ 𝑧𝑃 ) ∧ ⟨“ 𝐶 𝐷 𝑥 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝑦 𝑧 ”⟩ ) → ( 𝐶 𝑥 ) = ( 𝐸 𝑧 ) )
45 43 44 eqtrd ( ( ( ( ( ( ( 𝜑𝑥𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 𝐵 ) = ( 𝐶 𝑥 ) ) ) ∧ 𝑦𝑃 ) ∧ ( 𝑦 ∈ ( 𝐸 𝐼 𝐹 ) ∧ ( 𝐶 𝐷 ) = ( 𝐸 𝑦 ) ) ) ∧ 𝑧𝑃 ) ∧ ⟨“ 𝐶 𝐷 𝑥 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝑦 𝑧 ”⟩ ) → ( 𝐴 𝐵 ) = ( 𝐸 𝑧 ) )
46 41 45 jca ( ( ( ( ( ( ( 𝜑𝑥𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 𝐵 ) = ( 𝐶 𝑥 ) ) ) ∧ 𝑦𝑃 ) ∧ ( 𝑦 ∈ ( 𝐸 𝐼 𝐹 ) ∧ ( 𝐶 𝐷 ) = ( 𝐸 𝑦 ) ) ) ∧ 𝑧𝑃 ) ∧ ⟨“ 𝐶 𝐷 𝑥 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝑦 𝑧 ”⟩ ) → ( 𝑧 ∈ ( 𝐸 𝐼 𝐹 ) ∧ ( 𝐴 𝐵 ) = ( 𝐸 𝑧 ) ) )
47 46 ex ( ( ( ( ( ( 𝜑𝑥𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 𝐵 ) = ( 𝐶 𝑥 ) ) ) ∧ 𝑦𝑃 ) ∧ ( 𝑦 ∈ ( 𝐸 𝐼 𝐹 ) ∧ ( 𝐶 𝐷 ) = ( 𝐸 𝑦 ) ) ) ∧ 𝑧𝑃 ) → ( ⟨“ 𝐶 𝐷 𝑥 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝑦 𝑧 ”⟩ → ( 𝑧 ∈ ( 𝐸 𝐼 𝐹 ) ∧ ( 𝐴 𝐵 ) = ( 𝐸 𝑧 ) ) ) )
48 47 reximdva ( ( ( ( ( 𝜑𝑥𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 𝐵 ) = ( 𝐶 𝑥 ) ) ) ∧ 𝑦𝑃 ) ∧ ( 𝑦 ∈ ( 𝐸 𝐼 𝐹 ) ∧ ( 𝐶 𝐷 ) = ( 𝐸 𝑦 ) ) ) → ( ∃ 𝑧𝑃 ⟨“ 𝐶 𝐷 𝑥 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝑦 𝑧 ”⟩ → ∃ 𝑧𝑃 ( 𝑧 ∈ ( 𝐸 𝐼 𝐹 ) ∧ ( 𝐴 𝐵 ) = ( 𝐸 𝑧 ) ) ) )
49 26 48 mpd ( ( ( ( ( 𝜑𝑥𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 𝐵 ) = ( 𝐶 𝑥 ) ) ) ∧ 𝑦𝑃 ) ∧ ( 𝑦 ∈ ( 𝐸 𝐼 𝐹 ) ∧ ( 𝐶 𝐷 ) = ( 𝐸 𝑦 ) ) ) → ∃ 𝑧𝑃 ( 𝑧 ∈ ( 𝐸 𝐼 𝐹 ) ∧ ( 𝐴 𝐵 ) = ( 𝐸 𝑧 ) ) )
50 1 2 3 4 5 8 9 10 11 legov ( 𝜑 → ( ( 𝐶 𝐷 ) ( 𝐸 𝐹 ) ↔ ∃ 𝑦𝑃 ( 𝑦 ∈ ( 𝐸 𝐼 𝐹 ) ∧ ( 𝐶 𝐷 ) = ( 𝐸 𝑦 ) ) ) )
51 13 50 mpbid ( 𝜑 → ∃ 𝑦𝑃 ( 𝑦 ∈ ( 𝐸 𝐼 𝐹 ) ∧ ( 𝐶 𝐷 ) = ( 𝐸 𝑦 ) ) )
52 51 ad2antrr ( ( ( 𝜑𝑥𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 𝐵 ) = ( 𝐶 𝑥 ) ) ) → ∃ 𝑦𝑃 ( 𝑦 ∈ ( 𝐸 𝐼 𝐹 ) ∧ ( 𝐶 𝐷 ) = ( 𝐸 𝑦 ) ) )
53 49 52 r19.29a ( ( ( 𝜑𝑥𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 𝐵 ) = ( 𝐶 𝑥 ) ) ) → ∃ 𝑧𝑃 ( 𝑧 ∈ ( 𝐸 𝐼 𝐹 ) ∧ ( 𝐴 𝐵 ) = ( 𝐸 𝑧 ) ) )
54 1 2 3 4 5 6 7 8 9 legov ( 𝜑 → ( ( 𝐴 𝐵 ) ( 𝐶 𝐷 ) ↔ ∃ 𝑥𝑃 ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 𝐵 ) = ( 𝐶 𝑥 ) ) ) )
55 12 54 mpbid ( 𝜑 → ∃ 𝑥𝑃 ( 𝑥 ∈ ( 𝐶 𝐼 𝐷 ) ∧ ( 𝐴 𝐵 ) = ( 𝐶 𝑥 ) ) )
56 53 55 r19.29a ( 𝜑 → ∃ 𝑧𝑃 ( 𝑧 ∈ ( 𝐸 𝐼 𝐹 ) ∧ ( 𝐴 𝐵 ) = ( 𝐸 𝑧 ) ) )
57 1 2 3 4 5 6 7 10 11 legov ( 𝜑 → ( ( 𝐴 𝐵 ) ( 𝐸 𝐹 ) ↔ ∃ 𝑧𝑃 ( 𝑧 ∈ ( 𝐸 𝐼 𝐹 ) ∧ ( 𝐴 𝐵 ) = ( 𝐸 𝑧 ) ) ) )
58 56 57 mpbird ( 𝜑 → ( 𝐴 𝐵 ) ( 𝐸 𝐹 ) )