Metamath Proof Explorer

Theorem axtgeucl

Description: Euclid's Axiom. Axiom A10 of Schwabhauser p. 13. This is equivalent to Euclid's parallel postulate when combined with other axioms. (Contributed by Thierry Arnoux, 16-Mar-2019)

Ref Expression
Hypotheses axtrkge.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
axtrkge.d ⊢ − = ( dist ‘ 𝐺 )
axtrkge.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
axtgeucl.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiGE )
axtgeucl.1 ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
axtgeucl.2 ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
axtgeucl.3 ⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
axtgeucl.4 ⊢ ( 𝜑 → 𝑈 ∈ 𝑃 )
axtgeucl.5 ⊢ ( 𝜑 → 𝑉 ∈ 𝑃 )
axtgeucl.6 ⊢ ( 𝜑 → 𝑈 ∈ ( 𝑋 𝐼 𝑉 ) )
axtgeucl.7 ⊢ ( 𝜑 → 𝑈 ∈ ( 𝑌 𝐼 𝑍 ) )
axtgeucl.8 ⊢ ( 𝜑 → 𝑋 ≠ 𝑈 )
Assertion axtgeucl ( 𝜑 → ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ( 𝑌 ∈ ( 𝑋 𝐼 𝑎 ) ∧ 𝑍 ∈ ( 𝑋 𝐼 𝑏 ) ∧ 𝑉 ∈ ( 𝑎 𝐼 𝑏 ) ) )

Proof

