colperpexlem3

	Ref	Expression
Hypotheses	colperpex.p	$⊢ P = {Base}_{G}$
	colperpex.d	$⊢ \underset{˙}{-} = dist (G)$
	colperpex.i	$⊢ I = Itv (G)$
	colperpex.l	$⊢ L = {Line}_{𝒢} (G)$
	colperpex.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	colperpex.1	$⊢ φ \to A \in P$
	colperpex.2	$⊢ φ \to B \in P$
	colperpex.3	$⊢ φ \to C \in P$
	colperpex.4	$⊢ φ \to A \neq B$
	colperpexlem3.1	$⊢ φ \to \neg C \in (A L B)$
Assertion	colperpexlem3	$⊢ φ \to \exists p \in P ((A L p) ⟂_{𝒢} (G) (A L B) \land \exists t \in P ((t \in (A L B) \lor A = B) \land t \in (C I p)))$

Proof

Step	Hyp	Ref	Expression
1		colperpex.p	$⊢ P = {Base}_{G}$
2		colperpex.d	$⊢ \underset{˙}{-} = dist (G)$
3		colperpex.i	$⊢ I = Itv (G)$
4		colperpex.l	$⊢ L = {Line}_{𝒢} (G)$
5		colperpex.g	$⊢ φ \to G \in 𝒢_{Tarski}$
6		colperpex.1	$⊢ φ \to A \in P$
7		colperpex.2	$⊢ φ \to B \in P$
8		colperpex.3	$⊢ φ \to C \in P$
9		colperpex.4	$⊢ φ \to A \neq B$
10		colperpexlem3.1	$⊢ φ \to \neg C \in (A L B)$
11		eqid	$⊢ {pInv}_{𝒢} (G) = {pInv}_{𝒢} (G)$
12	5	ad2antrr	$⊢ ((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \to G \in 𝒢_{Tarski}$
13		eqid	$⊢ {pInv}_{𝒢} (G) (p) = {pInv}_{𝒢} (G) (p)$
14	1 3 4 5 6 7 9	tgelrnln	$⊢ φ \to A L B \in ran L$
15	14	ad2antrr	$⊢ ((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \to A L B \in ran L$
16		simplr	$⊢ ((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \to x \in (A L B)$
17	1 4 3 12 15 16	tglnpt	$⊢ ((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \to x \in P$
18		eqid	$⊢ {pInv}_{𝒢} (G) (x) = {pInv}_{𝒢} (G) (x)$
19	8	ad2antrr	$⊢ ((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \to C \in P$
20	1 2 3 4 11 12 17 18 19	mircl	$⊢ ((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \to {pInv}_{𝒢} (G) (x) (C) \in P$
21	6	ad2antrr	$⊢ ((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \to A \in P$
22		eqid	$⊢ {pInv}_{𝒢} (G) (A) = {pInv}_{𝒢} (G) (A)$
23	1 2 3 4 11 12 21 22 19	mircl	$⊢ ((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \to {pInv}_{𝒢} (G) (A) (C) \in P$
24	1 2 3 4 11 12 21 22 19	mircgr	$⊢ ((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \to A \underset{˙}{-} {pInv}_{𝒢} (G) (A) (C) = A \underset{˙}{-} C$
25	7	ad2antrr	$⊢ ((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \to B \in P$
26	10	ad2antrr	$⊢ ((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \to \neg C \in (A L B)$
27		nelne2	$⊢ (x \in (A L B) \land \neg C \in (A L B)) \to x \neq C$
28	16 26 27	syl2anc	$⊢ ((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \to x \neq C$
29	1 3 4 12 17 19 28	tgelrnln	$⊢ ((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \to x L C \in ran L$
30	1 3 4 12 17 19 28	tglinecom	$⊢ ((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \to x L C = C L x$
31		simpr	$⊢ ((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \to (C L x) ⟂_{𝒢} (G) (A L B)$
32	30 31	eqbrtrd	$⊢ ((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \to (x L C) ⟂_{𝒢} (G) (A L B)$
33	1 2 3 4 12 29 15 32	perpcom	$⊢ ((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \to (A L B) ⟂_{𝒢} (G) (x L C)$
34	1 2 3 4 12 21 25 16 19 33	perprag	$⊢ ((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \to ⟨“ A x C ”⟩ \in ∟_{𝒢} (G)$
35	1 2 3 4 11 12 21 17 19	israg	$⊢ ((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \to (⟨“ A x C ”⟩ \in ∟_{𝒢} (G) \leftrightarrow A \underset{˙}{-} C = A \underset{˙}{-} {pInv}_{𝒢} (G) (x) (C))$
36	34 35	mpbid	$⊢ ((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \to A \underset{˙}{-} C = A \underset{˙}{-} {pInv}_{𝒢} (G) (x) (C)$
37	24 36	eqtr2d	$⊢ ((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \to A \underset{˙}{-} {pInv}_{𝒢} (G) (x) (C) = A \underset{˙}{-} {pInv}_{𝒢} (G) (A) (C)$
38	1 2 3 4 11 12 13 20 23 21 37	midexlem	$⊢ ((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \to \exists p \in P {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))$
39	12	ad2antrr	$⊢ ((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \to G \in 𝒢_{Tarski}$
40	23	ad2antrr	$⊢ ((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \to {pInv}_{𝒢} (G) (A) (C) \in P$
41	21	ad2antrr	$⊢ ((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \to A \in P$
42	19	ad2antrr	$⊢ ((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \to C \in P$
43	20	ad2antrr	$⊢ ((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \to {pInv}_{𝒢} (G) (x) (C) \in P$
44	17	ad2antrr	$⊢ ((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \to x \in P$
45		simplr	$⊢ ((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \to p \in P$
46	1 2 3 4 11 39 41 22 42	mirbtwn	$⊢ ((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \to A \in ({pInv}_{𝒢} (G) (A) (C) I C)$
47	1 2 3 4 11 39 44 18 42	mirbtwn	$⊢ ((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \to x \in ({pInv}_{𝒢} (G) (x) (C) I C)$
48	1 2 3 4 11 39 45 13 43	mirbtwn	$⊢ ((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \to p \in ({pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C)) I {pInv}_{𝒢} (G) (x) (C))$
49		simpr	$⊢ ((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \to {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))$
50	49	eqcomd	$⊢ ((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \to {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C)) = {pInv}_{𝒢} (G) (A) (C)$
51	50	oveq1d	$⊢ ((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \to {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C)) I {pInv}_{𝒢} (G) (x) (C) = {pInv}_{𝒢} (G) (A) (C) I {pInv}_{𝒢} (G) (x) (C)$
52	48 51	eleqtrd	$⊢ ((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \to p \in ({pInv}_{𝒢} (G) (A) (C) I {pInv}_{𝒢} (G) (x) (C))$
53	1 2 3 39 40 41 42 43 44 45 46 47 52	tgtrisegint	$⊢ ((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \to \exists t \in P (t \in (p I C) \land t \in (A I x))$
54	39	ad3antrrr	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \land t \in P) \land (t \in (p I C) \land t \in (A I x))) \land x = A) \to G \in 𝒢_{Tarski}$
55	41	ad3antrrr	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \land t \in P) \land (t \in (p I C) \land t \in (A I x))) \land x = A) \to A \in P$
56		simpllr	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \land t \in P) \land (t \in (p I C) \land t \in (A I x))) \land x = A) \to t \in P$
57		simplrr	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \land t \in P) \land (t \in (p I C) \land t \in (A I x))) \land x = A) \to t \in (A I x)$
58		simpr	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \land t \in P) \land (t \in (p I C) \land t \in (A I x))) \land x = A) \to x = A$
59	58	oveq2d	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \land t \in P) \land (t \in (p I C) \land t \in (A I x))) \land x = A) \to A I x = A I A$
60	57 59	eleqtrd	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \land t \in P) \land (t \in (p I C) \land t \in (A I x))) \land x = A) \to t \in (A I A)$
61	1 2 3 54 55 56 60	axtgbtwnid	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \land t \in P) \land (t \in (p I C) \land t \in (A I x))) \land x = A) \to A = t$
62	61	eqcomd	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \land t \in P) \land (t \in (p I C) \land t \in (A I x))) \land x = A) \to t = A$
63	62	oveq1d	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \land t \in P) \land (t \in (p I C) \land t \in (A I x))) \land x = A) \to t L p = A L p$
64	50	ad3antrrr	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \land t \in P) \land (t \in (p I C) \land t \in (A I x))) \land x = A) \to {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C)) = {pInv}_{𝒢} (G) (A) (C)$
65	58	fveq2d	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \land t \in P) \land (t \in (p I C) \land t \in (A I x))) \land x = A) \to {pInv}_{𝒢} (G) (x) = {pInv}_{𝒢} (G) (A)$
66	65	fveq1d	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \land t \in P) \land (t \in (p I C) \land t \in (A I x))) \land x = A) \to {pInv}_{𝒢} (G) (x) (C) = {pInv}_{𝒢} (G) (A) (C)$
67	64 66	eqtr4d	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \land t \in P) \land (t \in (p I C) \land t \in (A I x))) \land x = A) \to {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C)) = {pInv}_{𝒢} (G) (x) (C)$
68	45	ad3antrrr	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \land t \in P) \land (t \in (p I C) \land t \in (A I x))) \land x = A) \to p \in P$
69	43	ad3antrrr	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \land t \in P) \land (t \in (p I C) \land t \in (A I x))) \land x = A) \to {pInv}_{𝒢} (G) (x) (C) \in P$
70	1 2 3 4 11 54 68 13 69	mirinv	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \land t \in P) \land (t \in (p I C) \land t \in (A I x))) \land x = A) \to ({pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C)) = {pInv}_{𝒢} (G) (x) (C) \leftrightarrow p = {pInv}_{𝒢} (G) (x) (C))$
71	67 70	mpbid	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \land t \in P) \land (t \in (p I C) \land t \in (A I x))) \land x = A) \to p = {pInv}_{𝒢} (G) (x) (C)$
72	44	ad3antrrr	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \land t \in P) \land (t \in (p I C) \land t \in (A I x))) \land x = A) \to x \in P$
73	58	oveq1d	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \land t \in P) \land (t \in (p I C) \land t \in (A I x))) \land x = A) \to x I x = A I x$
74	57 73	eleqtrrd	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \land t \in P) \land (t \in (p I C) \land t \in (A I x))) \land x = A) \to t \in (x I x)$
75	1 2 3 54 72 56 74	axtgbtwnid	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \land t \in P) \land (t \in (p I C) \land t \in (A I x))) \land x = A) \to x = t$
76	75	eqcomd	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \land t \in P) \land (t \in (p I C) \land t \in (A I x))) \land x = A) \to t = x$
77	71 76	oveq12d	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \land t \in P) \land (t \in (p I C) \land t \in (A I x))) \land x = A) \to p L t = {pInv}_{𝒢} (G) (x) (C) L x$
78	34	ad2antrr	$⊢ ((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \to ⟨“ A x C ”⟩ \in ∟_{𝒢} (G)$
79	1 2 3 4 11 39 45 13 43 50	mircom	$⊢ ((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \to {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (A) (C)) = {pInv}_{𝒢} (G) (x) (C)$
80	28	ad2antrr	$⊢ ((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \to x \neq C$
81	1 2 3 4 39 11 22 18 13 41 44 42 45 78 79 80	colperpexlem2	$⊢ ((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \to A \neq p$
82	81	ad3antrrr	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \land t \in P) \land (t \in (p I C) \land t \in (A I x))) \land x = A) \to A \neq p$
83	62 82	eqnetrd	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \land t \in P) \land (t \in (p I C) \land t \in (A I x))) \land x = A) \to t \neq p$
84	1 3 4 54 56 68 83	tglinecom	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \land t \in P) \land (t \in (p I C) \land t \in (A I x))) \land x = A) \to t L p = p L t$
85	42	ad3antrrr	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \land t \in P) \land (t \in (p I C) \land t \in (A I x))) \land x = A) \to C \in P$
86	80	ad3antrrr	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \land t \in P) \land (t \in (p I C) \land t \in (A I x))) \land x = A) \to x \neq C$
87	54	adantr	$⊢ ((((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \land t \in P) \land (t \in (p I C) \land t \in (A I x))) \land x = A) \land {pInv}_{𝒢} (G) (x) (C) = x) \to G \in 𝒢_{Tarski}$
88	72	adantr	$⊢ ((((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \land t \in P) \land (t \in (p I C) \land t \in (A I x))) \land x = A) \land {pInv}_{𝒢} (G) (x) (C) = x) \to x \in P$
89	85	adantr	$⊢ ((((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \land t \in P) \land (t \in (p I C) \land t \in (A I x))) \land x = A) \land {pInv}_{𝒢} (G) (x) (C) = x) \to C \in P$
90	1 2 3 4 11 87 88 18	mircinv	$⊢ ((((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \land t \in P) \land (t \in (p I C) \land t \in (A I x))) \land x = A) \land {pInv}_{𝒢} (G) (x) (C) = x) \to {pInv}_{𝒢} (G) (x) (x) = x$
91		simpr	$⊢ ((((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \land t \in P) \land (t \in (p I C) \land t \in (A I x))) \land x = A) \land {pInv}_{𝒢} (G) (x) (C) = x) \to {pInv}_{𝒢} (G) (x) (C) = x$
92	90 91	eqtr4d	$⊢ ((((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \land t \in P) \land (t \in (p I C) \land t \in (A I x))) \land x = A) \land {pInv}_{𝒢} (G) (x) (C) = x) \to {pInv}_{𝒢} (G) (x) (x) = {pInv}_{𝒢} (G) (x) (C)$
93	1 2 3 4 11 87 88 18 88 89 92	mireq	$⊢ ((((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \land t \in P) \land (t \in (p I C) \land t \in (A I x))) \land x = A) \land {pInv}_{𝒢} (G) (x) (C) = x) \to x = C$
94	86	adantr	$⊢ ((((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \land t \in P) \land (t \in (p I C) \land t \in (A I x))) \land x = A) \land {pInv}_{𝒢} (G) (x) (C) = x) \to x \neq C$
95	94	neneqd	$⊢ ((((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \land t \in P) \land (t \in (p I C) \land t \in (A I x))) \land x = A) \land {pInv}_{𝒢} (G) (x) (C) = x) \to \neg x = C$
96	93 95	pm2.65da	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \land t \in P) \land (t \in (p I C) \land t \in (A I x))) \land x = A) \to \neg {pInv}_{𝒢} (G) (x) (C) = x$
97	96	neqned	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \land t \in P) \land (t \in (p I C) \land t \in (A I x))) \land x = A) \to {pInv}_{𝒢} (G) (x) (C) \neq x$
98	47	ad3antrrr	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \land t \in P) \land (t \in (p I C) \land t \in (A I x))) \land x = A) \to x \in ({pInv}_{𝒢} (G) (x) (C) I C)$
99	1 3 4 54 72 85 69 86 98	btwnlng2	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \land t \in P) \land (t \in (p I C) \land t \in (A I x))) \land x = A) \to {pInv}_{𝒢} (G) (x) (C) \in (x L C)$
100	1 3 4 54 72 85 86 69 97 99	tglineelsb2	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \land t \in P) \land (t \in (p I C) \land t \in (A I x))) \land x = A) \to x L C = x L {pInv}_{𝒢} (G) (x) (C)$
101	28	necomd	$⊢ ((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \to C \neq x$
102	101	ad5antr	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \land t \in P) \land (t \in (p I C) \land t \in (A I x))) \land x = A) \to C \neq x$
103	1 3 4 54 85 72 102	tglinecom	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \land t \in P) \land (t \in (p I C) \land t \in (A I x))) \land x = A) \to C L x = x L C$
104	1 3 4 54 69 72 97	tglinecom	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \land t \in P) \land (t \in (p I C) \land t \in (A I x))) \land x = A) \to {pInv}_{𝒢} (G) (x) (C) L x = x L {pInv}_{𝒢} (G) (x) (C)$
105	100 103 104	3eqtr4d	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \land t \in P) \land (t \in (p I C) \land t \in (A I x))) \land x = A) \to C L x = {pInv}_{𝒢} (G) (x) (C) L x$
106	77 84 105	3eqtr4d	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \land t \in P) \land (t \in (p I C) \land t \in (A I x))) \land x = A) \to t L p = C L x$
107	63 106	eqtr3d	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \land t \in P) \land (t \in (p I C) \land t \in (A I x))) \land x = A) \to A L p = C L x$
108	31	ad5antr	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \land t \in P) \land (t \in (p I C) \land t \in (A I x))) \land x = A) \to (C L x) ⟂_{𝒢} (G) (A L B)$
109	107 108	eqbrtrd	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \land t \in P) \land (t \in (p I C) \land t \in (A I x))) \land x = A) \to (A L p) ⟂_{𝒢} (G) (A L B)$
110	39	ad3antrrr	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \land t \in P) \land (t \in (p I C) \land t \in (A I x))) \land x \neq A) \to G \in 𝒢_{Tarski}$
111	41	ad3antrrr	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \land t \in P) \land (t \in (p I C) \land t \in (A I x))) \land x \neq A) \to A \in P$
112	45	ad3antrrr	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \land t \in P) \land (t \in (p I C) \land t \in (A I x))) \land x \neq A) \to p \in P$
113	81	ad3antrrr	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \land t \in P) \land (t \in (p I C) \land t \in (A I x))) \land x \neq A) \to A \neq p$
114	1 3 4 110 111 112 113	tgelrnln	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \land t \in P) \land (t \in (p I C) \land t \in (A I x))) \land x \neq A) \to A L p \in ran L$
115	15	ad5antr	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \land t \in P) \land (t \in (p I C) \land t \in (A I x))) \land x \neq A) \to A L B \in ran L$
116	1 3 4 110 111 112 113	tglinerflx1	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \land t \in P) \land (t \in (p I C) \land t \in (A I x))) \land x \neq A) \to A \in (A L p)$
117	9	ad2antrr	$⊢ ((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \to A \neq B$
118	1 3 4 12 21 25 117	tglinerflx1	$⊢ ((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \to A \in (A L B)$
119	118	ad5antr	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \land t \in P) \land (t \in (p I C) \land t \in (A I x))) \land x \neq A) \to A \in (A L B)$
120	116 119	elind	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \land t \in P) \land (t \in (p I C) \land t \in (A I x))) \land x \neq A) \to A \in ((A L p) \cap (A L B))$
121	1 3 4 110 111 112 113	tglinerflx2	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \land t \in P) \land (t \in (p I C) \land t \in (A I x))) \land x \neq A) \to p \in (A L p)$
122	16	ad5antr	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \land t \in P) \land (t \in (p I C) \land t \in (A I x))) \land x \neq A) \to x \in (A L B)$
123	113	necomd	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \land t \in P) \land (t \in (p I C) \land t \in (A I x))) \land x \neq A) \to p \neq A$
124		simpr	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \land t \in P) \land (t \in (p I C) \land t \in (A I x))) \land x \neq A) \to x \neq A$
125	44	ad3antrrr	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \land t \in P) \land (t \in (p I C) \land t \in (A I x))) \land x \neq A) \to x \in P$
126	1 2 3 4 39 11 22 18 13 41 44 42 45 78 79	colperpexlem1	$⊢ ((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \to ⟨“ x A p ”⟩ \in ∟_{𝒢} (G)$
127	126	ad3antrrr	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \land t \in P) \land (t \in (p I C) \land t \in (A I x))) \land x \neq A) \to ⟨“ x A p ”⟩ \in ∟_{𝒢} (G)$
128	1 2 3 4 11 110 125 111 112 127	ragcom	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \land t \in P) \land (t \in (p I C) \land t \in (A I x))) \land x \neq A) \to ⟨“ p A x ”⟩ \in ∟_{𝒢} (G)$
129	1 2 3 4 110 114 115 120 121 122 123 124 128	ragperp	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \land t \in P) \land (t \in (p I C) \land t \in (A I x))) \land x \neq A) \to (A L p) ⟂_{𝒢} (G) (A L B)$
130	109 129	pm2.61dane	$⊢ ((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \land t \in P) \land (t \in (p I C) \land t \in (A I x))) \to (A L p) ⟂_{𝒢} (G) (A L B)$
131	118	ad5antr	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \land t \in P) \land (t \in (p I C) \land t \in (A I x))) \land x = A) \to A \in (A L B)$
132	62 131	eqeltrd	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \land t \in P) \land (t \in (p I C) \land t \in (A I x))) \land x = A) \to t \in (A L B)$
133	132	orcd	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \land t \in P) \land (t \in (p I C) \land t \in (A I x))) \land x = A) \to (t \in (A L B) \lor A = B)$
134	25	ad5antr	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \land t \in P) \land (t \in (p I C) \land t \in (A I x))) \land x \neq A) \to B \in P$
135	117	ad5antr	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \land t \in P) \land (t \in (p I C) \land t \in (A I x))) \land x \neq A) \to A \neq B$
136		simpllr	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \land t \in P) \land (t \in (p I C) \land t \in (A I x))) \land x \neq A) \to t \in P$
137	124	necomd	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \land t \in P) \land (t \in (p I C) \land t \in (A I x))) \land x \neq A) \to A \neq x$
138		simplrr	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \land t \in P) \land (t \in (p I C) \land t \in (A I x))) \land x \neq A) \to t \in (A I x)$
139	1 3 4 110 111 125 136 137 138	btwnlng1	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \land t \in P) \land (t \in (p I C) \land t \in (A I x))) \land x \neq A) \to t \in (A L x)$
140	1 3 4 110 111 134 135 125 124 122 136 139	tglineeltr	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \land t \in P) \land (t \in (p I C) \land t \in (A I x))) \land x \neq A) \to t \in (A L B)$
141	140	orcd	$⊢ (((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \land t \in P) \land (t \in (p I C) \land t \in (A I x))) \land x \neq A) \to (t \in (A L B) \lor A = B)$
142	133 141	pm2.61dane	$⊢ ((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \land t \in P) \land (t \in (p I C) \land t \in (A I x))) \to (t \in (A L B) \lor A = B)$
143	39	ad2antrr	$⊢ ((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \land t \in P) \land (t \in (p I C) \land t \in (A I x))) \to G \in 𝒢_{Tarski}$
144	45	ad2antrr	$⊢ ((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \land t \in P) \land (t \in (p I C) \land t \in (A I x))) \to p \in P$
145		simplr	$⊢ ((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \land t \in P) \land (t \in (p I C) \land t \in (A I x))) \to t \in P$
146	42	ad2antrr	$⊢ ((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \land t \in P) \land (t \in (p I C) \land t \in (A I x))) \to C \in P$
147		simprl	$⊢ ((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \land t \in P) \land (t \in (p I C) \land t \in (A I x))) \to t \in (p I C)$
148	1 2 3 143 144 145 146 147	tgbtwncom	$⊢ ((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \land t \in P) \land (t \in (p I C) \land t \in (A I x))) \to t \in (C I p)$
149	130 142 148	jca32	$⊢ ((((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \land t \in P) \land (t \in (p I C) \land t \in (A I x))) \to ((A L p) ⟂_{𝒢} (G) (A L B) \land ((t \in (A L B) \lor A = B) \land t \in (C I p)))$
150	149	ex	$⊢ (((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \land t \in P) \to ((t \in (p I C) \land t \in (A I x)) \to ((A L p) ⟂_{𝒢} (G) (A L B) \land ((t \in (A L B) \lor A = B) \land t \in (C I p))))$
151	150	reximdva	$⊢ ((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \to (\exists t \in P (t \in (p I C) \land t \in (A I x)) \to \exists t \in P ((A L p) ⟂_{𝒢} (G) (A L B) \land ((t \in (A L B) \lor A = B) \land t \in (C I p))))$
152	53 151	mpd	$⊢ ((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \to \exists t \in P ((A L p) ⟂_{𝒢} (G) (A L B) \land ((t \in (A L B) \lor A = B) \land t \in (C I p)))$
153		r19.42v	$⊢ \exists t \in P ((A L p) ⟂_{𝒢} (G) (A L B) \land ((t \in (A L B) \lor A = B) \land t \in (C I p))) \leftrightarrow ((A L p) ⟂_{𝒢} (G) (A L B) \land \exists t \in P ((t \in (A L B) \lor A = B) \land t \in (C I p)))$
154	152 153	sylib	$⊢ ((((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C))) \to ((A L p) ⟂_{𝒢} (G) (A L B) \land \exists t \in P ((t \in (A L B) \lor A = B) \land t \in (C I p)))$
155	154	ex	$⊢ (((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \land p \in P) \to ({pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C)) \to ((A L p) ⟂_{𝒢} (G) (A L B) \land \exists t \in P ((t \in (A L B) \lor A = B) \land t \in (C I p))))$
156	155	reximdva	$⊢ ((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \to (\exists p \in P {pInv}_{𝒢} (G) (A) (C) = {pInv}_{𝒢} (G) (p) ({pInv}_{𝒢} (G) (x) (C)) \to \exists p \in P ((A L p) ⟂_{𝒢} (G) (A L B) \land \exists t \in P ((t \in (A L B) \lor A = B) \land t \in (C I p))))$
157	38 156	mpd	$⊢ ((φ \land x \in (A L B)) \land (C L x) ⟂_{𝒢} (G) (A L B)) \to \exists p \in P ((A L p) ⟂_{𝒢} (G) (A L B) \land \exists t \in P ((t \in (A L B) \lor A = B) \land t \in (C I p)))$
158	1 2 3 4 5 14 8 10	footex	$⊢ φ \to \exists x \in (A L B) (C L x) ⟂_{𝒢} (G) (A L B)$
159	157 158	r19.29a	$⊢ φ \to \exists p \in P ((A L p) ⟂_{𝒢} (G) (A L B) \land \exists t \in P ((t \in (A L B) \lor A = B) \land t \in (C I p)))$

Metamath Proof Explorer

Theorem colperpexlem3

Proof