Theorem dfprlng2

Description: Alternate definition of (strict) parallelism. Theorem 12.7 of Schwabhauser p. 122. (Contributed by Thierry Arnoux, 13-Jul-2026)

	Ref	Expression
Hypotheses	dfprlng2.b	$$⊢P={\mathrm{Base}}_G$$
	dfprlng2.l	$$⊢L={Line}_{𝒢}\left(G\right)$$
	dfprlng2.p	No typesetting found for |- .|| = ( parlnG ` G ) with typecode |-
	dfprlng2.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
	dfprlng2.x	$$⊢\phi \to X\in P$$
	dfprlng2.y	$$⊢\phi \to Y\in \left(P\setminus \left\{X\right\}\right)$$
	dfprlng2.z	$$⊢\phi \to Z\in P$$
	dfprlng2.w	$$⊢\phi \to W\in \left(P\setminus \left\{Z\right\}\right)$$
	dfprlng2.1	$$⊢\phi \to XLY\ne ZLW$$
Assertion	dfprlng2	$$⊢\phi \to \left(\left(XLY\right)\underset{\dot{}}{\parallel }\left(ZLW\right)\leftrightarrow \left(Z{hp}_{𝒢}\left(G\right)\left(XLY\right)W\wedge \left(XLY\right)\cap \left(ZLW\right)=\varnothing \right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		dfprlng2.b	$$⊢P={\mathrm{Base}}_G$$
2		dfprlng2.l	$$⊢L={Line}_{𝒢}\left(G\right)$$
3		dfprlng2.p	Could not format .|| = ( parlnG ` G ) : No typesetting found for |- .|| = ( parlnG ` G ) with typecode |-
4		dfprlng2.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
5		dfprlng2.x	$$⊢\phi \to X\in P$$
6		dfprlng2.y	$$⊢\phi \to Y\in \left(P\setminus \left\{X\right\}\right)$$
7		dfprlng2.z	$$⊢\phi \to Z\in P$$
8		dfprlng2.w	$$⊢\phi \to W\in \left(P\setminus \left\{Z\right\}\right)$$
9		dfprlng2.1	$$⊢\phi \to XLY\ne ZLW$$
10	9	neneqd	$$⊢\phi \to \neg XLY=ZLW$$
11		biorf	Could not format ( -. ( X L Y ) = ( Z L W ) -> ( ( E. h e. ran ( PlnG ` G ) ( ( X L Y ) C_ h /\ ( Z L W ) C_ h ) /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) <-> ( ( X L Y ) = ( Z L W ) \/ ( E. h e. ran ( PlnG ` G ) ( ( X L Y ) C_ h /\ ( Z L W ) C_ h ) /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) ) ) ) : No typesetting found for |- ( -. ( X L Y ) = ( Z L W ) -> ( ( E. h e. ran ( PlnG ` G ) ( ( X L Y ) C_ h /\ ( Z L W ) C_ h ) /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) <-> ( ( X L Y ) = ( Z L W ) \/ ( E. h e. ran ( PlnG ` G ) ( ( X L Y ) C_ h /\ ( Z L W ) C_ h ) /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) ) ) ) with typecode |-
12	10 11	syl	Could not format ( ph -> ( ( E. h e. ran ( PlnG ` G ) ( ( X L Y ) C_ h /\ ( Z L W ) C_ h ) /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) <-> ( ( X L Y ) = ( Z L W ) \/ ( E. h e. ran ( PlnG ` G ) ( ( X L Y ) C_ h /\ ( Z L W ) C_ h ) /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) ) ) ) : No typesetting found for |- ( ph -> ( ( E. h e. ran ( PlnG ` G ) ( ( X L Y ) C_ h /\ ( Z L W ) C_ h ) /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) <-> ( ( X L Y ) = ( Z L W ) \/ ( E. h e. ran ( PlnG ` G ) ( ( X L Y ) C_ h /\ ( Z L W ) C_ h ) /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) ) ) ) with typecode |-
13	12	anbi2d	Could not format ( ph -> ( ( ( ( X L Y ) e. ran L /\ ( Z L W ) e. ran L ) /\ ( E. h e. ran ( PlnG ` G ) ( ( X L Y ) C_ h /\ ( Z L W ) C_ h ) /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) ) <-> ( ( ( X L Y ) e. ran L /\ ( Z L W ) e. ran L ) /\ ( ( X L Y ) = ( Z L W ) \/ ( E. h e. ran ( PlnG ` G ) ( ( X L Y ) C_ h /\ ( Z L W ) C_ h ) /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) ) ) ) ) : No typesetting found for |- ( ph -> ( ( ( ( X L Y ) e. ran L /\ ( Z L W ) e. ran L ) /\ ( E. h e. ran ( PlnG ` G ) ( ( X L Y ) C_ h /\ ( Z L W ) C_ h ) /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) ) <-> ( ( ( X L Y ) e. ran L /\ ( Z L W ) e. ran L ) /\ ( ( X L Y ) = ( Z L W ) \/ ( E. h e. ran ( PlnG ` G ) ( ( X L Y ) C_ h /\ ( Z L W ) C_ h ) /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) ) ) ) ) with typecode |-
14		eqid	$$⊢\mathrm{Itv}\left(G\right)=\mathrm{Itv}\left(G\right)$$
15	6	eldifad	$$⊢\phi \to Y\in P$$
16	6	eldifsnbd	$$⊢\phi \to Y\ne X$$
17	16	necomd	$$⊢\phi \to X\ne Y$$
18	1 14 2 4 5 15 17	tgelrnln	$$⊢\phi \to XLY\in \mathrm{ran}L$$
19	8	eldifad	$$⊢\phi \to W\in P$$
20	8	eldifsnbd	$$⊢\phi \to W\ne Z$$
21	20	necomd	$$⊢\phi \to Z\ne W$$
22	1 14 2 4 7 19 21	tgelrnln	$$⊢\phi \to ZLW\in \mathrm{ran}L$$
23	18 22	jca	$$⊢\phi \to \left(XLY\in \mathrm{ran}L\wedge ZLW\in \mathrm{ran}L\right)$$
24	23	biantrurd	Could not format ( ph -> ( ( E. h e. ran ( PlnG ` G ) ( ( X L Y ) C_ h /\ ( Z L W ) C_ h ) /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) <-> ( ( ( X L Y ) e. ran L /\ ( Z L W ) e. ran L ) /\ ( E. h e. ran ( PlnG ` G ) ( ( X L Y ) C_ h /\ ( Z L W ) C_ h ) /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) ) ) ) : No typesetting found for |- ( ph -> ( ( E. h e. ran ( PlnG ` G ) ( ( X L Y ) C_ h /\ ( Z L W ) C_ h ) /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) <-> ( ( ( X L Y ) e. ran L /\ ( Z L W ) e. ran L ) /\ ( E. h e. ran ( PlnG ` G ) ( ( X L Y ) C_ h /\ ( Z L W ) C_ h ) /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) ) ) ) with typecode |-
25		eqid	Could not format ( PlnG ` G ) = ( PlnG ` G ) : No typesetting found for |- ( PlnG ` G ) = ( PlnG ` G ) with typecode |-
26	2 25 3 4	brprlng	Could not format ( ph -> ( ( X L Y ) .|| ( Z L W ) <-> ( ( ( X L Y ) e. ran L /\ ( Z L W ) e. ran L ) /\ ( ( X L Y ) = ( Z L W ) \/ ( E. h e. ran ( PlnG ` G ) ( ( X L Y ) C_ h /\ ( Z L W ) C_ h ) /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) ) ) ) ) : No typesetting found for |- ( ph -> ( ( X L Y ) .|| ( Z L W ) <-> ( ( ( X L Y ) e. ran L /\ ( Z L W ) e. ran L ) /\ ( ( X L Y ) = ( Z L W ) \/ ( E. h e. ran ( PlnG ` G ) ( ( X L Y ) C_ h /\ ( Z L W ) C_ h ) /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) ) ) ) ) with typecode |-
27	13 24 26	3bitr4rd	Could not format ( ph -> ( ( X L Y ) .|| ( Z L W ) <-> ( E. h e. ran ( PlnG ` G ) ( ( X L Y ) C_ h /\ ( Z L W ) C_ h ) /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) ) ) : No typesetting found for |- ( ph -> ( ( X L Y ) .|| ( Z L W ) <-> ( E. h e. ran ( PlnG ` G ) ( ( X L Y ) C_ h /\ ( Z L W ) C_ h ) /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) ) ) with typecode |-
28	4	ad4antr	Could not format ( ( ( ( ( ph /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) /\ h e. ran ( PlnG ` G ) ) /\ ( X L Y ) C_ h ) /\ ( Z L W ) C_ h ) -> G e. TarskiG ) : No typesetting found for |- ( ( ( ( ( ph /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) /\ h e. ran ( PlnG ` G ) ) /\ ( X L Y ) C_ h ) /\ ( Z L W ) C_ h ) -> G e. TarskiG ) with typecode |-
29		simpllr	Could not format ( ( ( ( ( ph /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) /\ h e. ran ( PlnG ` G ) ) /\ ( X L Y ) C_ h ) /\ ( Z L W ) C_ h ) -> h e. ran ( PlnG ` G ) ) : No typesetting found for |- ( ( ( ( ( ph /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) /\ h e. ran ( PlnG ` G ) ) /\ ( X L Y ) C_ h ) /\ ( Z L W ) C_ h ) -> h e. ran ( PlnG ` G ) ) with typecode |-
30		simplr	Could not format ( ( ( ( ( ph /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) /\ h e. ran ( PlnG ` G ) ) /\ ( X L Y ) C_ h ) /\ ( Z L W ) C_ h ) -> ( X L Y ) C_ h ) : No typesetting found for |- ( ( ( ( ( ph /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) /\ h e. ran ( PlnG ` G ) ) /\ ( X L Y ) C_ h ) /\ ( Z L W ) C_ h ) -> ( X L Y ) C_ h ) with typecode |-
31		simpr	Could not format ( ( ( ( ( ph /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) /\ h e. ran ( PlnG ` G ) ) /\ ( X L Y ) C_ h ) /\ ( Z L W ) C_ h ) -> ( Z L W ) C_ h ) : No typesetting found for |- ( ( ( ( ( ph /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) /\ h e. ran ( PlnG ` G ) ) /\ ( X L Y ) C_ h ) /\ ( Z L W ) C_ h ) -> ( Z L W ) C_ h ) with typecode |-
32		rspe	Could not format ( ( h e. ran ( PlnG ` G ) /\ ( ( X L Y ) C_ h /\ ( Z L W ) C_ h ) ) -> E. h e. ran ( PlnG ` G ) ( ( X L Y ) C_ h /\ ( Z L W ) C_ h ) ) : No typesetting found for |- ( ( h e. ran ( PlnG ` G ) /\ ( ( X L Y ) C_ h /\ ( Z L W ) C_ h ) ) -> E. h e. ran ( PlnG ` G ) ( ( X L Y ) C_ h /\ ( Z L W ) C_ h ) ) with typecode |-
33	29 30 31 32	syl12anc	Could not format ( ( ( ( ( ph /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) /\ h e. ran ( PlnG ` G ) ) /\ ( X L Y ) C_ h ) /\ ( Z L W ) C_ h ) -> E. h e. ran ( PlnG ` G ) ( ( X L Y ) C_ h /\ ( Z L W ) C_ h ) ) : No typesetting found for |- ( ( ( ( ( ph /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) /\ h e. ran ( PlnG ` G ) ) /\ ( X L Y ) C_ h ) /\ ( Z L W ) C_ h ) -> E. h e. ran ( PlnG ` G ) ( ( X L Y ) C_ h /\ ( Z L W ) C_ h ) ) with typecode |-
34		simp-4r	Could not format ( ( ( ( ( ph /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) /\ h e. ran ( PlnG ` G ) ) /\ ( X L Y ) C_ h ) /\ ( Z L W ) C_ h ) -> ( ( X L Y ) i^i ( Z L W ) ) = (/) ) : No typesetting found for |- ( ( ( ( ( ph /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) /\ h e. ran ( PlnG ` G ) ) /\ ( X L Y ) C_ h ) /\ ( Z L W ) C_ h ) -> ( ( X L Y ) i^i ( Z L W ) ) = (/) ) with typecode |-
35	27	ad4antr	Could not format ( ( ( ( ( ph /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) /\ h e. ran ( PlnG ` G ) ) /\ ( X L Y ) C_ h ) /\ ( Z L W ) C_ h ) -> ( ( X L Y ) .|| ( Z L W ) <-> ( E. h e. ran ( PlnG ` G ) ( ( X L Y ) C_ h /\ ( Z L W ) C_ h ) /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) ) ) : No typesetting found for |- ( ( ( ( ( ph /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) /\ h e. ran ( PlnG ` G ) ) /\ ( X L Y ) C_ h ) /\ ( Z L W ) C_ h ) -> ( ( X L Y ) .|| ( Z L W ) <-> ( E. h e. ran ( PlnG ` G ) ( ( X L Y ) C_ h /\ ( Z L W ) C_ h ) /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) ) ) with typecode |-
36	33 34 35	mpbir2and	Could not format ( ( ( ( ( ph /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) /\ h e. ran ( PlnG ` G ) ) /\ ( X L Y ) C_ h ) /\ ( Z L W ) C_ h ) -> ( X L Y ) .|| ( Z L W ) ) : No typesetting found for |- ( ( ( ( ( ph /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) /\ h e. ran ( PlnG ` G ) ) /\ ( X L Y ) C_ h ) /\ ( Z L W ) C_ h ) -> ( X L Y ) .|| ( Z L W ) ) with typecode |-
37	9	ad4antr	Could not format ( ( ( ( ( ph /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) /\ h e. ran ( PlnG ` G ) ) /\ ( X L Y ) C_ h ) /\ ( Z L W ) C_ h ) -> ( X L Y ) =/= ( Z L W ) ) : No typesetting found for |- ( ( ( ( ( ph /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) /\ h e. ran ( PlnG ` G ) ) /\ ( X L Y ) C_ h ) /\ ( Z L W ) C_ h ) -> ( X L Y ) =/= ( Z L W ) ) with typecode |-
38	1 14 2 4 7 19 21	tglinerflx1	$$⊢\phi \to Z\in \left(ZLW\right)$$
39	38	ad4antr	Could not format ( ( ( ( ( ph /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) /\ h e. ran ( PlnG ` G ) ) /\ ( X L Y ) C_ h ) /\ ( Z L W ) C_ h ) -> Z e. ( Z L W ) ) : No typesetting found for |- ( ( ( ( ( ph /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) /\ h e. ran ( PlnG ` G ) ) /\ ( X L Y ) C_ h ) /\ ( Z L W ) C_ h ) -> Z e. ( Z L W ) ) with typecode |-
40	1 14 2 4 7 19 21	tglinerflx2	$$⊢\phi \to W\in \left(ZLW\right)$$
41	40	ad4antr	Could not format ( ( ( ( ( ph /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) /\ h e. ran ( PlnG ` G ) ) /\ ( X L Y ) C_ h ) /\ ( Z L W ) C_ h ) -> W e. ( Z L W ) ) : No typesetting found for |- ( ( ( ( ( ph /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) /\ h e. ran ( PlnG ` G ) ) /\ ( X L Y ) C_ h ) /\ ( Z L W ) C_ h ) -> W e. ( Z L W ) ) with typecode |-
42	2 25 3 28 36 37 39 41	prlnghpg	Could not format ( ( ( ( ( ph /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) /\ h e. ran ( PlnG ` G ) ) /\ ( X L Y ) C_ h ) /\ ( Z L W ) C_ h ) -> Z ( ( hpG ` G ) ` ( X L Y ) ) W ) : No typesetting found for |- ( ( ( ( ( ph /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) /\ h e. ran ( PlnG ` G ) ) /\ ( X L Y ) C_ h ) /\ ( Z L W ) C_ h ) -> Z ( ( hpG ` G ) ` ( X L Y ) ) W ) with typecode |-
43	42	anasss	Could not format ( ( ( ( ph /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) /\ h e. ran ( PlnG ` G ) ) /\ ( ( X L Y ) C_ h /\ ( Z L W ) C_ h ) ) -> Z ( ( hpG ` G ) ` ( X L Y ) ) W ) : No typesetting found for |- ( ( ( ( ph /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) /\ h e. ran ( PlnG ` G ) ) /\ ( ( X L Y ) C_ h /\ ( Z L W ) C_ h ) ) -> Z ( ( hpG ` G ) ` ( X L Y ) ) W ) with typecode |-
44	43	r19.29an	Could not format ( ( ( ph /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) /\ E. h e. ran ( PlnG ` G ) ( ( X L Y ) C_ h /\ ( Z L W ) C_ h ) ) -> Z ( ( hpG ` G ) ` ( X L Y ) ) W ) : No typesetting found for |- ( ( ( ph /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) /\ E. h e. ran ( PlnG ` G ) ( ( X L Y ) C_ h /\ ( Z L W ) C_ h ) ) -> Z ( ( hpG ` G ) ` ( X L Y ) ) W ) with typecode |-
45		sseq2	Could not format ( h = ( ( X L Y ) ( PlnG ` G ) W ) -> ( ( X L Y ) C_ h <-> ( X L Y ) C_ ( ( X L Y ) ( PlnG ` G ) W ) ) ) : No typesetting found for |- ( h = ( ( X L Y ) ( PlnG ` G ) W ) -> ( ( X L Y ) C_ h <-> ( X L Y ) C_ ( ( X L Y ) ( PlnG ` G ) W ) ) ) with typecode |-
46		sseq2	Could not format ( h = ( ( X L Y ) ( PlnG ` G ) W ) -> ( ( Z L W ) C_ h <-> ( Z L W ) C_ ( ( X L Y ) ( PlnG ` G ) W ) ) ) : No typesetting found for |- ( h = ( ( X L Y ) ( PlnG ` G ) W ) -> ( ( Z L W ) C_ h <-> ( Z L W ) C_ ( ( X L Y ) ( PlnG ` G ) W ) ) ) with typecode |-
47	45 46	anbi12d	Could not format ( h = ( ( X L Y ) ( PlnG ` G ) W ) -> ( ( ( X L Y ) C_ h /\ ( Z L W ) C_ h ) <-> ( ( X L Y ) C_ ( ( X L Y ) ( PlnG ` G ) W ) /\ ( Z L W ) C_ ( ( X L Y ) ( PlnG ` G ) W ) ) ) ) : No typesetting found for |- ( h = ( ( X L Y ) ( PlnG ` G ) W ) -> ( ( ( X L Y ) C_ h /\ ( Z L W ) C_ h ) <-> ( ( X L Y ) C_ ( ( X L Y ) ( PlnG ` G ) W ) /\ ( Z L W ) C_ ( ( X L Y ) ( PlnG ` G ) W ) ) ) ) with typecode |-
48	4	ad2antrr	$$⊢\left(\left(\phi \wedge \left(XLY\right)\cap \left(ZLW\right)=\varnothing \right)\wedge Z{hp}_{𝒢}\left(G\right)\left(XLY\right)W\right)\to G\in {𝒢}_{\mathrm{Tarski}}$$
49	18	ad2antrr	$$⊢\left(\left(\phi \wedge \left(XLY\right)\cap \left(ZLW\right)=\varnothing \right)\wedge Z{hp}_{𝒢}\left(G\right)\left(XLY\right)W\right)\to XLY\in \mathrm{ran}L$$
50	19	ad2antrr	$$⊢\left(\left(\phi \wedge \left(XLY\right)\cap \left(ZLW\right)=\varnothing \right)\wedge Z{hp}_{𝒢}\left(G\right)\left(XLY\right)W\right)\to W\in P$$
51		nel02	$$⊢\left(XLY\right)\cap \left(ZLW\right)=\varnothing \to \neg W\in \left(\left(XLY\right)\cap \left(ZLW\right)\right)$$
52	51	ad2antlr	$$⊢\left(\left(\phi \wedge \left(XLY\right)\cap \left(ZLW\right)=\varnothing \right)\wedge Z{hp}_{𝒢}\left(G\right)\left(XLY\right)W\right)\to \neg W\in \left(\left(XLY\right)\cap \left(ZLW\right)\right)$$
53		simpr	$$⊢\left(\left(\left(\phi \wedge \left(XLY\right)\cap \left(ZLW\right)=\varnothing \right)\wedge Z{hp}_{𝒢}\left(G\right)\left(XLY\right)W\right)\wedge W\in \left(XLY\right)\right)\to W\in \left(XLY\right)$$
54	40	ad3antrrr	$$⊢\left(\left(\left(\phi \wedge \left(XLY\right)\cap \left(ZLW\right)=\varnothing \right)\wedge Z{hp}_{𝒢}\left(G\right)\left(XLY\right)W\right)\wedge W\in \left(XLY\right)\right)\to W\in \left(ZLW\right)$$
55	53 54	elind	$$⊢\left(\left(\left(\phi \wedge \left(XLY\right)\cap \left(ZLW\right)=\varnothing \right)\wedge Z{hp}_{𝒢}\left(G\right)\left(XLY\right)W\right)\wedge W\in \left(XLY\right)\right)\to W\in \left(\left(XLY\right)\cap \left(ZLW\right)\right)$$
56	52 55	mtand	$$⊢\left(\left(\phi \wedge \left(XLY\right)\cap \left(ZLW\right)=\varnothing \right)\wedge Z{hp}_{𝒢}\left(G\right)\left(XLY\right)W\right)\to \neg W\in \left(XLY\right)$$
57	50 56	eldifd	$$⊢\left(\left(\phi \wedge \left(XLY\right)\cap \left(ZLW\right)=\varnothing \right)\wedge Z{hp}_{𝒢}\left(G\right)\left(XLY\right)W\right)\to W\in \left(P\setminus \left(XLY\right)\right)$$
58	1 2 25 48 49 57	tgelrnpln	Could not format ( ( ( ph /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) /\ Z ( ( hpG ` G ) ` ( X L Y ) ) W ) -> ( ( X L Y ) ( PlnG ` G ) W ) e. ran ( PlnG ` G ) ) : No typesetting found for |- ( ( ( ph /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) /\ Z ( ( hpG ` G ) ` ( X L Y ) ) W ) -> ( ( X L Y ) ( PlnG ` G ) W ) e. ran ( PlnG ` G ) ) with typecode |-
59	1 14 2 25 48 49 57	elplnglnid	Could not format ( ( ( ph /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) /\ Z ( ( hpG ` G ) ` ( X L Y ) ) W ) -> ( X L Y ) C_ ( ( X L Y ) ( PlnG ` G ) W ) ) : No typesetting found for |- ( ( ( ph /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) /\ Z ( ( hpG ` G ) ` ( X L Y ) ) W ) -> ( X L Y ) C_ ( ( X L Y ) ( PlnG ` G ) W ) ) with typecode |-
60	7	ad2antrr	$$⊢\left(\left(\phi \wedge \left(XLY\right)\cap \left(ZLW\right)=\varnothing \right)\wedge Z{hp}_{𝒢}\left(G\right)\left(XLY\right)W\right)\to Z\in P$$
61		simpr	$$⊢\left(\left(\phi \wedge \left(XLY\right)\cap \left(ZLW\right)=\varnothing \right)\wedge Z{hp}_{𝒢}\left(G\right)\left(XLY\right)W\right)\to Z{hp}_{𝒢}\left(G\right)\left(XLY\right)W$$
62	1 2 25 49 60 57 48 61	hpgssplng	Could not format ( ( ( ph /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) /\ Z ( ( hpG ` G ) ` ( X L Y ) ) W ) -> Z e. ( ( X L Y ) ( PlnG ` G ) W ) ) : No typesetting found for |- ( ( ( ph /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) /\ Z ( ( hpG ` G ) ` ( X L Y ) ) W ) -> Z e. ( ( X L Y ) ( PlnG ` G ) W ) ) with typecode |-
63	1 14 2 25 48 49 57	elplngid	Could not format ( ( ( ph /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) /\ Z ( ( hpG ` G ) ` ( X L Y ) ) W ) -> W e. ( ( X L Y ) ( PlnG ` G ) W ) ) : No typesetting found for |- ( ( ( ph /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) /\ Z ( ( hpG ` G ) ` ( X L Y ) ) W ) -> W e. ( ( X L Y ) ( PlnG ` G ) W ) ) with typecode |-
64	21	ad2antrr	$$⊢\left(\left(\phi \wedge \left(XLY\right)\cap \left(ZLW\right)=\varnothing \right)\wedge Z{hp}_{𝒢}\left(G\right)\left(XLY\right)W\right)\to Z\ne W$$
65	1 14 2 25 48 58 62 63 64	lnssplng1	Could not format ( ( ( ph /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) /\ Z ( ( hpG ` G ) ` ( X L Y ) ) W ) -> ( Z L W ) C_ ( ( X L Y ) ( PlnG ` G ) W ) ) : No typesetting found for |- ( ( ( ph /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) /\ Z ( ( hpG ` G ) ` ( X L Y ) ) W ) -> ( Z L W ) C_ ( ( X L Y ) ( PlnG ` G ) W ) ) with typecode |-
66	59 65	jca	Could not format ( ( ( ph /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) /\ Z ( ( hpG ` G ) ` ( X L Y ) ) W ) -> ( ( X L Y ) C_ ( ( X L Y ) ( PlnG ` G ) W ) /\ ( Z L W ) C_ ( ( X L Y ) ( PlnG ` G ) W ) ) ) : No typesetting found for |- ( ( ( ph /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) /\ Z ( ( hpG ` G ) ` ( X L Y ) ) W ) -> ( ( X L Y ) C_ ( ( X L Y ) ( PlnG ` G ) W ) /\ ( Z L W ) C_ ( ( X L Y ) ( PlnG ` G ) W ) ) ) with typecode |-
67	47 58 66	rspcedvdw	Could not format ( ( ( ph /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) /\ Z ( ( hpG ` G ) ` ( X L Y ) ) W ) -> E. h e. ran ( PlnG ` G ) ( ( X L Y ) C_ h /\ ( Z L W ) C_ h ) ) : No typesetting found for |- ( ( ( ph /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) /\ Z ( ( hpG ` G ) ` ( X L Y ) ) W ) -> E. h e. ran ( PlnG ` G ) ( ( X L Y ) C_ h /\ ( Z L W ) C_ h ) ) with typecode |-
68	44 67	impbida	Could not format ( ( ph /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) -> ( E. h e. ran ( PlnG ` G ) ( ( X L Y ) C_ h /\ ( Z L W ) C_ h ) <-> Z ( ( hpG ` G ) ` ( X L Y ) ) W ) ) : No typesetting found for |- ( ( ph /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) -> ( E. h e. ran ( PlnG ` G ) ( ( X L Y ) C_ h /\ ( Z L W ) C_ h ) <-> Z ( ( hpG ` G ) ` ( X L Y ) ) W ) ) with typecode |-
69	68	pm5.32da	Could not format ( ph -> ( ( ( ( X L Y ) i^i ( Z L W ) ) = (/) /\ E. h e. ran ( PlnG ` G ) ( ( X L Y ) C_ h /\ ( Z L W ) C_ h ) ) <-> ( ( ( X L Y ) i^i ( Z L W ) ) = (/) /\ Z ( ( hpG ` G ) ` ( X L Y ) ) W ) ) ) : No typesetting found for |- ( ph -> ( ( ( ( X L Y ) i^i ( Z L W ) ) = (/) /\ E. h e. ran ( PlnG ` G ) ( ( X L Y ) C_ h /\ ( Z L W ) C_ h ) ) <-> ( ( ( X L Y ) i^i ( Z L W ) ) = (/) /\ Z ( ( hpG ` G ) ` ( X L Y ) ) W ) ) ) with typecode |-
70		ancom	Could not format ( ( ( ( X L Y ) i^i ( Z L W ) ) = (/) /\ E. h e. ran ( PlnG ` G ) ( ( X L Y ) C_ h /\ ( Z L W ) C_ h ) ) <-> ( E. h e. ran ( PlnG ` G ) ( ( X L Y ) C_ h /\ ( Z L W ) C_ h ) /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) ) : No typesetting found for |- ( ( ( ( X L Y ) i^i ( Z L W ) ) = (/) /\ E. h e. ran ( PlnG ` G ) ( ( X L Y ) C_ h /\ ( Z L W ) C_ h ) ) <-> ( E. h e. ran ( PlnG ` G ) ( ( X L Y ) C_ h /\ ( Z L W ) C_ h ) /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) ) with typecode |-
71		ancom	$$⊢\left(\left(XLY\right)\cap \left(ZLW\right)=\varnothing \wedge Z{hp}_{𝒢}\left(G\right)\left(XLY\right)W\right)\leftrightarrow \left(Z{hp}_{𝒢}\left(G\right)\left(XLY\right)W\wedge \left(XLY\right)\cap \left(ZLW\right)=\varnothing \right)$$
72	69 70 71	3bitr3g	Could not format ( ph -> ( ( E. h e. ran ( PlnG ` G ) ( ( X L Y ) C_ h /\ ( Z L W ) C_ h ) /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) <-> ( Z ( ( hpG ` G ) ` ( X L Y ) ) W /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) ) ) : No typesetting found for |- ( ph -> ( ( E. h e. ran ( PlnG ` G ) ( ( X L Y ) C_ h /\ ( Z L W ) C_ h ) /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) <-> ( Z ( ( hpG ` G ) ` ( X L Y ) ) W /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) ) ) with typecode |-
73	27 72	bitrd	$$⊢\phi \to \left(\left(XLY\right)\underset{\dot{}}{\parallel }\left(ZLW\right)\leftrightarrow \left(Z{hp}_{𝒢}\left(G\right)\left(XLY\right)W\wedge \left(XLY\right)\cap \left(ZLW\right)=\varnothing \right)\right)$$