outpasch

Description: Axiom of Pasch, outer form. This was proven by Gupta from other axioms and is therefore presented as Theorem 9.6 in Schwabhauser p. 70. (Contributed by Thierry Arnoux, 16-Aug-2020)

	Ref	Expression
Hypotheses	outpasch.p	$⊢ P = {Base}_{G}$
	outpasch.i	$⊢ I = Itv (G)$
	outpasch.l	$⊢ L = {Line}_{𝒢} (G)$
	outpasch.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	outpasch.a	$⊢ φ \to A \in P$
	outpasch.b	$⊢ φ \to B \in P$
	outpasch.c	$⊢ φ \to C \in P$
	outpasch.r	$⊢ φ \to R \in P$
	outpasch.q	$⊢ φ \to Q \in P$
	outpasch.1	$⊢ φ \to C \in (A I R)$
	outpasch.2	$⊢ φ \to Q \in (B I C)$
Assertion	outpasch	$⊢ φ \to \exists x \in P (x \in (A I B) \land Q \in (R I x))$

Proof

Step	Hyp	Ref	Expression
1		outpasch.p	$⊢ P = {Base}_{G}$
2		outpasch.i	$⊢ I = Itv (G)$
3		outpasch.l	$⊢ L = {Line}_{𝒢} (G)$
4		outpasch.g	$⊢ φ \to G \in 𝒢_{Tarski}$
5		outpasch.a	$⊢ φ \to A \in P$
6		outpasch.b	$⊢ φ \to B \in P$
7		outpasch.c	$⊢ φ \to C \in P$
8		outpasch.r	$⊢ φ \to R \in P$
9		outpasch.q	$⊢ φ \to Q \in P$
10		outpasch.1	$⊢ φ \to C \in (A I R)$
11		outpasch.2	$⊢ φ \to Q \in (B I C)$
12	5	adantr	$⊢ (φ \land Q \in (R I C)) \to A \in P$
13		simpr	$⊢ ((φ \land Q \in (R I C)) \land x = A) \to x = A$
14	13	eleq1d	$⊢ ((φ \land Q \in (R I C)) \land x = A) \to (x \in (A I B) \leftrightarrow A \in (A I B))$
15	13	oveq2d	$⊢ ((φ \land Q \in (R I C)) \land x = A) \to R I x = R I A$
16	15	eleq2d	$⊢ ((φ \land Q \in (R I C)) \land x = A) \to (Q \in (R I x) \leftrightarrow Q \in (R I A))$
17	14 16	anbi12d	$⊢ ((φ \land Q \in (R I C)) \land x = A) \to ((x \in (A I B) \land Q \in (R I x)) \leftrightarrow (A \in (A I B) \land Q \in (R I A)))$
18		eqid	$⊢ dist (G) = dist (G)$
19	1 18 2 4 5 6	tgbtwntriv1	$⊢ φ \to A \in (A I B)$
20	19	adantr	$⊢ (φ \land Q \in (R I C)) \to A \in (A I B)$
21	4	adantr	$⊢ (φ \land Q \in (R I C)) \to G \in 𝒢_{Tarski}$
22	8	adantr	$⊢ (φ \land Q \in (R I C)) \to R \in P$
23	9	adantr	$⊢ (φ \land Q \in (R I C)) \to Q \in P$
24	7	adantr	$⊢ (φ \land Q \in (R I C)) \to C \in P$
25		simpr	$⊢ (φ \land Q \in (R I C)) \to Q \in (R I C)$
26	1 18 2 4 5 7 8 10	tgbtwncom	$⊢ φ \to C \in (R I A)$
27	26	adantr	$⊢ (φ \land Q \in (R I C)) \to C \in (R I A)$
28	1 18 2 21 22 23 24 12 25 27	tgbtwnexch	$⊢ (φ \land Q \in (R I C)) \to Q \in (R I A)$
29	20 28	jca	$⊢ (φ \land Q \in (R I C)) \to (A \in (A I B) \land Q \in (R I A))$
30	12 17 29	rspcedvd	$⊢ (φ \land Q \in (R I C)) \to \exists x \in P (x \in (A I B) \land Q \in (R I x))$
31	30	adantlr	$⊢ ((φ \land (R \in (Q L C) \lor Q = C)) \land Q \in (R I C)) \to \exists x \in P (x \in (A I B) \land Q \in (R I x))$
32	6	ad2antrr	$⊢ ((φ \land (R \in (Q L C) \lor Q = C)) \land \neg Q \in (R I C)) \to B \in P$
33		eleq1	$⊢ x = B \to (x \in (A I B) \leftrightarrow B \in (A I B))$
34		oveq2	$⊢ x = B \to R I x = R I B$
35	34	eleq2d	$⊢ x = B \to (Q \in (R I x) \leftrightarrow Q \in (R I B))$
36	33 35	anbi12d	$⊢ x = B \to ((x \in (A I B) \land Q \in (R I x)) \leftrightarrow (B \in (A I B) \land Q \in (R I B)))$
37	36	adantl	$⊢ (((φ \land (R \in (Q L C) \lor Q = C)) \land \neg Q \in (R I C)) \land x = B) \to ((x \in (A I B) \land Q \in (R I x)) \leftrightarrow (B \in (A I B) \land Q \in (R I B)))$
38	1 18 2 4 5 6	tgbtwntriv2	$⊢ φ \to B \in (A I B)$
39	38	ad2antrr	$⊢ ((φ \land (R \in (Q L C) \lor Q = C)) \land \neg Q \in (R I C)) \to B \in (A I B)$
40	4	ad3antrrr	$⊢ (((φ \land (R \in (Q L C) \lor Q = C)) \land \neg Q \in (R I C)) \land R \in (Q I C)) \to G \in 𝒢_{Tarski}$
41	7	ad3antrrr	$⊢ (((φ \land (R \in (Q L C) \lor Q = C)) \land \neg Q \in (R I C)) \land R \in (Q I C)) \to C \in P$
42	8	ad3antrrr	$⊢ (((φ \land (R \in (Q L C) \lor Q = C)) \land \neg Q \in (R I C)) \land R \in (Q I C)) \to R \in P$
43	9	ad3antrrr	$⊢ (((φ \land (R \in (Q L C) \lor Q = C)) \land \neg Q \in (R I C)) \land R \in (Q I C)) \to Q \in P$
44	6	ad3antrrr	$⊢ (((φ \land (R \in (Q L C) \lor Q = C)) \land \neg Q \in (R I C)) \land R \in (Q I C)) \to B \in P$
45		simpr	$⊢ (((φ \land (R \in (Q L C) \lor Q = C)) \land \neg Q \in (R I C)) \land R \in (Q I C)) \to R \in (Q I C)$
46	1 18 2 40 43 42 41 45	tgbtwncom	$⊢ (((φ \land (R \in (Q L C) \lor Q = C)) \land \neg Q \in (R I C)) \land R \in (Q I C)) \to R \in (C I Q)$
47	1 18 2 4 6 9 7 11	tgbtwncom	$⊢ φ \to Q \in (C I B)$
48	47	ad3antrrr	$⊢ (((φ \land (R \in (Q L C) \lor Q = C)) \land \neg Q \in (R I C)) \land R \in (Q I C)) \to Q \in (C I B)$
49	1 18 2 40 41 42 43 44 46 48	tgbtwnexch3	$⊢ (((φ \land (R \in (Q L C) \lor Q = C)) \land \neg Q \in (R I C)) \land R \in (Q I C)) \to Q \in (R I B)$
50	4	ad3antrrr	$⊢ (((φ \land (R \in (Q L C) \lor Q = C)) \land \neg Q \in (R I C)) \land C \in (Q I R)) \to G \in 𝒢_{Tarski}$
51	6	ad3antrrr	$⊢ (((φ \land (R \in (Q L C) \lor Q = C)) \land \neg Q \in (R I C)) \land C \in (Q I R)) \to B \in P$
52	9	ad3antrrr	$⊢ (((φ \land (R \in (Q L C) \lor Q = C)) \land \neg Q \in (R I C)) \land C \in (Q I R)) \to Q \in P$
53	8	ad3antrrr	$⊢ (((φ \land (R \in (Q L C) \lor Q = C)) \land \neg Q \in (R I C)) \land C \in (Q I R)) \to R \in P$
54	7	ad3antrrr	$⊢ (((φ \land (R \in (Q L C) \lor Q = C)) \land \neg Q \in (R I C)) \land C \in (Q I R)) \to C \in P$
55		simpr	$⊢ ((((φ \land (R \in (Q L C) \lor Q = C)) \land \neg Q \in (R I C)) \land C \in (Q I R)) \land Q = C) \to Q = C$
56	1 18 2 4 8 7	tgbtwntriv2	$⊢ φ \to C \in (R I C)$
57	56	ad4antr	$⊢ ((((φ \land (R \in (Q L C) \lor Q = C)) \land \neg Q \in (R I C)) \land C \in (Q I R)) \land Q = C) \to C \in (R I C)$
58	55 57	eqeltrd	$⊢ ((((φ \land (R \in (Q L C) \lor Q = C)) \land \neg Q \in (R I C)) \land C \in (Q I R)) \land Q = C) \to Q \in (R I C)$
59		simpllr	$⊢ ((((φ \land (R \in (Q L C) \lor Q = C)) \land \neg Q \in (R I C)) \land C \in (Q I R)) \land Q = C) \to \neg Q \in (R I C)$
60	58 59	pm2.65da	$⊢ (((φ \land (R \in (Q L C) \lor Q = C)) \land \neg Q \in (R I C)) \land C \in (Q I R)) \to \neg Q = C$
61	60	neqned	$⊢ (((φ \land (R \in (Q L C) \lor Q = C)) \land \neg Q \in (R I C)) \land C \in (Q I R)) \to Q \neq C$
62	11	ad3antrrr	$⊢ (((φ \land (R \in (Q L C) \lor Q = C)) \land \neg Q \in (R I C)) \land C \in (Q I R)) \to Q \in (B I C)$
63		simpr	$⊢ (((φ \land (R \in (Q L C) \lor Q = C)) \land \neg Q \in (R I C)) \land C \in (Q I R)) \to C \in (Q I R)$
64	1 18 2 50 51 52 54 53 61 62 63	tgbtwnouttr	$⊢ (((φ \land (R \in (Q L C) \lor Q = C)) \land \neg Q \in (R I C)) \land C \in (Q I R)) \to Q \in (B I R)$
65	1 18 2 50 51 52 53 64	tgbtwncom	$⊢ (((φ \land (R \in (Q L C) \lor Q = C)) \land \neg Q \in (R I C)) \land C \in (Q I R)) \to Q \in (R I B)$
66	1 3 2 4 9 7 8	tgcolg	$⊢ φ \to ((R \in (Q L C) \lor Q = C) \leftrightarrow (R \in (Q I C) \lor Q \in (R I C) \lor C \in (Q I R)))$
67	66	biimpa	$⊢ (φ \land (R \in (Q L C) \lor Q = C)) \to (R \in (Q I C) \lor Q \in (R I C) \lor C \in (Q I R))$
68		3orcoma	$⊢ (Q \in (R I C) \lor R \in (Q I C) \lor C \in (Q I R)) \leftrightarrow (R \in (Q I C) \lor Q \in (R I C) \lor C \in (Q I R))$
69		3orass	$⊢ (Q \in (R I C) \lor R \in (Q I C) \lor C \in (Q I R)) \leftrightarrow (Q \in (R I C) \lor (R \in (Q I C) \lor C \in (Q I R)))$
70	68 69	bitr3i	$⊢ (R \in (Q I C) \lor Q \in (R I C) \lor C \in (Q I R)) \leftrightarrow (Q \in (R I C) \lor (R \in (Q I C) \lor C \in (Q I R)))$
71	67 70	sylib	$⊢ (φ \land (R \in (Q L C) \lor Q = C)) \to (Q \in (R I C) \lor (R \in (Q I C) \lor C \in (Q I R)))$
72	71	orcanai	$⊢ ((φ \land (R \in (Q L C) \lor Q = C)) \land \neg Q \in (R I C)) \to (R \in (Q I C) \lor C \in (Q I R))$
73	49 65 72	mpjaodan	$⊢ ((φ \land (R \in (Q L C) \lor Q = C)) \land \neg Q \in (R I C)) \to Q \in (R I B)$
74	39 73	jca	$⊢ ((φ \land (R \in (Q L C) \lor Q = C)) \land \neg Q \in (R I C)) \to (B \in (A I B) \land Q \in (R I B))$
75	32 37 74	rspcedvd	$⊢ ((φ \land (R \in (Q L C) \lor Q = C)) \land \neg Q \in (R I C)) \to \exists x \in P (x \in (A I B) \land Q \in (R I x))$
76	31 75	pm2.61dan	$⊢ (φ \land (R \in (Q L C) \lor Q = C)) \to \exists x \in P (x \in (A I B) \land Q \in (R I x))$
77	6	ad2antrr	$⊢ ((φ \land \neg (R \in (Q L C) \lor Q = C)) \land B \in (R L Q)) \to B \in P$
78	36	adantl	$⊢ (((φ \land \neg (R \in (Q L C) \lor Q = C)) \land B \in (R L Q)) \land x = B) \to ((x \in (A I B) \land Q \in (R I x)) \leftrightarrow (B \in (A I B) \land Q \in (R I B)))$
79	38	ad2antrr	$⊢ ((φ \land \neg (R \in (Q L C) \lor Q = C)) \land B \in (R L Q)) \to B \in (A I B)$
80	4	ad2antrr	$⊢ ((φ \land \neg (R \in (Q L C) \lor Q = C)) \land B \in (R L Q)) \to G \in 𝒢_{Tarski}$
81	8	ad2antrr	$⊢ ((φ \land \neg (R \in (Q L C) \lor Q = C)) \land B \in (R L Q)) \to R \in P$
82	9	ad2antrr	$⊢ ((φ \land \neg (R \in (Q L C) \lor Q = C)) \land B \in (R L Q)) \to Q \in P$
83	7	ad2antrr	$⊢ ((φ \land \neg (R \in (Q L C) \lor Q = C)) \land B \in (R L Q)) \to C \in P$
84		simplr	$⊢ ((φ \land \neg (R \in (Q L C) \lor Q = C)) \land B \in (R L Q)) \to \neg (R \in (Q L C) \lor Q = C)$
85		simpr	$⊢ ((φ \land \neg (R \in (Q L C) \lor Q = C)) \land B \in (R L Q)) \to B \in (R L Q)$
86	4	adantr	$⊢ (φ \land \neg (R \in (Q L C) \lor Q = C)) \to G \in 𝒢_{Tarski}$
87	8	adantr	$⊢ (φ \land \neg (R \in (Q L C) \lor Q = C)) \to R \in P$
88	9	adantr	$⊢ (φ \land \neg (R \in (Q L C) \lor Q = C)) \to Q \in P$
89	7	adantr	$⊢ (φ \land \neg (R \in (Q L C) \lor Q = C)) \to C \in P$
90		simpr	$⊢ (φ \land \neg (R \in (Q L C) \lor Q = C)) \to \neg (R \in (Q L C) \lor Q = C)$
91	1 2 3 86 87 88 89 90	ncolne1	$⊢ (φ \land \neg (R \in (Q L C) \lor Q = C)) \to R \neq Q$
92	1 2 3 86 87 88 91	tglinerflx2	$⊢ (φ \land \neg (R \in (Q L C) \lor Q = C)) \to Q \in (R L Q)$
93	92	adantr	$⊢ ((φ \land \neg (R \in (Q L C) \lor Q = C)) \land B \in (R L Q)) \to Q \in (R L Q)$
94	1 3 2 86 88 89 87 90	ncolcom	$⊢ (φ \land \neg (R \in (Q L C) \lor Q = C)) \to \neg (R \in (C L Q) \lor C = Q)$
95	1 3 2 86 89 88 87 94	ncolrot1	$⊢ (φ \land \neg (R \in (Q L C) \lor Q = C)) \to \neg (C \in (Q L R) \lor Q = R)$
96	1 2 3 86 89 88 87 95	ncolne1	$⊢ (φ \land \neg (R \in (Q L C) \lor Q = C)) \to C \neq Q$
97	96	adantr	$⊢ ((φ \land \neg (R \in (Q L C) \lor Q = C)) \land B \in (R L Q)) \to C \neq Q$
98	47	ad2antrr	$⊢ ((φ \land \neg (R \in (Q L C) \lor Q = C)) \land B \in (R L Q)) \to Q \in (C I B)$
99	1 2 3 80 83 82 77 97 98	btwnlng3	$⊢ ((φ \land \neg (R \in (Q L C) \lor Q = C)) \land B \in (R L Q)) \to B \in (C L Q)$
100	1 2 3 80 83 82 97	tglinerflx2	$⊢ ((φ \land \neg (R \in (Q L C) \lor Q = C)) \land B \in (R L Q)) \to Q \in (C L Q)$
101	1 2 3 80 81 82 83 82 84 85 93 99 100	tglineinteq	$⊢ ((φ \land \neg (R \in (Q L C) \lor Q = C)) \land B \in (R L Q)) \to B = Q$
102	1 18 2 4 8 6	tgbtwntriv2	$⊢ φ \to B \in (R I B)$
103	102	ad2antrr	$⊢ ((φ \land \neg (R \in (Q L C) \lor Q = C)) \land B \in (R L Q)) \to B \in (R I B)$
104	101 103	eqeltrrd	$⊢ ((φ \land \neg (R \in (Q L C) \lor Q = C)) \land B \in (R L Q)) \to Q \in (R I B)$
105	79 104	jca	$⊢ ((φ \land \neg (R \in (Q L C) \lor Q = C)) \land B \in (R L Q)) \to (B \in (A I B) \land Q \in (R I B))$
106	77 78 105	rspcedvd	$⊢ ((φ \land \neg (R \in (Q L C) \lor Q = C)) \land B \in (R L Q)) \to \exists x \in P (x \in (A I B) \land Q \in (R I x))$
107		eleq1	$⊢ t = x \to (t \in (a I b) \leftrightarrow x \in (a I b))$
108	107	cbvrexvw	$⊢ \exists t \in (R L Q) t \in (a I b) \leftrightarrow \exists x \in (R L Q) x \in (a I b)$
109	108	anbi2i	$⊢ ((a \in (P ∖ (R L Q)) \land b \in (P ∖ (R L Q))) \land \exists t \in (R L Q) t \in (a I b)) \leftrightarrow ((a \in (P ∖ (R L Q)) \land b \in (P ∖ (R L Q))) \land \exists x \in (R L Q) x \in (a I b))$
110	109	opabbii	$⊢ \{⟨a, b⟩ \| ((a \in (P ∖ (R L Q)) \land b \in (P ∖ (R L Q))) \land \exists t \in (R L Q) t \in (a I b))\} = \{⟨a, b⟩ \| ((a \in (P ∖ (R L Q)) \land b \in (P ∖ (R L Q))) \land \exists x \in (R L Q) x \in (a I b))\}$
111	4	ad2antrr	$⊢ ((φ \land \neg (R \in (Q L C) \lor Q = C)) \land \neg B \in (R L Q)) \to G \in 𝒢_{Tarski}$
112	8	ad2antrr	$⊢ ((φ \land \neg (R \in (Q L C) \lor Q = C)) \land \neg B \in (R L Q)) \to R \in P$
113	9	ad2antrr	$⊢ ((φ \land \neg (R \in (Q L C) \lor Q = C)) \land \neg B \in (R L Q)) \to Q \in P$
114	91	adantr	$⊢ ((φ \land \neg (R \in (Q L C) \lor Q = C)) \land \neg B \in (R L Q)) \to R \neq Q$
115	1 2 3 111 112 113 114	tgelrnln	$⊢ ((φ \land \neg (R \in (Q L C) \lor Q = C)) \land \neg B \in (R L Q)) \to R L Q \in ran L$
116		eqid	$⊢ {hl}_{𝒢} (G) = {hl}_{𝒢} (G)$
117	7	ad2antrr	$⊢ ((φ \land \neg (R \in (Q L C) \lor Q = C)) \land \neg B \in (R L Q)) \to C \in P$
118	5	ad2antrr	$⊢ ((φ \land \neg (R \in (Q L C) \lor Q = C)) \land \neg B \in (R L Q)) \to A \in P$
119	6	ad2antrr	$⊢ ((φ \land \neg (R \in (Q L C) \lor Q = C)) \land \neg B \in (R L Q)) \to B \in P$
120	92	adantr	$⊢ ((φ \land \neg (R \in (Q L C) \lor Q = C)) \land \neg B \in (R L Q)) \to Q \in (R L Q)$
121	1 3 2 86 88 89 87 90	ncolrot2	$⊢ (φ \land \neg (R \in (Q L C) \lor Q = C)) \to \neg (C \in (R L Q) \lor R = Q)$
122		pm2.45	$⊢ \neg (C \in (R L Q) \lor R = Q) \to \neg C \in (R L Q)$
123	121 122	syl	$⊢ (φ \land \neg (R \in (Q L C) \lor Q = C)) \to \neg C \in (R L Q)$
124	123	adantr	$⊢ ((φ \land \neg (R \in (Q L C) \lor Q = C)) \land \neg B \in (R L Q)) \to \neg C \in (R L Q)$
125		simpr	$⊢ ((φ \land \neg (R \in (Q L C) \lor Q = C)) \land \neg B \in (R L Q)) \to \neg B \in (R L Q)$
126	47	ad2antrr	$⊢ ((φ \land \neg (R \in (Q L C) \lor Q = C)) \land \neg B \in (R L Q)) \to Q \in (C I B)$
127	1 18 2 110 117 119 120 124 125 126	islnoppd	$⊢ ((φ \land \neg (R \in (Q L C) \lor Q = C)) \land \neg B \in (R L Q)) \to C \{⟨a, b⟩ \| ((a \in (P ∖ (R L Q)) \land b \in (P ∖ (R L Q))) \land \exists t \in (R L Q) t \in (a I b))\} B$
128	1 2 3 86 87 88 91	tglinerflx1	$⊢ (φ \land \neg (R \in (Q L C) \lor Q = C)) \to R \in (R L Q)$
129	128	adantr	$⊢ ((φ \land \neg (R \in (Q L C) \lor Q = C)) \land \neg B \in (R L Q)) \to R \in (R L Q)$
130	26	ad2antrr	$⊢ ((φ \land \neg (R \in (Q L C) \lor Q = C)) \land \neg B \in (R L Q)) \to C \in (R I A)$
131	1 2 3 86 89 87 88 121	ncolne1	$⊢ (φ \land \neg (R \in (Q L C) \lor Q = C)) \to C \neq R$
132	131	adantr	$⊢ ((φ \land \neg (R \in (Q L C) \lor Q = C)) \land \neg B \in (R L Q)) \to C \neq R$
133	1 18 2 111 112 117 118 130 132	tgbtwnne	$⊢ ((φ \land \neg (R \in (Q L C) \lor Q = C)) \land \neg B \in (R L Q)) \to R \neq A$
134	1 2 116 112 118 117 111 118 130 133 132	btwnhl1	$⊢ ((φ \land \neg (R \in (Q L C) \lor Q = C)) \land \neg B \in (R L Q)) \to C {hl}_{𝒢} (G) (R) A$
135	1 18 2 110 3 115 111 116 117 118 119 127 129 134	opphl	$⊢ ((φ \land \neg (R \in (Q L C) \lor Q = C)) \land \neg B \in (R L Q)) \to A \{⟨a, b⟩ \| ((a \in (P ∖ (R L Q)) \land b \in (P ∖ (R L Q))) \land \exists t \in (R L Q) t \in (a I b))\} B$
136	1 18 2 110 118 119	islnopp	$⊢ ((φ \land \neg (R \in (Q L C) \lor Q = C)) \land \neg B \in (R L Q)) \to (A \{⟨a, b⟩ \| ((a \in (P ∖ (R L Q)) \land b \in (P ∖ (R L Q))) \land \exists t \in (R L Q) t \in (a I b))\} B \leftrightarrow ((\neg A \in (R L Q) \land \neg B \in (R L Q)) \land \exists x \in (R L Q) x \in (A I B)))$
137	135 136	mpbid	$⊢ ((φ \land \neg (R \in (Q L C) \lor Q = C)) \land \neg B \in (R L Q)) \to ((\neg A \in (R L Q) \land \neg B \in (R L Q)) \land \exists x \in (R L Q) x \in (A I B))$
138	137	simprd	$⊢ ((φ \land \neg (R \in (Q L C) \lor Q = C)) \land \neg B \in (R L Q)) \to \exists x \in (R L Q) x \in (A I B)$
139	111	ad2antrr	$⊢ ((((φ \land \neg (R \in (Q L C) \lor Q = C)) \land \neg B \in (R L Q)) \land x \in (R L Q)) \land x \in (A I B)) \to G \in 𝒢_{Tarski}$
140	115	ad2antrr	$⊢ ((((φ \land \neg (R \in (Q L C) \lor Q = C)) \land \neg B \in (R L Q)) \land x \in (R L Q)) \land x \in (A I B)) \to R L Q \in ran L$
141		simplr	$⊢ ((((φ \land \neg (R \in (Q L C) \lor Q = C)) \land \neg B \in (R L Q)) \land x \in (R L Q)) \land x \in (A I B)) \to x \in (R L Q)$
142	1 3 2 139 140 141	tglnpt	$⊢ ((((φ \land \neg (R \in (Q L C) \lor Q = C)) \land \neg B \in (R L Q)) \land x \in (R L Q)) \land x \in (A I B)) \to x \in P$
143		simpr	$⊢ ((((φ \land \neg (R \in (Q L C) \lor Q = C)) \land \neg B \in (R L Q)) \land x \in (R L Q)) \land x \in (A I B)) \to x \in (A I B)$
144	139	ad2antrr	$⊢ ((((((φ \land \neg (R \in (Q L C) \lor Q = C)) \land \neg B \in (R L Q)) \land x \in (R L Q)) \land x \in (A I B)) \land t \in P) \land (t \in (x I R) \land t \in (C I B))) \to G \in 𝒢_{Tarski}$
145	87	ad3antrrr	$⊢ ((((φ \land \neg (R \in (Q L C) \lor Q = C)) \land \neg B \in (R L Q)) \land x \in (R L Q)) \land x \in (A I B)) \to R \in P$
146	145	ad2antrr	$⊢ ((((((φ \land \neg (R \in (Q L C) \lor Q = C)) \land \neg B \in (R L Q)) \land x \in (R L Q)) \land x \in (A I B)) \land t \in P) \land (t \in (x I R) \land t \in (C I B))) \to R \in P$
147	88	ad5antr	$⊢ ((((((φ \land \neg (R \in (Q L C) \lor Q = C)) \land \neg B \in (R L Q)) \land x \in (R L Q)) \land x \in (A I B)) \land t \in P) \land (t \in (x I R) \land t \in (C I B))) \to Q \in P$
148	117	ad2antrr	$⊢ ((((φ \land \neg (R \in (Q L C) \lor Q = C)) \land \neg B \in (R L Q)) \land x \in (R L Q)) \land x \in (A I B)) \to C \in P$
149	148	ad2antrr	$⊢ ((((((φ \land \neg (R \in (Q L C) \lor Q = C)) \land \neg B \in (R L Q)) \land x \in (R L Q)) \land x \in (A I B)) \land t \in P) \land (t \in (x I R) \land t \in (C I B))) \to C \in P$
150	90	ad5antr	$⊢ ((((((φ \land \neg (R \in (Q L C) \lor Q = C)) \land \neg B \in (R L Q)) \land x \in (R L Q)) \land x \in (A I B)) \land t \in P) \land (t \in (x I R) \land t \in (C I B))) \to \neg (R \in (Q L C) \lor Q = C)$
151		simplr	$⊢ ((((((φ \land \neg (R \in (Q L C) \lor Q = C)) \land \neg B \in (R L Q)) \land x \in (R L Q)) \land x \in (A I B)) \land t \in P) \land (t \in (x I R) \land t \in (C I B))) \to t \in P$
152	114	ad4antr	$⊢ ((((((φ \land \neg (R \in (Q L C) \lor Q = C)) \land \neg B \in (R L Q)) \land x \in (R L Q)) \land x \in (A I B)) \land t \in P) \land (t \in (x I R) \land t \in (C I B))) \to R \neq Q$
153	142	ad2antrr	$⊢ ((((((φ \land \neg (R \in (Q L C) \lor Q = C)) \land \neg B \in (R L Q)) \land x \in (R L Q)) \land x \in (A I B)) \land t \in P) \land (t \in (x I R) \land t \in (C I B))) \to x \in P$
154	91	necomd	$⊢ (φ \land \neg (R \in (Q L C) \lor Q = C)) \to Q \neq R$
155	154	ad5antr	$⊢ ((((((φ \land \neg (R \in (Q L C) \lor Q = C)) \land \neg B \in (R L Q)) \land x \in (R L Q)) \land x \in (A I B)) \land t \in P) \land (t \in (x I R) \land t \in (C I B))) \to Q \neq R$
156	141	ad2antrr	$⊢ ((((((φ \land \neg (R \in (Q L C) \lor Q = C)) \land \neg B \in (R L Q)) \land x \in (R L Q)) \land x \in (A I B)) \land t \in P) \land (t \in (x I R) \land t \in (C I B))) \to x \in (R L Q)$
157	1 2 3 144 147 146 153 155 156	lncom	$⊢ ((((((φ \land \neg (R \in (Q L C) \lor Q = C)) \land \neg B \in (R L Q)) \land x \in (R L Q)) \land x \in (A I B)) \land t \in P) \land (t \in (x I R) \land t \in (C I B))) \to x \in (Q L R)$
158		simprl	$⊢ ((((((φ \land \neg (R \in (Q L C) \lor Q = C)) \land \neg B \in (R L Q)) \land x \in (R L Q)) \land x \in (A I B)) \land t \in P) \land (t \in (x I R) \land t \in (C I B))) \to t \in (x I R)$
159	1 2 3 144 153 147 146 151 157 158	coltr3	$⊢ ((((((φ \land \neg (R \in (Q L C) \lor Q = C)) \land \neg B \in (R L Q)) \land x \in (R L Q)) \land x \in (A I B)) \land t \in P) \land (t \in (x I R) \land t \in (C I B))) \to t \in (Q L R)$
160	1 2 3 144 146 147 151 152 159	lncom	$⊢ ((((((φ \land \neg (R \in (Q L C) \lor Q = C)) \land \neg B \in (R L Q)) \land x \in (R L Q)) \land x \in (A I B)) \land t \in P) \land (t \in (x I R) \land t \in (C I B))) \to t \in (R L Q)$
161	92	ad5antr	$⊢ ((((((φ \land \neg (R \in (Q L C) \lor Q = C)) \land \neg B \in (R L Q)) \land x \in (R L Q)) \land x \in (A I B)) \land t \in P) \land (t \in (x I R) \land t \in (C I B))) \to Q \in (R L Q)$
162	96	ad5antr	$⊢ ((((((φ \land \neg (R \in (Q L C) \lor Q = C)) \land \neg B \in (R L Q)) \land x \in (R L Q)) \land x \in (A I B)) \land t \in P) \land (t \in (x I R) \land t \in (C I B))) \to C \neq Q$
163	119	ad2antrr	$⊢ ((((φ \land \neg (R \in (Q L C) \lor Q = C)) \land \neg B \in (R L Q)) \land x \in (R L Q)) \land x \in (A I B)) \to B \in P$
164	163	ad2antrr	$⊢ ((((((φ \land \neg (R \in (Q L C) \lor Q = C)) \land \neg B \in (R L Q)) \land x \in (R L Q)) \land x \in (A I B)) \land t \in P) \land (t \in (x I R) \land t \in (C I B))) \to B \in P$
165	6	adantr	$⊢ (φ \land \neg (R \in (Q L C) \lor Q = C)) \to B \in P$
166	96	necomd	$⊢ (φ \land \neg (R \in (Q L C) \lor Q = C)) \to Q \neq C$
167	11	adantr	$⊢ (φ \land \neg (R \in (Q L C) \lor Q = C)) \to Q \in (B I C)$
168	1 2 3 86 88 89 165 166 167	btwnlng2	$⊢ (φ \land \neg (R \in (Q L C) \lor Q = C)) \to B \in (Q L C)$
169	168	ad5antr	$⊢ ((((((φ \land \neg (R \in (Q L C) \lor Q = C)) \land \neg B \in (R L Q)) \land x \in (R L Q)) \land x \in (A I B)) \land t \in P) \land (t \in (x I R) \land t \in (C I B))) \to B \in (Q L C)$
170		simprr	$⊢ ((((((φ \land \neg (R \in (Q L C) \lor Q = C)) \land \neg B \in (R L Q)) \land x \in (R L Q)) \land x \in (A I B)) \land t \in P) \land (t \in (x I R) \land t \in (C I B))) \to t \in (C I B)$
171	1 18 2 144 149 151 164 170	tgbtwncom	$⊢ ((((((φ \land \neg (R \in (Q L C) \lor Q = C)) \land \neg B \in (R L Q)) \land x \in (R L Q)) \land x \in (A I B)) \land t \in P) \land (t \in (x I R) \land t \in (C I B))) \to t \in (B I C)$
172	1 2 3 144 164 147 149 151 169 171	coltr3	$⊢ ((((((φ \land \neg (R \in (Q L C) \lor Q = C)) \land \neg B \in (R L Q)) \land x \in (R L Q)) \land x \in (A I B)) \land t \in P) \land (t \in (x I R) \land t \in (C I B))) \to t \in (Q L C)$
173	1 2 3 144 149 147 151 162 172	lncom	$⊢ ((((((φ \land \neg (R \in (Q L C) \lor Q = C)) \land \neg B \in (R L Q)) \land x \in (R L Q)) \land x \in (A I B)) \land t \in P) \land (t \in (x I R) \land t \in (C I B))) \to t \in (C L Q)$
174	1 2 3 86 89 88 96	tglinerflx2	$⊢ (φ \land \neg (R \in (Q L C) \lor Q = C)) \to Q \in (C L Q)$
175	174	ad5antr	$⊢ ((((((φ \land \neg (R \in (Q L C) \lor Q = C)) \land \neg B \in (R L Q)) \land x \in (R L Q)) \land x \in (A I B)) \land t \in P) \land (t \in (x I R) \land t \in (C I B))) \to Q \in (C L Q)$
176	1 2 3 144 146 147 149 147 150 160 161 173 175	tglineinteq	$⊢ ((((((φ \land \neg (R \in (Q L C) \lor Q = C)) \land \neg B \in (R L Q)) \land x \in (R L Q)) \land x \in (A I B)) \land t \in P) \land (t \in (x I R) \land t \in (C I B))) \to t = Q$
177	1 18 2 144 153 151 146 158	tgbtwncom	$⊢ ((((((φ \land \neg (R \in (Q L C) \lor Q = C)) \land \neg B \in (R L Q)) \land x \in (R L Q)) \land x \in (A I B)) \land t \in P) \land (t \in (x I R) \land t \in (C I B))) \to t \in (R I x)$
178	176 177	eqeltrrd	$⊢ ((((((φ \land \neg (R \in (Q L C) \lor Q = C)) \land \neg B \in (R L Q)) \land x \in (R L Q)) \land x \in (A I B)) \land t \in P) \land (t \in (x I R) \land t \in (C I B))) \to Q \in (R I x)$
179	118	ad2antrr	$⊢ ((((φ \land \neg (R \in (Q L C) \lor Q = C)) \land \neg B \in (R L Q)) \land x \in (R L Q)) \land x \in (A I B)) \to A \in P$
180	1 18 2 139 179 142 163 143	tgbtwncom	$⊢ ((((φ \land \neg (R \in (Q L C) \lor Q = C)) \land \neg B \in (R L Q)) \land x \in (R L Q)) \land x \in (A I B)) \to x \in (B I A)$
181	26	ad4antr	$⊢ ((((φ \land \neg (R \in (Q L C) \lor Q = C)) \land \neg B \in (R L Q)) \land x \in (R L Q)) \land x \in (A I B)) \to C \in (R I A)$
182	1 18 2 139 163 145 179 142 148 180 181	axtgpasch	$⊢ ((((φ \land \neg (R \in (Q L C) \lor Q = C)) \land \neg B \in (R L Q)) \land x \in (R L Q)) \land x \in (A I B)) \to \exists t \in P (t \in (x I R) \land t \in (C I B))$
183	178 182	r19.29a	$⊢ ((((φ \land \neg (R \in (Q L C) \lor Q = C)) \land \neg B \in (R L Q)) \land x \in (R L Q)) \land x \in (A I B)) \to Q \in (R I x)$
184	142 143 183	jca32	$⊢ ((((φ \land \neg (R \in (Q L C) \lor Q = C)) \land \neg B \in (R L Q)) \land x \in (R L Q)) \land x \in (A I B)) \to (x \in P \land (x \in (A I B) \land Q \in (R I x)))$
185	184	expl	$⊢ ((φ \land \neg (R \in (Q L C) \lor Q = C)) \land \neg B \in (R L Q)) \to ((x \in (R L Q) \land x \in (A I B)) \to (x \in P \land (x \in (A I B) \land Q \in (R I x))))$
186	185	reximdv2	$⊢ ((φ \land \neg (R \in (Q L C) \lor Q = C)) \land \neg B \in (R L Q)) \to (\exists x \in (R L Q) x \in (A I B) \to \exists x \in P (x \in (A I B) \land Q \in (R I x)))$
187	138 186	mpd	$⊢ ((φ \land \neg (R \in (Q L C) \lor Q = C)) \land \neg B \in (R L Q)) \to \exists x \in P (x \in (A I B) \land Q \in (R I x))$
188	106 187	pm2.61dan	$⊢ (φ \land \neg (R \in (Q L C) \lor Q = C)) \to \exists x \in P (x \in (A I B) \land Q \in (R I x))$
189	76 188	pm2.61dan	$⊢ φ \to \exists x \in P (x \in (A I B) \land Q \in (R I x))$

Metamath Proof Explorer

Theorem outpasch

Proof