Step Hyp Ref Expression
1 axtrkge.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 axtrkge.d ⊢ − = ( dist ‘ 𝐺 )
3 axtrkge.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
4 axtgeucl.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiGE )
5 axtgeucl.1 ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
6 axtgeucl.2 ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
7 axtgeucl.3 ⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
8 axtgeucl.4 ⊢ ( 𝜑 → 𝑈 ∈ 𝑃 )
9 axtgeucl.5 ⊢ ( 𝜑 → 𝑉 ∈ 𝑃 )
10 axtgeucl.6 ⊢ ( 𝜑 → 𝑈 ∈ ( 𝑋 𝐼 𝑉 ) )
11 axtgeucl.7 ⊢ ( 𝜑 → 𝑈 ∈ ( 𝑌 𝐼 𝑍 ) )
12 axtgeucl.8 ⊢ ( 𝜑 → 𝑋 ≠ 𝑈 )
13 1 2 3 istrkge ⊢ ( 𝐺 ∈ TarskiGE ↔ ( 𝐺 ∈ V ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ∀ 𝑧 ∈ 𝑃 ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( 𝑢 ∈ ( 𝑥 𝐼 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝐼 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) → ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ( 𝑦 ∈ ( 𝑥 𝐼 𝑎 ) ∧ 𝑧 ∈ ( 𝑥 𝐼 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝐼 𝑏 ) ) ) ) )
14 4 13 sylib ⊢ ( 𝜑 → ( 𝐺 ∈ V ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ∀ 𝑧 ∈ 𝑃 ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( 𝑢 ∈ ( 𝑥 𝐼 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝐼 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) → ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ( 𝑦 ∈ ( 𝑥 𝐼 𝑎 ) ∧ 𝑧 ∈ ( 𝑥 𝐼 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝐼 𝑏 ) ) ) ) )
15 14 simprd ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ∀ 𝑧 ∈ 𝑃 ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( 𝑢 ∈ ( 𝑥 𝐼 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝐼 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) → ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ( 𝑦 ∈ ( 𝑥 𝐼 𝑎 ) ∧ 𝑧 ∈ ( 𝑥 𝐼 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝐼 𝑏 ) ) ) )
16 oveq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 𝐼 𝑣 ) = ( 𝑋 𝐼 𝑣 ) )
17 16 eleq2d ⊢ ( 𝑥 = 𝑋 → ( 𝑢 ∈ ( 𝑥 𝐼 𝑣 ) ↔ 𝑢 ∈ ( 𝑋 𝐼 𝑣 ) ) )
18 neeq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 ≠ 𝑢 ↔ 𝑋 ≠ 𝑢 ) )
19 17 18 3anbi13d ⊢ ( 𝑥 = 𝑋 → ( ( 𝑢 ∈ ( 𝑥 𝐼 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝐼 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) ↔ ( 𝑢 ∈ ( 𝑋 𝐼 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝐼 𝑧 ) ∧ 𝑋 ≠ 𝑢 ) ) )
20 oveq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 𝐼 𝑎 ) = ( 𝑋 𝐼 𝑎 ) )
21 20 eleq2d ⊢ ( 𝑥 = 𝑋 → ( 𝑦 ∈ ( 𝑥 𝐼 𝑎 ) ↔ 𝑦 ∈ ( 𝑋 𝐼 𝑎 ) ) )
22 oveq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 𝐼 𝑏 ) = ( 𝑋 𝐼 𝑏 ) )
23 22 eleq2d ⊢ ( 𝑥 = 𝑋 → ( 𝑧 ∈ ( 𝑥 𝐼 𝑏 ) ↔ 𝑧 ∈ ( 𝑋 𝐼 𝑏 ) ) )
24 21 23 3anbi12d ⊢ ( 𝑥 = 𝑋 → ( ( 𝑦 ∈ ( 𝑥 𝐼 𝑎 ) ∧ 𝑧 ∈ ( 𝑥 𝐼 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝐼 𝑏 ) ) ↔ ( 𝑦 ∈ ( 𝑋 𝐼 𝑎 ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝐼 𝑏 ) ) ) )
25 24 2rexbidv ⊢ ( 𝑥 = 𝑋 → ( ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ( 𝑦 ∈ ( 𝑥 𝐼 𝑎 ) ∧ 𝑧 ∈ ( 𝑥 𝐼 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝐼 𝑏 ) ) ↔ ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ( 𝑦 ∈ ( 𝑋 𝐼 𝑎 ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝐼 𝑏 ) ) ) )
26 19 25 imbi12d ⊢ ( 𝑥 = 𝑋 → ( ( ( 𝑢 ∈ ( 𝑥 𝐼 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝐼 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) → ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ( 𝑦 ∈ ( 𝑥 𝐼 𝑎 ) ∧ 𝑧 ∈ ( 𝑥 𝐼 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝐼 𝑏 ) ) ) ↔ ( ( 𝑢 ∈ ( 𝑋 𝐼 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝐼 𝑧 ) ∧ 𝑋 ≠ 𝑢 ) → ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ( 𝑦 ∈ ( 𝑋 𝐼 𝑎 ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝐼 𝑏 ) ) ) ) )
27 26 2ralbidv ⊢ ( 𝑥 = 𝑋 → ( ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( 𝑢 ∈ ( 𝑥 𝐼 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝐼 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) → ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ( 𝑦 ∈ ( 𝑥 𝐼 𝑎 ) ∧ 𝑧 ∈ ( 𝑥 𝐼 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝐼 𝑏 ) ) ) ↔ ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( 𝑢 ∈ ( 𝑋 𝐼 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝐼 𝑧 ) ∧ 𝑋 ≠ 𝑢 ) → ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ( 𝑦 ∈ ( 𝑋 𝐼 𝑎 ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝐼 𝑏 ) ) ) ) )
28 oveq1 ⊢ ( 𝑦 = 𝑌 → ( 𝑦 𝐼 𝑧 ) = ( 𝑌 𝐼 𝑧 ) )
29 28 eleq2d ⊢ ( 𝑦 = 𝑌 → ( 𝑢 ∈ ( 𝑦 𝐼 𝑧 ) ↔ 𝑢 ∈ ( 𝑌 𝐼 𝑧 ) ) )
30 29 3anbi2d ⊢ ( 𝑦 = 𝑌 → ( ( 𝑢 ∈ ( 𝑋 𝐼 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝐼 𝑧 ) ∧ 𝑋 ≠ 𝑢 ) ↔ ( 𝑢 ∈ ( 𝑋 𝐼 𝑣 ) ∧ 𝑢 ∈ ( 𝑌 𝐼 𝑧 ) ∧ 𝑋 ≠ 𝑢 ) ) )
31 eleq1 ⊢ ( 𝑦 = 𝑌 → ( 𝑦 ∈ ( 𝑋 𝐼 𝑎 ) ↔ 𝑌 ∈ ( 𝑋 𝐼 𝑎 ) ) )
32 31 3anbi1d ⊢ ( 𝑦 = 𝑌 → ( ( 𝑦 ∈ ( 𝑋 𝐼 𝑎 ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝐼 𝑏 ) ) ↔ ( 𝑌 ∈ ( 𝑋 𝐼 𝑎 ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝐼 𝑏 ) ) ) )
33 32 2rexbidv ⊢ ( 𝑦 = 𝑌 → ( ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ( 𝑦 ∈ ( 𝑋 𝐼 𝑎 ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝐼 𝑏 ) ) ↔ ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ( 𝑌 ∈ ( 𝑋 𝐼 𝑎 ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝐼 𝑏 ) ) ) )
34 30 33 imbi12d ⊢ ( 𝑦 = 𝑌 → ( ( ( 𝑢 ∈ ( 𝑋 𝐼 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝐼 𝑧 ) ∧ 𝑋 ≠ 𝑢 ) → ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ( 𝑦 ∈ ( 𝑋 𝐼 𝑎 ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝐼 𝑏 ) ) ) ↔ ( ( 𝑢 ∈ ( 𝑋 𝐼 𝑣 ) ∧ 𝑢 ∈ ( 𝑌 𝐼 𝑧 ) ∧ 𝑋 ≠ 𝑢 ) → ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ( 𝑌 ∈ ( 𝑋 𝐼 𝑎 ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝐼 𝑏 ) ) ) ) )
35 34 2ralbidv ⊢ ( 𝑦 = 𝑌 → ( ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( 𝑢 ∈ ( 𝑋 𝐼 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝐼 𝑧 ) ∧ 𝑋 ≠ 𝑢 ) → ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ( 𝑦 ∈ ( 𝑋 𝐼 𝑎 ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝐼 𝑏 ) ) ) ↔ ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( 𝑢 ∈ ( 𝑋 𝐼 𝑣 ) ∧ 𝑢 ∈ ( 𝑌 𝐼 𝑧 ) ∧ 𝑋 ≠ 𝑢 ) → ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ( 𝑌 ∈ ( 𝑋 𝐼 𝑎 ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝐼 𝑏 ) ) ) ) )
36 oveq2 ⊢ ( 𝑧 = 𝑍 → ( 𝑌 𝐼 𝑧 ) = ( 𝑌 𝐼 𝑍 ) )
37 36 eleq2d ⊢ ( 𝑧 = 𝑍 → ( 𝑢 ∈ ( 𝑌 𝐼 𝑧 ) ↔ 𝑢 ∈ ( 𝑌 𝐼 𝑍 ) ) )
38 37 3anbi2d ⊢ ( 𝑧 = 𝑍 → ( ( 𝑢 ∈ ( 𝑋 𝐼 𝑣 ) ∧ 𝑢 ∈ ( 𝑌 𝐼 𝑧 ) ∧ 𝑋 ≠ 𝑢 ) ↔ ( 𝑢 ∈ ( 𝑋 𝐼 𝑣 ) ∧ 𝑢 ∈ ( 𝑌 𝐼 𝑍 ) ∧ 𝑋 ≠ 𝑢 ) ) )
39 eleq1 ⊢ ( 𝑧 = 𝑍 → ( 𝑧 ∈ ( 𝑋 𝐼 𝑏 ) ↔ 𝑍 ∈ ( 𝑋 𝐼 𝑏 ) ) )
40 39 3anbi2d ⊢ ( 𝑧 = 𝑍 → ( ( 𝑌 ∈ ( 𝑋 𝐼 𝑎 ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝐼 𝑏 ) ) ↔ ( 𝑌 ∈ ( 𝑋 𝐼 𝑎 ) ∧ 𝑍 ∈ ( 𝑋 𝐼 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝐼 𝑏 ) ) ) )
41 40 2rexbidv ⊢ ( 𝑧 = 𝑍 → ( ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ( 𝑌 ∈ ( 𝑋 𝐼 𝑎 ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝐼 𝑏 ) ) ↔ ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ( 𝑌 ∈ ( 𝑋 𝐼 𝑎 ) ∧ 𝑍 ∈ ( 𝑋 𝐼 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝐼 𝑏 ) ) ) )
42 38 41 imbi12d ⊢ ( 𝑧 = 𝑍 → ( ( ( 𝑢 ∈ ( 𝑋 𝐼 𝑣 ) ∧ 𝑢 ∈ ( 𝑌 𝐼 𝑧 ) ∧ 𝑋 ≠ 𝑢 ) → ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ( 𝑌 ∈ ( 𝑋 𝐼 𝑎 ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝐼 𝑏 ) ) ) ↔ ( ( 𝑢 ∈ ( 𝑋 𝐼 𝑣 ) ∧ 𝑢 ∈ ( 𝑌 𝐼 𝑍 ) ∧ 𝑋 ≠ 𝑢 ) → ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ( 𝑌 ∈ ( 𝑋 𝐼 𝑎 ) ∧ 𝑍 ∈ ( 𝑋 𝐼 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝐼 𝑏 ) ) ) ) )
43 42 2ralbidv ⊢ ( 𝑧 = 𝑍 → ( ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( 𝑢 ∈ ( 𝑋 𝐼 𝑣 ) ∧ 𝑢 ∈ ( 𝑌 𝐼 𝑧 ) ∧ 𝑋 ≠ 𝑢 ) → ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ( 𝑌 ∈ ( 𝑋 𝐼 𝑎 ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝐼 𝑏 ) ) ) ↔ ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( 𝑢 ∈ ( 𝑋 𝐼 𝑣 ) ∧ 𝑢 ∈ ( 𝑌 𝐼 𝑍 ) ∧ 𝑋 ≠ 𝑢 ) → ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ( 𝑌 ∈ ( 𝑋 𝐼 𝑎 ) ∧ 𝑍 ∈ ( 𝑋 𝐼 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝐼 𝑏 ) ) ) ) )
44 27 35 43 rspc3v ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃 ) → ( ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ∀ 𝑧 ∈ 𝑃 ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( 𝑢 ∈ ( 𝑥 𝐼 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝐼 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) → ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ( 𝑦 ∈ ( 𝑥 𝐼 𝑎 ) ∧ 𝑧 ∈ ( 𝑥 𝐼 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝐼 𝑏 ) ) ) → ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( 𝑢 ∈ ( 𝑋 𝐼 𝑣 ) ∧ 𝑢 ∈ ( 𝑌 𝐼 𝑍 ) ∧ 𝑋 ≠ 𝑢 ) → ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ( 𝑌 ∈ ( 𝑋 𝐼 𝑎 ) ∧ 𝑍 ∈ ( 𝑋 𝐼 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝐼 𝑏 ) ) ) ) )
45 5 6 7 44 syl3anc ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ∀ 𝑧 ∈ 𝑃 ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( 𝑢 ∈ ( 𝑥 𝐼 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝐼 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) → ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ( 𝑦 ∈ ( 𝑥 𝐼 𝑎 ) ∧ 𝑧 ∈ ( 𝑥 𝐼 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝐼 𝑏 ) ) ) → ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( 𝑢 ∈ ( 𝑋 𝐼 𝑣 ) ∧ 𝑢 ∈ ( 𝑌 𝐼 𝑍 ) ∧ 𝑋 ≠ 𝑢 ) → ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ( 𝑌 ∈ ( 𝑋 𝐼 𝑎 ) ∧ 𝑍 ∈ ( 𝑋 𝐼 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝐼 𝑏 ) ) ) ) )
46 15 45 mpd ⊢ ( 𝜑 → ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( 𝑢 ∈ ( 𝑋 𝐼 𝑣 ) ∧ 𝑢 ∈ ( 𝑌 𝐼 𝑍 ) ∧ 𝑋 ≠ 𝑢 ) → ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ( 𝑌 ∈ ( 𝑋 𝐼 𝑎 ) ∧ 𝑍 ∈ ( 𝑋 𝐼 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝐼 𝑏 ) ) ) )
47 eleq1 ⊢ ( 𝑢 = 𝑈 → ( 𝑢 ∈ ( 𝑋 𝐼 𝑣 ) ↔ 𝑈 ∈ ( 𝑋 𝐼 𝑣 ) ) )
48 eleq1 ⊢ ( 𝑢 = 𝑈 → ( 𝑢 ∈ ( 𝑌 𝐼 𝑍 ) ↔ 𝑈 ∈ ( 𝑌 𝐼 𝑍 ) ) )
49 neeq2 ⊢ ( 𝑢 = 𝑈 → ( 𝑋 ≠ 𝑢 ↔ 𝑋 ≠ 𝑈 ) )
50 47 48 49 3anbi123d ⊢ ( 𝑢 = 𝑈 → ( ( 𝑢 ∈ ( 𝑋 𝐼 𝑣 ) ∧ 𝑢 ∈ ( 𝑌 𝐼 𝑍 ) ∧ 𝑋 ≠ 𝑢 ) ↔ ( 𝑈 ∈ ( 𝑋 𝐼 𝑣 ) ∧ 𝑈 ∈ ( 𝑌 𝐼 𝑍 ) ∧ 𝑋 ≠ 𝑈 ) ) )
51 50 imbi1d ⊢ ( 𝑢 = 𝑈 → ( ( ( 𝑢 ∈ ( 𝑋 𝐼 𝑣 ) ∧ 𝑢 ∈ ( 𝑌 𝐼 𝑍 ) ∧ 𝑋 ≠ 𝑢 ) → ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ( 𝑌 ∈ ( 𝑋 𝐼 𝑎 ) ∧ 𝑍 ∈ ( 𝑋 𝐼 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝐼 𝑏 ) ) ) ↔ ( ( 𝑈 ∈ ( 𝑋 𝐼 𝑣 ) ∧ 𝑈 ∈ ( 𝑌 𝐼 𝑍 ) ∧ 𝑋 ≠ 𝑈 ) → ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ( 𝑌 ∈ ( 𝑋 𝐼 𝑎 ) ∧ 𝑍 ∈ ( 𝑋 𝐼 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝐼 𝑏 ) ) ) ) )
52 oveq2 ⊢ ( 𝑣 = 𝑉 → ( 𝑋 𝐼 𝑣 ) = ( 𝑋 𝐼 𝑉 ) )
53 52 eleq2d ⊢ ( 𝑣 = 𝑉 → ( 𝑈 ∈ ( 𝑋 𝐼 𝑣 ) ↔ 𝑈 ∈ ( 𝑋 𝐼 𝑉 ) ) )
54 53 3anbi1d ⊢ ( 𝑣 = 𝑉 → ( ( 𝑈 ∈ ( 𝑋 𝐼 𝑣 ) ∧ 𝑈 ∈ ( 𝑌 𝐼 𝑍 ) ∧ 𝑋 ≠ 𝑈 ) ↔ ( 𝑈 ∈ ( 𝑋 𝐼 𝑉 ) ∧ 𝑈 ∈ ( 𝑌 𝐼 𝑍 ) ∧ 𝑋 ≠ 𝑈 ) ) )
55 eleq1 ⊢ ( 𝑣 = 𝑉 → ( 𝑣 ∈ ( 𝑎 𝐼 𝑏 ) ↔ 𝑉 ∈ ( 𝑎 𝐼 𝑏 ) ) )
56 55 3anbi3d ⊢ ( 𝑣 = 𝑉 → ( ( 𝑌 ∈ ( 𝑋 𝐼 𝑎 ) ∧ 𝑍 ∈ ( 𝑋 𝐼 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝐼 𝑏 ) ) ↔ ( 𝑌 ∈ ( 𝑋 𝐼 𝑎 ) ∧ 𝑍 ∈ ( 𝑋 𝐼 𝑏 ) ∧ 𝑉 ∈ ( 𝑎 𝐼 𝑏 ) ) ) )
57 56 2rexbidv ⊢ ( 𝑣 = 𝑉 → ( ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ( 𝑌 ∈ ( 𝑋 𝐼 𝑎 ) ∧ 𝑍 ∈ ( 𝑋 𝐼 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝐼 𝑏 ) ) ↔ ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ( 𝑌 ∈ ( 𝑋 𝐼 𝑎 ) ∧ 𝑍 ∈ ( 𝑋 𝐼 𝑏 ) ∧ 𝑉 ∈ ( 𝑎 𝐼 𝑏 ) ) ) )
58 54 57 imbi12d ⊢ ( 𝑣 = 𝑉 → ( ( ( 𝑈 ∈ ( 𝑋 𝐼 𝑣 ) ∧ 𝑈 ∈ ( 𝑌 𝐼 𝑍 ) ∧ 𝑋 ≠ 𝑈 ) → ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ( 𝑌 ∈ ( 𝑋 𝐼 𝑎 ) ∧ 𝑍 ∈ ( 𝑋 𝐼 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝐼 𝑏 ) ) ) ↔ ( ( 𝑈 ∈ ( 𝑋 𝐼 𝑉 ) ∧ 𝑈 ∈ ( 𝑌 𝐼 𝑍 ) ∧ 𝑋 ≠ 𝑈 ) → ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ( 𝑌 ∈ ( 𝑋 𝐼 𝑎 ) ∧ 𝑍 ∈ ( 𝑋 𝐼 𝑏 ) ∧ 𝑉 ∈ ( 𝑎 𝐼 𝑏 ) ) ) ) )
59 51 58 rspc2v ⊢ ( ( 𝑈 ∈ 𝑃 ∧ 𝑉 ∈ 𝑃 ) → ( ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( 𝑢 ∈ ( 𝑋 𝐼 𝑣 ) ∧ 𝑢 ∈ ( 𝑌 𝐼 𝑍 ) ∧ 𝑋 ≠ 𝑢 ) → ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ( 𝑌 ∈ ( 𝑋 𝐼 𝑎 ) ∧ 𝑍 ∈ ( 𝑋 𝐼 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝐼 𝑏 ) ) ) → ( ( 𝑈 ∈ ( 𝑋 𝐼 𝑉 ) ∧ 𝑈 ∈ ( 𝑌 𝐼 𝑍 ) ∧ 𝑋 ≠ 𝑈 ) → ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ( 𝑌 ∈ ( 𝑋 𝐼 𝑎 ) ∧ 𝑍 ∈ ( 𝑋 𝐼 𝑏 ) ∧ 𝑉 ∈ ( 𝑎 𝐼 𝑏 ) ) ) ) )
60 8 9 59 syl2anc ⊢ ( 𝜑 → ( ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( 𝑢 ∈ ( 𝑋 𝐼 𝑣 ) ∧ 𝑢 ∈ ( 𝑌 𝐼 𝑍 ) ∧ 𝑋 ≠ 𝑢 ) → ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ( 𝑌 ∈ ( 𝑋 𝐼 𝑎 ) ∧ 𝑍 ∈ ( 𝑋 𝐼 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝐼 𝑏 ) ) ) → ( ( 𝑈 ∈ ( 𝑋 𝐼 𝑉 ) ∧ 𝑈 ∈ ( 𝑌 𝐼 𝑍 ) ∧ 𝑋 ≠ 𝑈 ) → ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ( 𝑌 ∈ ( 𝑋 𝐼 𝑎 ) ∧ 𝑍 ∈ ( 𝑋 𝐼 𝑏 ) ∧ 𝑉 ∈ ( 𝑎 𝐼 𝑏 ) ) ) ) )
61 46 60 mpd ⊢ ( 𝜑 → ( ( 𝑈 ∈ ( 𝑋 𝐼 𝑉 ) ∧ 𝑈 ∈ ( 𝑌 𝐼 𝑍 ) ∧ 𝑋 ≠ 𝑈 ) → ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ( 𝑌 ∈ ( 𝑋 𝐼 𝑎 ) ∧ 𝑍 ∈ ( 𝑋 𝐼 𝑏 ) ∧ 𝑉 ∈ ( 𝑎 𝐼 𝑏 ) ) ) )
62 10 11 12 61 mp3and ⊢ ( 𝜑 → ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ( 𝑌 ∈ ( 𝑋 𝐼 𝑎 ) ∧ 𝑍 ∈ ( 𝑋 𝐼 𝑏 ) ∧ 𝑉 ∈ ( 𝑎 𝐼 𝑏 ) ) )