mirconn

Description: Point inversion of connectedness. (Contributed by Thierry Arnoux, 2-Mar-2020)

	Ref	Expression
Hypotheses	mirval.p	$⊢ P = {Base}_{G}$
	mirval.d	$⊢ \underset{˙}{-} = dist (G)$
	mirval.i	$⊢ I = Itv (G)$
	mirval.l	$⊢ L = {Line}_{𝒢} (G)$
	mirval.s	$⊢ S = {pInv}_{𝒢} (G)$
	mirval.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	mirconn.m	$⊢ M = S (A)$
	mirconn.a	$⊢ φ \to A \in P$
	mirconn.x	$⊢ φ \to X \in P$
	mirconn.y	$⊢ φ \to Y \in P$
	mirconn.1	$⊢ φ \to (X \in (A I Y) \lor Y \in (A I X))$
Assertion	mirconn	$⊢ φ \to A \in (X I M (Y))$

Proof

Step	Hyp	Ref	Expression
1		mirval.p	$⊢ P = {Base}_{G}$
2		mirval.d	$⊢ \underset{˙}{-} = dist (G)$
3		mirval.i	$⊢ I = Itv (G)$
4		mirval.l	$⊢ L = {Line}_{𝒢} (G)$
5		mirval.s	$⊢ S = {pInv}_{𝒢} (G)$
6		mirval.g	$⊢ φ \to G \in 𝒢_{Tarski}$
7		mirconn.m	$⊢ M = S (A)$
8		mirconn.a	$⊢ φ \to A \in P$
9		mirconn.x	$⊢ φ \to X \in P$
10		mirconn.y	$⊢ φ \to Y \in P$
11		mirconn.1	$⊢ φ \to (X \in (A I Y) \lor Y \in (A I X))$
12	6	adantr	$⊢ (φ \land X \in (A I Y)) \to G \in 𝒢_{Tarski}$
13	9	adantr	$⊢ (φ \land X \in (A I Y)) \to X \in P$
14	8	adantr	$⊢ (φ \land X \in (A I Y)) \to A \in P$
15	1 2 3 4 5 6 8 7 10	mircl	$⊢ φ \to M (Y) \in P$
16	15	adantr	$⊢ (φ \land X \in (A I Y)) \to M (Y) \in P$
17	10	adantr	$⊢ (φ \land X \in (A I Y)) \to Y \in P$
18		simpr	$⊢ (φ \land X \in (A I Y)) \to X \in (A I Y)$
19	1 2 3 4 5 6 8 7 10	mirbtwn	$⊢ φ \to A \in (M (Y) I Y)$
20	19	adantr	$⊢ (φ \land X \in (A I Y)) \to A \in (M (Y) I Y)$
21	1 2 3 12 13 14 16 17 18 20	tgbtwnintr	$⊢ (φ \land X \in (A I Y)) \to A \in (X I M (Y))$
22	1 2 3 6 9 8	tgbtwntriv2	$⊢ φ \to A \in (X I A)$
23	22	adantr	$⊢ (φ \land Y = A) \to A \in (X I A)$
24		simpr	$⊢ (φ \land Y = A) \to Y = A$
25	24	fveq2d	$⊢ (φ \land Y = A) \to M (Y) = M (A)$
26	1 2 3 4 5 6 8 7	mircinv	$⊢ φ \to M (A) = A$
27	26	adantr	$⊢ (φ \land Y = A) \to M (A) = A$
28	25 27	eqtrd	$⊢ (φ \land Y = A) \to M (Y) = A$
29	28	oveq2d	$⊢ (φ \land Y = A) \to X I M (Y) = X I A$
30	23 29	eleqtrrd	$⊢ (φ \land Y = A) \to A \in (X I M (Y))$
31	30	adantlr	$⊢ ((φ \land Y \in (A I X)) \land Y = A) \to A \in (X I M (Y))$
32	6	ad2antrr	$⊢ ((φ \land Y \in (A I X)) \land Y \neq A) \to G \in 𝒢_{Tarski}$
33	9	ad2antrr	$⊢ ((φ \land Y \in (A I X)) \land Y \neq A) \to X \in P$
34	10	ad2antrr	$⊢ ((φ \land Y \in (A I X)) \land Y \neq A) \to Y \in P$
35	8	ad2antrr	$⊢ ((φ \land Y \in (A I X)) \land Y \neq A) \to A \in P$
36	15	ad2antrr	$⊢ ((φ \land Y \in (A I X)) \land Y \neq A) \to M (Y) \in P$
37		simpr	$⊢ ((φ \land Y \in (A I X)) \land Y \neq A) \to Y \neq A$
38		simplr	$⊢ ((φ \land Y \in (A I X)) \land Y \neq A) \to Y \in (A I X)$
39	1 2 3 32 35 34 33 38	tgbtwncom	$⊢ ((φ \land Y \in (A I X)) \land Y \neq A) \to Y \in (X I A)$
40	1 2 3 6 15 8 10 19	tgbtwncom	$⊢ φ \to A \in (Y I M (Y))$
41	40	ad2antrr	$⊢ ((φ \land Y \in (A I X)) \land Y \neq A) \to A \in (Y I M (Y))$
42	1 2 3 32 33 34 35 36 37 39 41	tgbtwnouttr2	$⊢ ((φ \land Y \in (A I X)) \land Y \neq A) \to A \in (X I M (Y))$
43	31 42	pm2.61dane	$⊢ (φ \land Y \in (A I X)) \to A \in (X I M (Y))$
44	21 43 11	mpjaodan	$⊢ φ \to A \in (X I M (Y))$

Metamath Proof Explorer

Theorem mirconn

Proof