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 ( 𝜑 → ∃ 𝑎𝑃 ( 𝑎 ∈ ( 𝑈 𝐼 𝑌 ) ∧ 𝑎 ∈ ( 𝑉 𝐼 𝑋 ) ) )