Metamath Proof Explorer

Theorem axtgpasch

Description: Axiom of (Inner) Pasch, Axiom A7 of Schwabhauser p. 12. Given triangle X Y Z , point U in segment X Z , and point V in segment Y Z , there exists a point a on both the segment U Y and the segment V X . This axiom is essentially a subset of the general Pasch axiom. The general Pasch axiom asserts that on a plane "a line intersecting a triangle in one of its sides, and not intersecting any of the vertices, must intersect one of the other two sides" (per the discussion about Axiom 7 of Tarski1999 p. 179). The (general) Pasch axiom was used implicitly by Euclid, but never stated; Moritz Pasch discovered its omission in 1882. As noted in the Metamath book, this means that the omission of Pasch's axiom from Euclid went unnoticed for 2000 years. Only the inner Pasch algorithm is included as an axiom; the "outer" form of the Pasch axiom can be proved using the inner form (see theorem 9.6 of Schwabhauser p. 69 and the brief discussion in axiom 7.1 of Tarski1999 p. 180). (Contributed by Thierry Arnoux, 15-Mar-2019)

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

Proof

Step Hyp Ref Expression
1 axtrkg.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 axtrkg.d ⊢ − = ( dist ‘ 𝐺 )
3 axtrkg.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
4 axtrkg.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5 axtgpasch.1 ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
6 axtgpasch.2 ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
7 axtgpasch.3 ⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
8 axtgpasch.4 ⊢ ( 𝜑 → 𝑈 ∈ 𝑃 )
9 axtgpasch.5 ⊢ ( 𝜑 → 𝑉 ∈ 𝑃 )
10 axtgpasch.6 ⊢ ( 𝜑 → 𝑈 ∈ ( 𝑋 𝐼 𝑍 ) )
11 axtgpasch.7 ⊢ ( 𝜑 → 𝑉 ∈ ( 𝑌 𝐼 𝑍 ) )
12 df-trkg ⊢ TarskiG = ( ( TarskiGC ∩ TarskiGB ) ∩ ( TarskiGCB ∩ { 𝑓 ∣ [ ( Base ‘ 𝑓 ) / 𝑝 ] [ ( Itv ‘ 𝑓 ) / 𝑖 ] ( LineG ‘ 𝑓 ) = ( 𝑥 ∈ 𝑝 , 𝑦 ∈ ( 𝑝 ∖ { 𝑥 } ) ↦ { 𝑧 ∈ 𝑝 ∣ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) } ) } ) )
13 inss1 ⊢ ( ( TarskiGC ∩ TarskiGB ) ∩ ( TarskiGCB ∩ { 𝑓 ∣ [ ( Base ‘ 𝑓 ) / 𝑝 ] [ ( Itv ‘ 𝑓 ) / 𝑖 ] ( LineG ‘ 𝑓 ) = ( 𝑥 ∈ 𝑝 , 𝑦 ∈ ( 𝑝 ∖ { 𝑥 } ) ↦ { 𝑧 ∈ 𝑝 ∣ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) } ) } ) ) ⊆ ( TarskiGC ∩ TarskiGB )
14 inss2 ⊢ ( TarskiGC ∩ TarskiGB ) ⊆ TarskiGB
15 13 14 sstri ⊢ ( ( TarskiGC ∩ TarskiGB ) ∩ ( TarskiGCB ∩ { 𝑓 ∣ [ ( Base ‘ 𝑓 ) / 𝑝 ] [ ( Itv ‘ 𝑓 ) / 𝑖 ] ( LineG ‘ 𝑓 ) = ( 𝑥 ∈ 𝑝 , 𝑦 ∈ ( 𝑝 ∖ { 𝑥 } ) ↦ { 𝑧 ∈ 𝑝 ∣ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) } ) } ) ) ⊆ TarskiGB
16 12 15 eqsstri ⊢ TarskiG ⊆ TarskiGB
17 16 4 sselid ⊢ ( 𝜑 → 𝐺 ∈ TarskiGB )
18 1 2 3 istrkgb ⊢ ( 𝐺 ∈ TarskiGB ↔ ( 𝐺 ∈ V ∧ ( ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ( 𝑦 ∈ ( 𝑥 𝐼 𝑥 ) → 𝑥 = 𝑦 ) ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ∀ 𝑧 ∈ 𝑃 ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( 𝑢 ∈ ( 𝑥 𝐼 𝑧 ) ∧ 𝑣 ∈ ( 𝑦 𝐼 𝑧 ) ) → ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑢 𝐼 𝑦 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑥 ) ) ) ∧ ∀ 𝑠 ∈ 𝒫 𝑃 ∀ 𝑡 ∈ 𝒫 𝑃 ( ∃ 𝑎 ∈ 𝑃 ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑡 𝑥 ∈ ( 𝑎 𝐼 𝑦 ) → ∃ 𝑏 ∈ 𝑃 ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑡 𝑏 ∈ ( 𝑥 𝐼 𝑦 ) ) ) ) )
19 18 simprbi ⊢ ( 𝐺 ∈ TarskiGB → ( ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ( 𝑦 ∈ ( 𝑥 𝐼 𝑥 ) → 𝑥 = 𝑦 ) ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ∀ 𝑧 ∈ 𝑃 ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( 𝑢 ∈ ( 𝑥 𝐼 𝑧 ) ∧ 𝑣 ∈ ( 𝑦 𝐼 𝑧 ) ) → ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑢 𝐼 𝑦 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑥 ) ) ) ∧ ∀ 𝑠 ∈ 𝒫 𝑃 ∀ 𝑡 ∈ 𝒫 𝑃 ( ∃ 𝑎 ∈ 𝑃 ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑡 𝑥 ∈ ( 𝑎 𝐼 𝑦 ) → ∃ 𝑏 ∈ 𝑃 ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑡 𝑏 ∈ ( 𝑥 𝐼 𝑦 ) ) ) )
20 19 simp2d ⊢ ( 𝐺 ∈ TarskiGB → ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ∀ 𝑧 ∈ 𝑃 ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( 𝑢 ∈ ( 𝑥 𝐼 𝑧 ) ∧ 𝑣 ∈ ( 𝑦 𝐼 𝑧 ) ) → ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑢 𝐼 𝑦 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑥 ) ) ) )
21 17 20 syl ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ∀ 𝑧 ∈ 𝑃 ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( 𝑢 ∈ ( 𝑥 𝐼 𝑧 ) ∧ 𝑣 ∈ ( 𝑦 𝐼 𝑧 ) ) → ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑢 𝐼 𝑦 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑥 ) ) ) )
22 oveq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 𝐼 𝑧 ) = ( 𝑋 𝐼 𝑧 ) )
23 22 eleq2d ⊢ ( 𝑥 = 𝑋 → ( 𝑢 ∈ ( 𝑥 𝐼 𝑧 ) ↔ 𝑢 ∈ ( 𝑋 𝐼 𝑧 ) ) )
24 23 anbi1d ⊢ ( 𝑥 = 𝑋 → ( ( 𝑢 ∈ ( 𝑥 𝐼 𝑧 ) ∧ 𝑣 ∈ ( 𝑦 𝐼 𝑧 ) ) ↔ ( 𝑢 ∈ ( 𝑋 𝐼 𝑧 ) ∧ 𝑣 ∈ ( 𝑦 𝐼 𝑧 ) ) ) )
25 oveq2 ⊢ ( 𝑥 = 𝑋 → ( 𝑣 𝐼 𝑥 ) = ( 𝑣 𝐼 𝑋 ) )
26 25 eleq2d ⊢ ( 𝑥 = 𝑋 → ( 𝑎 ∈ ( 𝑣 𝐼 𝑥 ) ↔ 𝑎 ∈ ( 𝑣 𝐼 𝑋 ) ) )
27 26 anbi2d ⊢ ( 𝑥 = 𝑋 → ( ( 𝑎 ∈ ( 𝑢 𝐼 𝑦 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑥 ) ) ↔ ( 𝑎 ∈ ( 𝑢 𝐼 𝑦 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑋 ) ) ) )
28 27 rexbidv ⊢ ( 𝑥 = 𝑋 → ( ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑢 𝐼 𝑦 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑥 ) ) ↔ ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑢 𝐼 𝑦 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑋 ) ) ) )
29 24 28 imbi12d ⊢ ( 𝑥 = 𝑋 → ( ( ( 𝑢 ∈ ( 𝑥 𝐼 𝑧 ) ∧ 𝑣 ∈ ( 𝑦 𝐼 𝑧 ) ) → ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑢 𝐼 𝑦 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑥 ) ) ) ↔ ( ( 𝑢 ∈ ( 𝑋 𝐼 𝑧 ) ∧ 𝑣 ∈ ( 𝑦 𝐼 𝑧 ) ) → ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑢 𝐼 𝑦 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑋 ) ) ) ) )
30 29 2ralbidv ⊢ ( 𝑥 = 𝑋 → ( ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( 𝑢 ∈ ( 𝑥 𝐼 𝑧 ) ∧ 𝑣 ∈ ( 𝑦 𝐼 𝑧 ) ) → ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑢 𝐼 𝑦 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑥 ) ) ) ↔ ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( 𝑢 ∈ ( 𝑋 𝐼 𝑧 ) ∧ 𝑣 ∈ ( 𝑦 𝐼 𝑧 ) ) → ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑢 𝐼 𝑦 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑋 ) ) ) ) )
31 oveq1 ⊢ ( 𝑦 = 𝑌 → ( 𝑦 𝐼 𝑧 ) = ( 𝑌 𝐼 𝑧 ) )
32 31 eleq2d ⊢ ( 𝑦 = 𝑌 → ( 𝑣 ∈ ( 𝑦 𝐼 𝑧 ) ↔ 𝑣 ∈ ( 𝑌 𝐼 𝑧 ) ) )
33 32 anbi2d ⊢ ( 𝑦 = 𝑌 → ( ( 𝑢 ∈ ( 𝑋 𝐼 𝑧 ) ∧ 𝑣 ∈ ( 𝑦 𝐼 𝑧 ) ) ↔ ( 𝑢 ∈ ( 𝑋 𝐼 𝑧 ) ∧ 𝑣 ∈ ( 𝑌 𝐼 𝑧 ) ) ) )
34 oveq2 ⊢ ( 𝑦 = 𝑌 → ( 𝑢 𝐼 𝑦 ) = ( 𝑢 𝐼 𝑌 ) )
35 34 eleq2d ⊢ ( 𝑦 = 𝑌 → ( 𝑎 ∈ ( 𝑢 𝐼 𝑦 ) ↔ 𝑎 ∈ ( 𝑢 𝐼 𝑌 ) ) )
36 35 anbi1d ⊢ ( 𝑦 = 𝑌 → ( ( 𝑎 ∈ ( 𝑢 𝐼 𝑦 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑋 ) ) ↔ ( 𝑎 ∈ ( 𝑢 𝐼 𝑌 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑋 ) ) ) )
37 36 rexbidv ⊢ ( 𝑦 = 𝑌 → ( ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑢 𝐼 𝑦 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑋 ) ) ↔ ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑢 𝐼 𝑌 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑋 ) ) ) )
38 33 37 imbi12d ⊢ ( 𝑦 = 𝑌 → ( ( ( 𝑢 ∈ ( 𝑋 𝐼 𝑧 ) ∧ 𝑣 ∈ ( 𝑦 𝐼 𝑧 ) ) → ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑢 𝐼 𝑦 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑋 ) ) ) ↔ ( ( 𝑢 ∈ ( 𝑋 𝐼 𝑧 ) ∧ 𝑣 ∈ ( 𝑌 𝐼 𝑧 ) ) → ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑢 𝐼 𝑌 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑋 ) ) ) ) )
39 38 2ralbidv ⊢ ( 𝑦 = 𝑌 → ( ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( 𝑢 ∈ ( 𝑋 𝐼 𝑧 ) ∧ 𝑣 ∈ ( 𝑦 𝐼 𝑧 ) ) → ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑢 𝐼 𝑦 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑋 ) ) ) ↔ ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( 𝑢 ∈ ( 𝑋 𝐼 𝑧 ) ∧ 𝑣 ∈ ( 𝑌 𝐼 𝑧 ) ) → ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑢 𝐼 𝑌 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑋 ) ) ) ) )
40 oveq2 ⊢ ( 𝑧 = 𝑍 → ( 𝑋 𝐼 𝑧 ) = ( 𝑋 𝐼 𝑍 ) )
41 40 eleq2d ⊢ ( 𝑧 = 𝑍 → ( 𝑢 ∈ ( 𝑋 𝐼 𝑧 ) ↔ 𝑢 ∈ ( 𝑋 𝐼 𝑍 ) ) )
42 oveq2 ⊢ ( 𝑧 = 𝑍 → ( 𝑌 𝐼 𝑧 ) = ( 𝑌 𝐼 𝑍 ) )
43 42 eleq2d ⊢ ( 𝑧 = 𝑍 → ( 𝑣 ∈ ( 𝑌 𝐼 𝑧 ) ↔ 𝑣 ∈ ( 𝑌 𝐼 𝑍 ) ) )
44 41 43 anbi12d ⊢ ( 𝑧 = 𝑍 → ( ( 𝑢 ∈ ( 𝑋 𝐼 𝑧 ) ∧ 𝑣 ∈ ( 𝑌 𝐼 𝑧 ) ) ↔ ( 𝑢 ∈ ( 𝑋 𝐼 𝑍 ) ∧ 𝑣 ∈ ( 𝑌 𝐼 𝑍 ) ) ) )
45 44 imbi1d ⊢ ( 𝑧 = 𝑍 → ( ( ( 𝑢 ∈ ( 𝑋 𝐼 𝑧 ) ∧ 𝑣 ∈ ( 𝑌 𝐼 𝑧 ) ) → ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑢 𝐼 𝑌 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑋 ) ) ) ↔ ( ( 𝑢 ∈ ( 𝑋 𝐼 𝑍 ) ∧ 𝑣 ∈ ( 𝑌 𝐼 𝑍 ) ) → ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑢 𝐼 𝑌 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑋 ) ) ) ) )
46 45 2ralbidv ⊢ ( 𝑧 = 𝑍 → ( ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( 𝑢 ∈ ( 𝑋 𝐼 𝑧 ) ∧ 𝑣 ∈ ( 𝑌 𝐼 𝑧 ) ) → ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑢 𝐼 𝑌 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑋 ) ) ) ↔ ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( 𝑢 ∈ ( 𝑋 𝐼 𝑍 ) ∧ 𝑣 ∈ ( 𝑌 𝐼 𝑍 ) ) → ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑢 𝐼 𝑌 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑋 ) ) ) ) )
47 30 39 46 rspc3v ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃 ) → ( ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ∀ 𝑧 ∈ 𝑃 ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( 𝑢 ∈ ( 𝑥 𝐼 𝑧 ) ∧ 𝑣 ∈ ( 𝑦 𝐼 𝑧 ) ) → ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑢 𝐼 𝑦 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑥 ) ) ) → ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( 𝑢 ∈ ( 𝑋 𝐼 𝑍 ) ∧ 𝑣 ∈ ( 𝑌 𝐼 𝑍 ) ) → ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑢 𝐼 𝑌 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑋 ) ) ) ) )
48 5 6 7 47 syl3anc ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ∀ 𝑧 ∈ 𝑃 ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( 𝑢 ∈ ( 𝑥 𝐼 𝑧 ) ∧ 𝑣 ∈ ( 𝑦 𝐼 𝑧 ) ) → ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑢 𝐼 𝑦 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑥 ) ) ) → ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( 𝑢 ∈ ( 𝑋 𝐼 𝑍 ) ∧ 𝑣 ∈ ( 𝑌 𝐼 𝑍 ) ) → ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑢 𝐼 𝑌 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑋 ) ) ) ) )
49 21 48 mpd ⊢ ( 𝜑 → ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( 𝑢 ∈ ( 𝑋 𝐼 𝑍 ) ∧ 𝑣 ∈ ( 𝑌 𝐼 𝑍 ) ) → ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑢 𝐼 𝑌 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑋 ) ) ) )
50 eleq1 ⊢ ( 𝑢 = 𝑈 → ( 𝑢 ∈ ( 𝑋 𝐼 𝑍 ) ↔ 𝑈 ∈ ( 𝑋 𝐼 𝑍 ) ) )
51 50 anbi1d ⊢ ( 𝑢 = 𝑈 → ( ( 𝑢 ∈ ( 𝑋 𝐼 𝑍 ) ∧ 𝑣 ∈ ( 𝑌 𝐼 𝑍 ) ) ↔ ( 𝑈 ∈ ( 𝑋 𝐼 𝑍 ) ∧ 𝑣 ∈ ( 𝑌 𝐼 𝑍 ) ) ) )
52 oveq1 ⊢ ( 𝑢 = 𝑈 → ( 𝑢 𝐼 𝑌 ) = ( 𝑈 𝐼 𝑌 ) )
53 52 eleq2d ⊢ ( 𝑢 = 𝑈 → ( 𝑎 ∈ ( 𝑢 𝐼 𝑌 ) ↔ 𝑎 ∈ ( 𝑈 𝐼 𝑌 ) ) )
54 53 anbi1d ⊢ ( 𝑢 = 𝑈 → ( ( 𝑎 ∈ ( 𝑢 𝐼 𝑌 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑋 ) ) ↔ ( 𝑎 ∈ ( 𝑈 𝐼 𝑌 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑋 ) ) ) )
55 54 rexbidv ⊢ ( 𝑢 = 𝑈 → ( ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑢 𝐼 𝑌 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑋 ) ) ↔ ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑈 𝐼 𝑌 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑋 ) ) ) )
56 51 55 imbi12d ⊢ ( 𝑢 = 𝑈 → ( ( ( 𝑢 ∈ ( 𝑋 𝐼 𝑍 ) ∧ 𝑣 ∈ ( 𝑌 𝐼 𝑍 ) ) → ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑢 𝐼 𝑌 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑋 ) ) ) ↔ ( ( 𝑈 ∈ ( 𝑋 𝐼 𝑍 ) ∧ 𝑣 ∈ ( 𝑌 𝐼 𝑍 ) ) → ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑈 𝐼 𝑌 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑋 ) ) ) ) )
57 eleq1 ⊢ ( 𝑣 = 𝑉 → ( 𝑣 ∈ ( 𝑌 𝐼 𝑍 ) ↔ 𝑉 ∈ ( 𝑌 𝐼 𝑍 ) ) )
58 57 anbi2d ⊢ ( 𝑣 = 𝑉 → ( ( 𝑈 ∈ ( 𝑋 𝐼 𝑍 ) ∧ 𝑣 ∈ ( 𝑌 𝐼 𝑍 ) ) ↔ ( 𝑈 ∈ ( 𝑋 𝐼 𝑍 ) ∧ 𝑉 ∈ ( 𝑌 𝐼 𝑍 ) ) ) )
59 oveq1 ⊢ ( 𝑣 = 𝑉 → ( 𝑣 𝐼 𝑋 ) = ( 𝑉 𝐼 𝑋 ) )
60 59 eleq2d ⊢ ( 𝑣 = 𝑉 → ( 𝑎 ∈ ( 𝑣 𝐼 𝑋 ) ↔ 𝑎 ∈ ( 𝑉 𝐼 𝑋 ) ) )
61 60 anbi2d ⊢ ( 𝑣 = 𝑉 → ( ( 𝑎 ∈ ( 𝑈 𝐼 𝑌 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑋 ) ) ↔ ( 𝑎 ∈ ( 𝑈 𝐼 𝑌 ) ∧ 𝑎 ∈ ( 𝑉 𝐼 𝑋 ) ) ) )
62 61 rexbidv ⊢ ( 𝑣 = 𝑉 → ( ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑈 𝐼 𝑌 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑋 ) ) ↔ ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑈 𝐼 𝑌 ) ∧ 𝑎 ∈ ( 𝑉 𝐼 𝑋 ) ) ) )
63 58 62 imbi12d ⊢ ( 𝑣 = 𝑉 → ( ( ( 𝑈 ∈ ( 𝑋 𝐼 𝑍 ) ∧ 𝑣 ∈ ( 𝑌 𝐼 𝑍 ) ) → ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑈 𝐼 𝑌 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑋 ) ) ) ↔ ( ( 𝑈 ∈ ( 𝑋 𝐼 𝑍 ) ∧ 𝑉 ∈ ( 𝑌 𝐼 𝑍 ) ) → ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑈 𝐼 𝑌 ) ∧ 𝑎 ∈ ( 𝑉 𝐼 𝑋 ) ) ) ) )
64 56 63 rspc2v ⊢ ( ( 𝑈 ∈ 𝑃 ∧ 𝑉 ∈ 𝑃 ) → ( ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( 𝑢 ∈ ( 𝑋 𝐼 𝑍 ) ∧ 𝑣 ∈ ( 𝑌 𝐼 𝑍 ) ) → ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑢 𝐼 𝑌 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑋 ) ) ) → ( ( 𝑈 ∈ ( 𝑋 𝐼 𝑍 ) ∧ 𝑉 ∈ ( 𝑌 𝐼 𝑍 ) ) → ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑈 𝐼 𝑌 ) ∧ 𝑎 ∈ ( 𝑉 𝐼 𝑋 ) ) ) ) )
65 8 9 64 syl2anc ⊢ ( 𝜑 → ( ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( 𝑢 ∈ ( 𝑋 𝐼 𝑍 ) ∧ 𝑣 ∈ ( 𝑌 𝐼 𝑍 ) ) → ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑢 𝐼 𝑌 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑋 ) ) ) → ( ( 𝑈 ∈ ( 𝑋 𝐼 𝑍 ) ∧ 𝑉 ∈ ( 𝑌 𝐼 𝑍 ) ) → ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑈 𝐼 𝑌 ) ∧ 𝑎 ∈ ( 𝑉 𝐼 𝑋 ) ) ) ) )
66 49 65 mpd ⊢ ( 𝜑 → ( ( 𝑈 ∈ ( 𝑋 𝐼 𝑍 ) ∧ 𝑉 ∈ ( 𝑌 𝐼 𝑍 ) ) → ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑈 𝐼 𝑌 ) ∧ 𝑎 ∈ ( 𝑉 𝐼 𝑋 ) ) ) )
67 10 11 66 mp2and ⊢ ( 𝜑 → ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑈 𝐼 𝑌 ) ∧ 𝑎 ∈ ( 𝑉 𝐼 𝑋 ) ) )