# 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 ${⊢}{P}={\mathrm{Base}}_{{G}}$
axtrkg.d
axtrkg.i ${⊢}{I}=\mathrm{Itv}\left({G}\right)$
axtrkg.g ${⊢}{\phi }\to {G}\in {𝒢}_{\mathrm{Tarski}}$
axtgpasch.1 ${⊢}{\phi }\to {X}\in {P}$
axtgpasch.2 ${⊢}{\phi }\to {Y}\in {P}$
axtgpasch.3 ${⊢}{\phi }\to {Z}\in {P}$
axtgpasch.4 ${⊢}{\phi }\to {U}\in {P}$
axtgpasch.5 ${⊢}{\phi }\to {V}\in {P}$
axtgpasch.6 ${⊢}{\phi }\to {U}\in \left({X}{I}{Z}\right)$
axtgpasch.7 ${⊢}{\phi }\to {V}\in \left({Y}{I}{Z}\right)$
Assertion axtgpasch ${⊢}{\phi }\to \exists {a}\in {P}\phantom{\rule{.4em}{0ex}}\left({a}\in \left({U}{I}{Y}\right)\wedge {a}\in \left({V}{I}{X}\right)\right)$

### Proof

Step Hyp Ref Expression
1 axtrkg.p ${⊢}{P}={\mathrm{Base}}_{{G}}$
2 axtrkg.d
3 axtrkg.i ${⊢}{I}=\mathrm{Itv}\left({G}\right)$
4 axtrkg.g ${⊢}{\phi }\to {G}\in {𝒢}_{\mathrm{Tarski}}$
5 axtgpasch.1 ${⊢}{\phi }\to {X}\in {P}$
6 axtgpasch.2 ${⊢}{\phi }\to {Y}\in {P}$
7 axtgpasch.3 ${⊢}{\phi }\to {Z}\in {P}$
8 axtgpasch.4 ${⊢}{\phi }\to {U}\in {P}$
9 axtgpasch.5 ${⊢}{\phi }\to {V}\in {P}$
10 axtgpasch.6 ${⊢}{\phi }\to {U}\in \left({X}{I}{Z}\right)$
11 axtgpasch.7 ${⊢}{\phi }\to {V}\in \left({Y}{I}{Z}\right)$
12 df-trkg
13 inss1
14 inss2 ${⊢}{𝒢}_{\mathrm{Tarski}}^{C}\cap {𝒢}_{\mathrm{Tarski}}^{B}\subseteq {𝒢}_{\mathrm{Tarski}}^{B}$
15 13 14 sstri
16 12 15 eqsstri ${⊢}{𝒢}_{\mathrm{Tarski}}\subseteq {𝒢}_{\mathrm{Tarski}}^{B}$
17 16 4 sseldi ${⊢}{\phi }\to {G}\in {𝒢}_{\mathrm{Tarski}}^{B}$
18 1 2 3 istrkgb ${⊢}{G}\in {𝒢}_{\mathrm{Tarski}}^{B}↔\left({G}\in \mathrm{V}\wedge \left(\forall {x}\in {P}\phantom{\rule{.4em}{0ex}}\forall {y}\in {P}\phantom{\rule{.4em}{0ex}}\left({y}\in \left({x}{I}{x}\right)\to {x}={y}\right)\wedge \forall {x}\in {P}\phantom{\rule{.4em}{0ex}}\forall {y}\in {P}\phantom{\rule{.4em}{0ex}}\forall {z}\in {P}\phantom{\rule{.4em}{0ex}}\forall {u}\in {P}\phantom{\rule{.4em}{0ex}}\forall {v}\in {P}\phantom{\rule{.4em}{0ex}}\left(\left({u}\in \left({x}{I}{z}\right)\wedge {v}\in \left({y}{I}{z}\right)\right)\to \exists {a}\in {P}\phantom{\rule{.4em}{0ex}}\left({a}\in \left({u}{I}{y}\right)\wedge {a}\in \left({v}{I}{x}\right)\right)\right)\wedge \forall {s}\in 𝒫{P}\phantom{\rule{.4em}{0ex}}\forall {t}\in 𝒫{P}\phantom{\rule{.4em}{0ex}}\left(\exists {a}\in {P}\phantom{\rule{.4em}{0ex}}\forall {x}\in {s}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{x}\in \left({a}{I}{y}\right)\to \exists {b}\in {P}\phantom{\rule{.4em}{0ex}}\forall {x}\in {s}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{b}\in \left({x}{I}{y}\right)\right)\right)\right)$
19 18 simprbi ${⊢}{G}\in {𝒢}_{\mathrm{Tarski}}^{B}\to \left(\forall {x}\in {P}\phantom{\rule{.4em}{0ex}}\forall {y}\in {P}\phantom{\rule{.4em}{0ex}}\left({y}\in \left({x}{I}{x}\right)\to {x}={y}\right)\wedge \forall {x}\in {P}\phantom{\rule{.4em}{0ex}}\forall {y}\in {P}\phantom{\rule{.4em}{0ex}}\forall {z}\in {P}\phantom{\rule{.4em}{0ex}}\forall {u}\in {P}\phantom{\rule{.4em}{0ex}}\forall {v}\in {P}\phantom{\rule{.4em}{0ex}}\left(\left({u}\in \left({x}{I}{z}\right)\wedge {v}\in \left({y}{I}{z}\right)\right)\to \exists {a}\in {P}\phantom{\rule{.4em}{0ex}}\left({a}\in \left({u}{I}{y}\right)\wedge {a}\in \left({v}{I}{x}\right)\right)\right)\wedge \forall {s}\in 𝒫{P}\phantom{\rule{.4em}{0ex}}\forall {t}\in 𝒫{P}\phantom{\rule{.4em}{0ex}}\left(\exists {a}\in {P}\phantom{\rule{.4em}{0ex}}\forall {x}\in {s}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{x}\in \left({a}{I}{y}\right)\to \exists {b}\in {P}\phantom{\rule{.4em}{0ex}}\forall {x}\in {s}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{b}\in \left({x}{I}{y}\right)\right)\right)$
20 19 simp2d ${⊢}{G}\in {𝒢}_{\mathrm{Tarski}}^{B}\to \forall {x}\in {P}\phantom{\rule{.4em}{0ex}}\forall {y}\in {P}\phantom{\rule{.4em}{0ex}}\forall {z}\in {P}\phantom{\rule{.4em}{0ex}}\forall {u}\in {P}\phantom{\rule{.4em}{0ex}}\forall {v}\in {P}\phantom{\rule{.4em}{0ex}}\left(\left({u}\in \left({x}{I}{z}\right)\wedge {v}\in \left({y}{I}{z}\right)\right)\to \exists {a}\in {P}\phantom{\rule{.4em}{0ex}}\left({a}\in \left({u}{I}{y}\right)\wedge {a}\in \left({v}{I}{x}\right)\right)\right)$
21 17 20 syl ${⊢}{\phi }\to \forall {x}\in {P}\phantom{\rule{.4em}{0ex}}\forall {y}\in {P}\phantom{\rule{.4em}{0ex}}\forall {z}\in {P}\phantom{\rule{.4em}{0ex}}\forall {u}\in {P}\phantom{\rule{.4em}{0ex}}\forall {v}\in {P}\phantom{\rule{.4em}{0ex}}\left(\left({u}\in \left({x}{I}{z}\right)\wedge {v}\in \left({y}{I}{z}\right)\right)\to \exists {a}\in {P}\phantom{\rule{.4em}{0ex}}\left({a}\in \left({u}{I}{y}\right)\wedge {a}\in \left({v}{I}{x}\right)\right)\right)$
22 oveq1 ${⊢}{x}={X}\to {x}{I}{z}={X}{I}{z}$
23 22 eleq2d ${⊢}{x}={X}\to \left({u}\in \left({x}{I}{z}\right)↔{u}\in \left({X}{I}{z}\right)\right)$
24 23 anbi1d ${⊢}{x}={X}\to \left(\left({u}\in \left({x}{I}{z}\right)\wedge {v}\in \left({y}{I}{z}\right)\right)↔\left({u}\in \left({X}{I}{z}\right)\wedge {v}\in \left({y}{I}{z}\right)\right)\right)$
25 oveq2 ${⊢}{x}={X}\to {v}{I}{x}={v}{I}{X}$
26 25 eleq2d ${⊢}{x}={X}\to \left({a}\in \left({v}{I}{x}\right)↔{a}\in \left({v}{I}{X}\right)\right)$
27 26 anbi2d ${⊢}{x}={X}\to \left(\left({a}\in \left({u}{I}{y}\right)\wedge {a}\in \left({v}{I}{x}\right)\right)↔\left({a}\in \left({u}{I}{y}\right)\wedge {a}\in \left({v}{I}{X}\right)\right)\right)$
28 27 rexbidv ${⊢}{x}={X}\to \left(\exists {a}\in {P}\phantom{\rule{.4em}{0ex}}\left({a}\in \left({u}{I}{y}\right)\wedge {a}\in \left({v}{I}{x}\right)\right)↔\exists {a}\in {P}\phantom{\rule{.4em}{0ex}}\left({a}\in \left({u}{I}{y}\right)\wedge {a}\in \left({v}{I}{X}\right)\right)\right)$
29 24 28 imbi12d ${⊢}{x}={X}\to \left(\left(\left({u}\in \left({x}{I}{z}\right)\wedge {v}\in \left({y}{I}{z}\right)\right)\to \exists {a}\in {P}\phantom{\rule{.4em}{0ex}}\left({a}\in \left({u}{I}{y}\right)\wedge {a}\in \left({v}{I}{x}\right)\right)\right)↔\left(\left({u}\in \left({X}{I}{z}\right)\wedge {v}\in \left({y}{I}{z}\right)\right)\to \exists {a}\in {P}\phantom{\rule{.4em}{0ex}}\left({a}\in \left({u}{I}{y}\right)\wedge {a}\in \left({v}{I}{X}\right)\right)\right)\right)$
30 29 2ralbidv ${⊢}{x}={X}\to \left(\forall {u}\in {P}\phantom{\rule{.4em}{0ex}}\forall {v}\in {P}\phantom{\rule{.4em}{0ex}}\left(\left({u}\in \left({x}{I}{z}\right)\wedge {v}\in \left({y}{I}{z}\right)\right)\to \exists {a}\in {P}\phantom{\rule{.4em}{0ex}}\left({a}\in \left({u}{I}{y}\right)\wedge {a}\in \left({v}{I}{x}\right)\right)\right)↔\forall {u}\in {P}\phantom{\rule{.4em}{0ex}}\forall {v}\in {P}\phantom{\rule{.4em}{0ex}}\left(\left({u}\in \left({X}{I}{z}\right)\wedge {v}\in \left({y}{I}{z}\right)\right)\to \exists {a}\in {P}\phantom{\rule{.4em}{0ex}}\left({a}\in \left({u}{I}{y}\right)\wedge {a}\in \left({v}{I}{X}\right)\right)\right)\right)$
31 oveq1 ${⊢}{y}={Y}\to {y}{I}{z}={Y}{I}{z}$
32 31 eleq2d ${⊢}{y}={Y}\to \left({v}\in \left({y}{I}{z}\right)↔{v}\in \left({Y}{I}{z}\right)\right)$
33 32 anbi2d ${⊢}{y}={Y}\to \left(\left({u}\in \left({X}{I}{z}\right)\wedge {v}\in \left({y}{I}{z}\right)\right)↔\left({u}\in \left({X}{I}{z}\right)\wedge {v}\in \left({Y}{I}{z}\right)\right)\right)$
34 oveq2 ${⊢}{y}={Y}\to {u}{I}{y}={u}{I}{Y}$
35 34 eleq2d ${⊢}{y}={Y}\to \left({a}\in \left({u}{I}{y}\right)↔{a}\in \left({u}{I}{Y}\right)\right)$
36 35 anbi1d ${⊢}{y}={Y}\to \left(\left({a}\in \left({u}{I}{y}\right)\wedge {a}\in \left({v}{I}{X}\right)\right)↔\left({a}\in \left({u}{I}{Y}\right)\wedge {a}\in \left({v}{I}{X}\right)\right)\right)$
37 36 rexbidv ${⊢}{y}={Y}\to \left(\exists {a}\in {P}\phantom{\rule{.4em}{0ex}}\left({a}\in \left({u}{I}{y}\right)\wedge {a}\in \left({v}{I}{X}\right)\right)↔\exists {a}\in {P}\phantom{\rule{.4em}{0ex}}\left({a}\in \left({u}{I}{Y}\right)\wedge {a}\in \left({v}{I}{X}\right)\right)\right)$
38 33 37 imbi12d ${⊢}{y}={Y}\to \left(\left(\left({u}\in \left({X}{I}{z}\right)\wedge {v}\in \left({y}{I}{z}\right)\right)\to \exists {a}\in {P}\phantom{\rule{.4em}{0ex}}\left({a}\in \left({u}{I}{y}\right)\wedge {a}\in \left({v}{I}{X}\right)\right)\right)↔\left(\left({u}\in \left({X}{I}{z}\right)\wedge {v}\in \left({Y}{I}{z}\right)\right)\to \exists {a}\in {P}\phantom{\rule{.4em}{0ex}}\left({a}\in \left({u}{I}{Y}\right)\wedge {a}\in \left({v}{I}{X}\right)\right)\right)\right)$
39 38 2ralbidv ${⊢}{y}={Y}\to \left(\forall {u}\in {P}\phantom{\rule{.4em}{0ex}}\forall {v}\in {P}\phantom{\rule{.4em}{0ex}}\left(\left({u}\in \left({X}{I}{z}\right)\wedge {v}\in \left({y}{I}{z}\right)\right)\to \exists {a}\in {P}\phantom{\rule{.4em}{0ex}}\left({a}\in \left({u}{I}{y}\right)\wedge {a}\in \left({v}{I}{X}\right)\right)\right)↔\forall {u}\in {P}\phantom{\rule{.4em}{0ex}}\forall {v}\in {P}\phantom{\rule{.4em}{0ex}}\left(\left({u}\in \left({X}{I}{z}\right)\wedge {v}\in \left({Y}{I}{z}\right)\right)\to \exists {a}\in {P}\phantom{\rule{.4em}{0ex}}\left({a}\in \left({u}{I}{Y}\right)\wedge {a}\in \left({v}{I}{X}\right)\right)\right)\right)$
40 oveq2 ${⊢}{z}={Z}\to {X}{I}{z}={X}{I}{Z}$
41 40 eleq2d ${⊢}{z}={Z}\to \left({u}\in \left({X}{I}{z}\right)↔{u}\in \left({X}{I}{Z}\right)\right)$
42 oveq2 ${⊢}{z}={Z}\to {Y}{I}{z}={Y}{I}{Z}$
43 42 eleq2d ${⊢}{z}={Z}\to \left({v}\in \left({Y}{I}{z}\right)↔{v}\in \left({Y}{I}{Z}\right)\right)$
44 41 43 anbi12d ${⊢}{z}={Z}\to \left(\left({u}\in \left({X}{I}{z}\right)\wedge {v}\in \left({Y}{I}{z}\right)\right)↔\left({u}\in \left({X}{I}{Z}\right)\wedge {v}\in \left({Y}{I}{Z}\right)\right)\right)$
45 44 imbi1d ${⊢}{z}={Z}\to \left(\left(\left({u}\in \left({X}{I}{z}\right)\wedge {v}\in \left({Y}{I}{z}\right)\right)\to \exists {a}\in {P}\phantom{\rule{.4em}{0ex}}\left({a}\in \left({u}{I}{Y}\right)\wedge {a}\in \left({v}{I}{X}\right)\right)\right)↔\left(\left({u}\in \left({X}{I}{Z}\right)\wedge {v}\in \left({Y}{I}{Z}\right)\right)\to \exists {a}\in {P}\phantom{\rule{.4em}{0ex}}\left({a}\in \left({u}{I}{Y}\right)\wedge {a}\in \left({v}{I}{X}\right)\right)\right)\right)$
46 45 2ralbidv ${⊢}{z}={Z}\to \left(\forall {u}\in {P}\phantom{\rule{.4em}{0ex}}\forall {v}\in {P}\phantom{\rule{.4em}{0ex}}\left(\left({u}\in \left({X}{I}{z}\right)\wedge {v}\in \left({Y}{I}{z}\right)\right)\to \exists {a}\in {P}\phantom{\rule{.4em}{0ex}}\left({a}\in \left({u}{I}{Y}\right)\wedge {a}\in \left({v}{I}{X}\right)\right)\right)↔\forall {u}\in {P}\phantom{\rule{.4em}{0ex}}\forall {v}\in {P}\phantom{\rule{.4em}{0ex}}\left(\left({u}\in \left({X}{I}{Z}\right)\wedge {v}\in \left({Y}{I}{Z}\right)\right)\to \exists {a}\in {P}\phantom{\rule{.4em}{0ex}}\left({a}\in \left({u}{I}{Y}\right)\wedge {a}\in \left({v}{I}{X}\right)\right)\right)\right)$
47 30 39 46 rspc3v ${⊢}\left({X}\in {P}\wedge {Y}\in {P}\wedge {Z}\in {P}\right)\to \left(\forall {x}\in {P}\phantom{\rule{.4em}{0ex}}\forall {y}\in {P}\phantom{\rule{.4em}{0ex}}\forall {z}\in {P}\phantom{\rule{.4em}{0ex}}\forall {u}\in {P}\phantom{\rule{.4em}{0ex}}\forall {v}\in {P}\phantom{\rule{.4em}{0ex}}\left(\left({u}\in \left({x}{I}{z}\right)\wedge {v}\in \left({y}{I}{z}\right)\right)\to \exists {a}\in {P}\phantom{\rule{.4em}{0ex}}\left({a}\in \left({u}{I}{y}\right)\wedge {a}\in \left({v}{I}{x}\right)\right)\right)\to \forall {u}\in {P}\phantom{\rule{.4em}{0ex}}\forall {v}\in {P}\phantom{\rule{.4em}{0ex}}\left(\left({u}\in \left({X}{I}{Z}\right)\wedge {v}\in \left({Y}{I}{Z}\right)\right)\to \exists {a}\in {P}\phantom{\rule{.4em}{0ex}}\left({a}\in \left({u}{I}{Y}\right)\wedge {a}\in \left({v}{I}{X}\right)\right)\right)\right)$
48 5 6 7 47 syl3anc ${⊢}{\phi }\to \left(\forall {x}\in {P}\phantom{\rule{.4em}{0ex}}\forall {y}\in {P}\phantom{\rule{.4em}{0ex}}\forall {z}\in {P}\phantom{\rule{.4em}{0ex}}\forall {u}\in {P}\phantom{\rule{.4em}{0ex}}\forall {v}\in {P}\phantom{\rule{.4em}{0ex}}\left(\left({u}\in \left({x}{I}{z}\right)\wedge {v}\in \left({y}{I}{z}\right)\right)\to \exists {a}\in {P}\phantom{\rule{.4em}{0ex}}\left({a}\in \left({u}{I}{y}\right)\wedge {a}\in \left({v}{I}{x}\right)\right)\right)\to \forall {u}\in {P}\phantom{\rule{.4em}{0ex}}\forall {v}\in {P}\phantom{\rule{.4em}{0ex}}\left(\left({u}\in \left({X}{I}{Z}\right)\wedge {v}\in \left({Y}{I}{Z}\right)\right)\to \exists {a}\in {P}\phantom{\rule{.4em}{0ex}}\left({a}\in \left({u}{I}{Y}\right)\wedge {a}\in \left({v}{I}{X}\right)\right)\right)\right)$
49 21 48 mpd ${⊢}{\phi }\to \forall {u}\in {P}\phantom{\rule{.4em}{0ex}}\forall {v}\in {P}\phantom{\rule{.4em}{0ex}}\left(\left({u}\in \left({X}{I}{Z}\right)\wedge {v}\in \left({Y}{I}{Z}\right)\right)\to \exists {a}\in {P}\phantom{\rule{.4em}{0ex}}\left({a}\in \left({u}{I}{Y}\right)\wedge {a}\in \left({v}{I}{X}\right)\right)\right)$
50 eleq1 ${⊢}{u}={U}\to \left({u}\in \left({X}{I}{Z}\right)↔{U}\in \left({X}{I}{Z}\right)\right)$
51 50 anbi1d ${⊢}{u}={U}\to \left(\left({u}\in \left({X}{I}{Z}\right)\wedge {v}\in \left({Y}{I}{Z}\right)\right)↔\left({U}\in \left({X}{I}{Z}\right)\wedge {v}\in \left({Y}{I}{Z}\right)\right)\right)$
52 oveq1 ${⊢}{u}={U}\to {u}{I}{Y}={U}{I}{Y}$
53 52 eleq2d ${⊢}{u}={U}\to \left({a}\in \left({u}{I}{Y}\right)↔{a}\in \left({U}{I}{Y}\right)\right)$
54 53 anbi1d ${⊢}{u}={U}\to \left(\left({a}\in \left({u}{I}{Y}\right)\wedge {a}\in \left({v}{I}{X}\right)\right)↔\left({a}\in \left({U}{I}{Y}\right)\wedge {a}\in \left({v}{I}{X}\right)\right)\right)$
55 54 rexbidv ${⊢}{u}={U}\to \left(\exists {a}\in {P}\phantom{\rule{.4em}{0ex}}\left({a}\in \left({u}{I}{Y}\right)\wedge {a}\in \left({v}{I}{X}\right)\right)↔\exists {a}\in {P}\phantom{\rule{.4em}{0ex}}\left({a}\in \left({U}{I}{Y}\right)\wedge {a}\in \left({v}{I}{X}\right)\right)\right)$
56 51 55 imbi12d ${⊢}{u}={U}\to \left(\left(\left({u}\in \left({X}{I}{Z}\right)\wedge {v}\in \left({Y}{I}{Z}\right)\right)\to \exists {a}\in {P}\phantom{\rule{.4em}{0ex}}\left({a}\in \left({u}{I}{Y}\right)\wedge {a}\in \left({v}{I}{X}\right)\right)\right)↔\left(\left({U}\in \left({X}{I}{Z}\right)\wedge {v}\in \left({Y}{I}{Z}\right)\right)\to \exists {a}\in {P}\phantom{\rule{.4em}{0ex}}\left({a}\in \left({U}{I}{Y}\right)\wedge {a}\in \left({v}{I}{X}\right)\right)\right)\right)$
57 eleq1 ${⊢}{v}={V}\to \left({v}\in \left({Y}{I}{Z}\right)↔{V}\in \left({Y}{I}{Z}\right)\right)$
58 57 anbi2d ${⊢}{v}={V}\to \left(\left({U}\in \left({X}{I}{Z}\right)\wedge {v}\in \left({Y}{I}{Z}\right)\right)↔\left({U}\in \left({X}{I}{Z}\right)\wedge {V}\in \left({Y}{I}{Z}\right)\right)\right)$
59 oveq1 ${⊢}{v}={V}\to {v}{I}{X}={V}{I}{X}$
60 59 eleq2d ${⊢}{v}={V}\to \left({a}\in \left({v}{I}{X}\right)↔{a}\in \left({V}{I}{X}\right)\right)$
61 60 anbi2d ${⊢}{v}={V}\to \left(\left({a}\in \left({U}{I}{Y}\right)\wedge {a}\in \left({v}{I}{X}\right)\right)↔\left({a}\in \left({U}{I}{Y}\right)\wedge {a}\in \left({V}{I}{X}\right)\right)\right)$
62 61 rexbidv ${⊢}{v}={V}\to \left(\exists {a}\in {P}\phantom{\rule{.4em}{0ex}}\left({a}\in \left({U}{I}{Y}\right)\wedge {a}\in \left({v}{I}{X}\right)\right)↔\exists {a}\in {P}\phantom{\rule{.4em}{0ex}}\left({a}\in \left({U}{I}{Y}\right)\wedge {a}\in \left({V}{I}{X}\right)\right)\right)$
63 58 62 imbi12d ${⊢}{v}={V}\to \left(\left(\left({U}\in \left({X}{I}{Z}\right)\wedge {v}\in \left({Y}{I}{Z}\right)\right)\to \exists {a}\in {P}\phantom{\rule{.4em}{0ex}}\left({a}\in \left({U}{I}{Y}\right)\wedge {a}\in \left({v}{I}{X}\right)\right)\right)↔\left(\left({U}\in \left({X}{I}{Z}\right)\wedge {V}\in \left({Y}{I}{Z}\right)\right)\to \exists {a}\in {P}\phantom{\rule{.4em}{0ex}}\left({a}\in \left({U}{I}{Y}\right)\wedge {a}\in \left({V}{I}{X}\right)\right)\right)\right)$
64 56 63 rspc2v ${⊢}\left({U}\in {P}\wedge {V}\in {P}\right)\to \left(\forall {u}\in {P}\phantom{\rule{.4em}{0ex}}\forall {v}\in {P}\phantom{\rule{.4em}{0ex}}\left(\left({u}\in \left({X}{I}{Z}\right)\wedge {v}\in \left({Y}{I}{Z}\right)\right)\to \exists {a}\in {P}\phantom{\rule{.4em}{0ex}}\left({a}\in \left({u}{I}{Y}\right)\wedge {a}\in \left({v}{I}{X}\right)\right)\right)\to \left(\left({U}\in \left({X}{I}{Z}\right)\wedge {V}\in \left({Y}{I}{Z}\right)\right)\to \exists {a}\in {P}\phantom{\rule{.4em}{0ex}}\left({a}\in \left({U}{I}{Y}\right)\wedge {a}\in \left({V}{I}{X}\right)\right)\right)\right)$
65 8 9 64 syl2anc ${⊢}{\phi }\to \left(\forall {u}\in {P}\phantom{\rule{.4em}{0ex}}\forall {v}\in {P}\phantom{\rule{.4em}{0ex}}\left(\left({u}\in \left({X}{I}{Z}\right)\wedge {v}\in \left({Y}{I}{Z}\right)\right)\to \exists {a}\in {P}\phantom{\rule{.4em}{0ex}}\left({a}\in \left({u}{I}{Y}\right)\wedge {a}\in \left({v}{I}{X}\right)\right)\right)\to \left(\left({U}\in \left({X}{I}{Z}\right)\wedge {V}\in \left({Y}{I}{Z}\right)\right)\to \exists {a}\in {P}\phantom{\rule{.4em}{0ex}}\left({a}\in \left({U}{I}{Y}\right)\wedge {a}\in \left({V}{I}{X}\right)\right)\right)\right)$
66 49 65 mpd ${⊢}{\phi }\to \left(\left({U}\in \left({X}{I}{Z}\right)\wedge {V}\in \left({Y}{I}{Z}\right)\right)\to \exists {a}\in {P}\phantom{\rule{.4em}{0ex}}\left({a}\in \left({U}{I}{Y}\right)\wedge {a}\in \left({V}{I}{X}\right)\right)\right)$
67 10 11 66 mp2and ${⊢}{\phi }\to \exists {a}\in {P}\phantom{\rule{.4em}{0ex}}\left({a}\in \left({U}{I}{Y}\right)\wedge {a}\in \left({V}{I}{X}\right)\right)$