krippenlem

Description: Lemma for krippen . We can assume krippen.7 "without loss of generality". (Contributed by Thierry Arnoux, 12-Aug-2019)

	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}$
	krippen.m	$⊢ M = S (X)$
	krippen.n	$⊢ N = S (Y)$
	krippen.a	$⊢ φ \to A \in P$
	krippen.b	$⊢ φ \to B \in P$
	krippen.c	$⊢ φ \to C \in P$
	krippen.e	$⊢ φ \to E \in P$
	krippen.f	$⊢ φ \to F \in P$
	krippen.x	$⊢ φ \to X \in P$
	krippen.y	$⊢ φ \to Y \in P$
	krippen.1	$⊢ φ \to C \in (A I E)$
	krippen.2	$⊢ φ \to C \in (B I F)$
	krippen.3	$⊢ φ \to C \underset{˙}{-} A = C \underset{˙}{-} B$
	krippen.4	$⊢ φ \to C \underset{˙}{-} E = C \underset{˙}{-} F$
	krippen.5	$⊢ φ \to B = M (A)$
	krippen.6	$⊢ φ \to F = N (E)$
	krippen.l	$⊢ \underset{˙}{\leq} = \leq_{𝒢} (G)$
	krippen.7	$⊢ φ \to (C \underset{˙}{-} A) \underset{˙}{\leq} (C \underset{˙}{-} E)$
Assertion	krippenlem	$⊢ φ \to C \in (X I 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		krippen.m	$⊢ M = S (X)$
8		krippen.n	$⊢ N = S (Y)$
9		krippen.a	$⊢ φ \to A \in P$
10		krippen.b	$⊢ φ \to B \in P$
11		krippen.c	$⊢ φ \to C \in P$
12		krippen.e	$⊢ φ \to E \in P$
13		krippen.f	$⊢ φ \to F \in P$
14		krippen.x	$⊢ φ \to X \in P$
15		krippen.y	$⊢ φ \to Y \in P$
16		krippen.1	$⊢ φ \to C \in (A I E)$
17		krippen.2	$⊢ φ \to C \in (B I F)$
18		krippen.3	$⊢ φ \to C \underset{˙}{-} A = C \underset{˙}{-} B$
19		krippen.4	$⊢ φ \to C \underset{˙}{-} E = C \underset{˙}{-} F$
20		krippen.5	$⊢ φ \to B = M (A)$
21		krippen.6	$⊢ φ \to F = N (E)$
22		krippen.l	$⊢ \underset{˙}{\leq} = \leq_{𝒢} (G)$
23		krippen.7	$⊢ φ \to (C \underset{˙}{-} A) \underset{˙}{\leq} (C \underset{˙}{-} E)$
24	16	adantr	$⊢ (φ \land E = C) \to C \in (A I E)$
25	6	adantr	$⊢ (φ \land E = C) \to G \in 𝒢_{Tarski}$
26	11	adantr	$⊢ (φ \land E = C) \to C \in P$
27	9	adantr	$⊢ (φ \land E = C) \to A \in P$
28	10	adantr	$⊢ (φ \land E = C) \to B \in P$
29	18	adantr	$⊢ (φ \land E = C) \to C \underset{˙}{-} A = C \underset{˙}{-} B$
30	23	adantr	$⊢ (φ \land E = C) \to (C \underset{˙}{-} A) \underset{˙}{\leq} (C \underset{˙}{-} E)$
31		simpr	$⊢ (φ \land E = C) \to E = C$
32	31	oveq2d	$⊢ (φ \land E = C) \to C \underset{˙}{-} E = C \underset{˙}{-} C$
33	30 32	breqtrd	$⊢ (φ \land E = C) \to (C \underset{˙}{-} A) \underset{˙}{\leq} (C \underset{˙}{-} C)$
34	1 2 3 22 25 26 27 26 28 33	legeq	$⊢ (φ \land E = C) \to C = A$
35	1 2 3 25 26 27 26 28 29 34	tgcgreq	$⊢ (φ \land E = C) \to C = B$
36	20	adantr	$⊢ (φ \land E = C) \to B = M (A)$
37	35 34 36	3eqtr3rd	$⊢ (φ \land E = C) \to M (A) = A$
38	14	adantr	$⊢ (φ \land E = C) \to X \in P$
39	1 2 3 4 5 25 38 7 27	mirinv	$⊢ (φ \land E = C) \to (M (A) = A \leftrightarrow X = A)$
40	37 39	mpbid	$⊢ (φ \land E = C) \to X = A$
41	13	adantr	$⊢ (φ \land E = C) \to F \in P$
42	19	adantr	$⊢ (φ \land E = C) \to C \underset{˙}{-} E = C \underset{˙}{-} F$
43	42 32	eqtr3d	$⊢ (φ \land E = C) \to C \underset{˙}{-} F = C \underset{˙}{-} C$
44	1 2 3 25 26 41 26 43	axtgcgrid	$⊢ (φ \land E = C) \to C = F$
45	21	adantr	$⊢ (φ \land E = C) \to F = N (E)$
46	31 44 45	3eqtrrd	$⊢ (φ \land E = C) \to N (E) = E$
47	15	adantr	$⊢ (φ \land E = C) \to Y \in P$
48	12	adantr	$⊢ (φ \land E = C) \to E \in P$
49	1 2 3 4 5 25 47 8 48	mirinv	$⊢ (φ \land E = C) \to (N (E) = E \leftrightarrow Y = E)$
50	46 49	mpbid	$⊢ (φ \land E = C) \to Y = E$
51	40 50	oveq12d	$⊢ (φ \land E = C) \to X I Y = A I E$
52	24 51	eleqtrrd	$⊢ (φ \land E = C) \to C \in (X I Y)$
53	6	adantr	$⊢ (φ \land E \neq C) \to G \in 𝒢_{Tarski}$
54	53	ad2antrr	$⊢ (((φ \land E \neq C) \land q \in P) \land (q \in (S (C) (Y) I C) \land q \in (A I B))) \to G \in 𝒢_{Tarski}$
55	11	adantr	$⊢ (φ \land E \neq C) \to C \in P$
56		eqid	$⊢ S (C) = S (C)$
57	1 2 3 4 5 53 55 56	mirf	$⊢ (φ \land E \neq C) \to S (C) : P ⟶ P$
58	15	adantr	$⊢ (φ \land E \neq C) \to Y \in P$
59	57 58	ffvelrnd	$⊢ (φ \land E \neq C) \to S (C) (Y) \in P$
60	59	ad2antrr	$⊢ (((φ \land E \neq C) \land q \in P) \land (q \in (S (C) (Y) I C) \land q \in (A I B))) \to S (C) (Y) \in P$
61		simplr	$⊢ (((φ \land E \neq C) \land q \in P) \land (q \in (S (C) (Y) I C) \land q \in (A I B))) \to q \in P$
62	55	ad2antrr	$⊢ (((φ \land E \neq C) \land q \in P) \land (q \in (S (C) (Y) I C) \land q \in (A I B))) \to C \in P$
63	58	ad2antrr	$⊢ (((φ \land E \neq C) \land q \in P) \land (q \in (S (C) (Y) I C) \land q \in (A I B))) \to Y \in P$
64		simprl	$⊢ (((φ \land E \neq C) \land q \in P) \land (q \in (S (C) (Y) I C) \land q \in (A I B))) \to q \in (S (C) (Y) I C)$
65	1 2 3 4 5 6 11 56 15	mirbtwn	$⊢ φ \to C \in (S (C) (Y) I Y)$
66	65	ad3antrrr	$⊢ (((φ \land E \neq C) \land q \in P) \land (q \in (S (C) (Y) I C) \land q \in (A I B))) \to C \in (S (C) (Y) I Y)$
67	1 2 3 54 60 61 62 63 64 66	tgbtwnexch3	$⊢ (((φ \land E \neq C) \land q \in P) \land (q \in (S (C) (Y) I C) \land q \in (A I B))) \to C \in (q I Y)$
68	14	ad3antrrr	$⊢ (((φ \land E \neq C) \land q \in P) \land (q \in (S (C) (Y) I C) \land q \in (A I B))) \to X \in P$
69	9	adantr	$⊢ (φ \land E \neq C) \to A \in P$
70	69	ad2antrr	$⊢ (((φ \land E \neq C) \land q \in P) \land (q \in (S (C) (Y) I C) \land q \in (A I B))) \to A \in P$
71	10	adantr	$⊢ (φ \land E \neq C) \to B \in P$
72	71	ad2antrr	$⊢ (((φ \land E \neq C) \land q \in P) \land (q \in (S (C) (Y) I C) \land q \in (A I B))) \to B \in P$
73		eqid	$⊢ S (q) = S (q)$
74	12	adantr	$⊢ (φ \land E \neq C) \to E \in P$
75	57 74	ffvelrnd	$⊢ (φ \land E \neq C) \to S (C) (E) \in P$
76	13	adantr	$⊢ (φ \land E \neq C) \to F \in P$
77	57 76	ffvelrnd	$⊢ (φ \land E \neq C) \to S (C) (F) \in P$
78	6	ad2antrr	$⊢ ((φ \land E \neq C) \land A = C) \to G \in 𝒢_{Tarski}$
79	9	ad2antrr	$⊢ ((φ \land E \neq C) \land A = C) \to A \in P$
80	75	adantr	$⊢ ((φ \land E \neq C) \land A = C) \to S (C) (E) \in P$
81	1 2 3 78 79 80	tgbtwntriv1	$⊢ ((φ \land E \neq C) \land A = C) \to A \in (A I S (C) (E))$
82		simpr	$⊢ ((φ \land E \neq C) \land A = C) \to A = C$
83	82	oveq1d	$⊢ ((φ \land E \neq C) \land A = C) \to A I S (C) (E) = C I S (C) (E)$
84	81 83	eleqtrd	$⊢ ((φ \land E \neq C) \land A = C) \to A \in (C I S (C) (E))$
85	6	ad2antrr	$⊢ ((φ \land E \neq C) \land A \neq C) \to G \in 𝒢_{Tarski}$
86	9	ad2antrr	$⊢ ((φ \land E \neq C) \land A \neq C) \to A \in P$
87	75	adantr	$⊢ ((φ \land E \neq C) \land A \neq C) \to S (C) (E) \in P$
88	11	ad2antrr	$⊢ ((φ \land E \neq C) \land A \neq C) \to C \in P$
89	12	ad2antrr	$⊢ ((φ \land E \neq C) \land A \neq C) \to E \in P$
90		simplr	$⊢ ((φ \land E \neq C) \land A \neq C) \to E \neq C$
91	1 2 3 6 9 11 12 16	tgbtwncom	$⊢ φ \to C \in (E I A)$
92	91	ad2antrr	$⊢ ((φ \land E \neq C) \land A \neq C) \to C \in (E I A)$
93	1 2 3 4 5 85 88 56 89	mirbtwn	$⊢ ((φ \land E \neq C) \land A \neq C) \to C \in (S (C) (E) I E)$
94	1 2 3 85 87 88 89 93	tgbtwncom	$⊢ ((φ \land E \neq C) \land A \neq C) \to C \in (E I S (C) (E))$
95	1 3 85 89 88 86 87 90 92 94	tgbtwnconn2	$⊢ ((φ \land E \neq C) \land A \neq C) \to (A \in (C I S (C) (E)) \lor S (C) (E) \in (C I A))$
96	23	adantr	$⊢ (φ \land E \neq C) \to (C \underset{˙}{-} A) \underset{˙}{\leq} (C \underset{˙}{-} E)$
97	1 2 3 4 5 53 55 56 74	mircgr	$⊢ (φ \land E \neq C) \to C \underset{˙}{-} S (C) (E) = C \underset{˙}{-} E$
98	96 97	breqtrrd	$⊢ (φ \land E \neq C) \to (C \underset{˙}{-} A) \underset{˙}{\leq} (C \underset{˙}{-} S (C) (E))$
99	98	adantr	$⊢ ((φ \land E \neq C) \land A \neq C) \to (C \underset{˙}{-} A) \underset{˙}{\leq} (C \underset{˙}{-} S (C) (E))$
100	1 2 3 22 85 86 87 88 86 95 99	legbtwn	$⊢ ((φ \land E \neq C) \land A \neq C) \to A \in (C I S (C) (E))$
101	84 100	pm2.61dane	$⊢ (φ \land E \neq C) \to A \in (C I S (C) (E))$
102	1 2 3 53 55 69 75 101	tgbtwncom	$⊢ (φ \land E \neq C) \to A \in (S (C) (E) I C)$
103	6	ad2antrr	$⊢ ((φ \land E \neq C) \land B = C) \to G \in 𝒢_{Tarski}$
104	10	ad2antrr	$⊢ ((φ \land E \neq C) \land B = C) \to B \in P$
105	77	adantr	$⊢ ((φ \land E \neq C) \land B = C) \to S (C) (F) \in P$
106	1 2 3 103 104 105	tgbtwntriv1	$⊢ ((φ \land E \neq C) \land B = C) \to B \in (B I S (C) (F))$
107		simpr	$⊢ ((φ \land E \neq C) \land B = C) \to B = C$
108	107	oveq1d	$⊢ ((φ \land E \neq C) \land B = C) \to B I S (C) (F) = C I S (C) (F)$
109	106 108	eleqtrd	$⊢ ((φ \land E \neq C) \land B = C) \to B \in (C I S (C) (F))$
110	6	ad2antrr	$⊢ ((φ \land E \neq C) \land B \neq C) \to G \in 𝒢_{Tarski}$
111	10	ad2antrr	$⊢ ((φ \land E \neq C) \land B \neq C) \to B \in P$
112	77	adantr	$⊢ ((φ \land E \neq C) \land B \neq C) \to S (C) (F) \in P$
113	11	ad2antrr	$⊢ ((φ \land E \neq C) \land B \neq C) \to C \in P$
114	13	ad2antrr	$⊢ ((φ \land E \neq C) \land B \neq C) \to F \in P$
115	6	adantr	$⊢ (φ \land F = C) \to G \in 𝒢_{Tarski}$
116	11	adantr	$⊢ (φ \land F = C) \to C \in P$
117	12	adantr	$⊢ (φ \land F = C) \to E \in P$
118	19	adantr	$⊢ (φ \land F = C) \to C \underset{˙}{-} E = C \underset{˙}{-} F$
119		simpr	$⊢ (φ \land F = C) \to F = C$
120	119	oveq2d	$⊢ (φ \land F = C) \to C \underset{˙}{-} F = C \underset{˙}{-} C$
121	118 120	eqtrd	$⊢ (φ \land F = C) \to C \underset{˙}{-} E = C \underset{˙}{-} C$
122	1 2 3 115 116 117 116 121	axtgcgrid	$⊢ (φ \land F = C) \to C = E$
123	122	eqcomd	$⊢ (φ \land F = C) \to E = C$
124	123	adantlr	$⊢ ((φ \land E \neq C) \land F = C) \to E = C$
125		simplr	$⊢ ((φ \land E \neq C) \land F = C) \to E \neq C$
126	125	neneqd	$⊢ ((φ \land E \neq C) \land F = C) \to \neg E = C$
127	124 126	pm2.65da	$⊢ (φ \land E \neq C) \to \neg F = C$
128	127	neqned	$⊢ (φ \land E \neq C) \to F \neq C$
129	128	adantr	$⊢ ((φ \land E \neq C) \land B \neq C) \to F \neq C$
130	1 2 3 6 10 11 13 17	tgbtwncom	$⊢ φ \to C \in (F I B)$
131	130	ad2antrr	$⊢ ((φ \land E \neq C) \land B \neq C) \to C \in (F I B)$
132	1 2 3 4 5 110 113 56 114	mirbtwn	$⊢ ((φ \land E \neq C) \land B \neq C) \to C \in (S (C) (F) I F)$
133	1 2 3 110 112 113 114 132	tgbtwncom	$⊢ ((φ \land E \neq C) \land B \neq C) \to C \in (F I S (C) (F))$
134	1 3 110 114 113 111 112 129 131 133	tgbtwnconn2	$⊢ ((φ \land E \neq C) \land B \neq C) \to (B \in (C I S (C) (F)) \lor S (C) (F) \in (C I B))$
135	23 18 19	3brtr3d	$⊢ φ \to (C \underset{˙}{-} B) \underset{˙}{\leq} (C \underset{˙}{-} F)$
136	135	adantr	$⊢ (φ \land E \neq C) \to (C \underset{˙}{-} B) \underset{˙}{\leq} (C \underset{˙}{-} F)$
137	1 2 3 4 5 53 55 56 76	mircgr	$⊢ (φ \land E \neq C) \to C \underset{˙}{-} S (C) (F) = C \underset{˙}{-} F$
138	136 137	breqtrrd	$⊢ (φ \land E \neq C) \to (C \underset{˙}{-} B) \underset{˙}{\leq} (C \underset{˙}{-} S (C) (F))$
139	138	adantr	$⊢ ((φ \land E \neq C) \land B \neq C) \to (C \underset{˙}{-} B) \underset{˙}{\leq} (C \underset{˙}{-} S (C) (F))$
140	1 2 3 22 110 111 112 113 111 134 139	legbtwn	$⊢ ((φ \land E \neq C) \land B \neq C) \to B \in (C I S (C) (F))$
141	109 140	pm2.61dane	$⊢ (φ \land E \neq C) \to B \in (C I S (C) (F))$
142	1 2 3 53 55 71 77 141	tgbtwncom	$⊢ (φ \land E \neq C) \to B \in (S (C) (F) I C)$
143	19	adantr	$⊢ (φ \land E \neq C) \to C \underset{˙}{-} E = C \underset{˙}{-} F$
144	143 97 137	3eqtr4d	$⊢ (φ \land E \neq C) \to C \underset{˙}{-} S (C) (E) = C \underset{˙}{-} S (C) (F)$
145	1 2 3 53 55 75 55 77 144	tgcgrcomlr	$⊢ (φ \land E \neq C) \to S (C) (E) \underset{˙}{-} C = S (C) (F) \underset{˙}{-} C$
146	18	adantr	$⊢ (φ \land E \neq C) \to C \underset{˙}{-} A = C \underset{˙}{-} B$
147	1 2 3 53 55 69 55 71 146	tgcgrcomlr	$⊢ (φ \land E \neq C) \to A \underset{˙}{-} C = B \underset{˙}{-} C$
148		eqid	$⊢ S (S (C) (Y)) = S (S (C) (Y))$
149	1 2 3 4 5 53 59 148 75	mircgr	$⊢ (φ \land E \neq C) \to S (C) (Y) \underset{˙}{-} S (S (C) (Y)) (S (C) (E)) = S (C) (Y) \underset{˙}{-} S (C) (E)$
150		eqid	$⊢ S (C) (Y) = S (C) (Y)$
151		eqid	$⊢ S (C) (E) = S (C) (E)$
152		eqid	$⊢ S (C) (F) = S (C) (F)$
153	21	adantr	$⊢ (φ \land E \neq C) \to F = N (E)$
154	8	fveq1i	$⊢ N (E) = S (Y) (E)$
155	153 154	syl6req	$⊢ (φ \land E \neq C) \to S (Y) (E) = F$
156	1 2 3 4 5 53 56 150 151 152 55 58 74 76 155	mirauto	$⊢ (φ \land E \neq C) \to S (S (C) (Y)) (S (C) (E)) = S (C) (F)$
157	156	oveq2d	$⊢ (φ \land E \neq C) \to S (C) (Y) \underset{˙}{-} S (S (C) (Y)) (S (C) (E)) = S (C) (Y) \underset{˙}{-} S (C) (F)$
158	149 157	eqtr3d	$⊢ (φ \land E \neq C) \to S (C) (Y) \underset{˙}{-} S (C) (E) = S (C) (Y) \underset{˙}{-} S (C) (F)$
159	1 2 3 53 59 75 59 77 158	tgcgrcomlr	$⊢ (φ \land E \neq C) \to S (C) (E) \underset{˙}{-} S (C) (Y) = S (C) (F) \underset{˙}{-} S (C) (Y)$
160		eqidd	$⊢ (φ \land E \neq C) \to C \underset{˙}{-} S (C) (Y) = C \underset{˙}{-} S (C) (Y)$
161	1 2 3 53 75 69 55 59 77 71 55 59 102 142 145 147 159 160	tgifscgr	$⊢ (φ \land E \neq C) \to A \underset{˙}{-} S (C) (Y) = B \underset{˙}{-} S (C) (Y)$
162	1 2 3 53 69 59 71 59 161	tgcgrcomlr	$⊢ (φ \land E \neq C) \to S (C) (Y) \underset{˙}{-} A = S (C) (Y) \underset{˙}{-} B$
163	162	ad3antrrr	$⊢ ((((φ \land E \neq C) \land q \in P) \land (q \in (S (C) (Y) I C) \land q \in (A I B))) \land S (C) (Y) = C) \to S (C) (Y) \underset{˙}{-} A = S (C) (Y) \underset{˙}{-} B$
164	54	adantr	$⊢ ((((φ \land E \neq C) \land q \in P) \land (q \in (S (C) (Y) I C) \land q \in (A I B))) \land S (C) (Y) = C) \to G \in 𝒢_{Tarski}$
165	60	adantr	$⊢ ((((φ \land E \neq C) \land q \in P) \land (q \in (S (C) (Y) I C) \land q \in (A I B))) \land S (C) (Y) = C) \to S (C) (Y) \in P$
166	61	adantr	$⊢ ((((φ \land E \neq C) \land q \in P) \land (q \in (S (C) (Y) I C) \land q \in (A I B))) \land S (C) (Y) = C) \to q \in P$
167	64	adantr	$⊢ ((((φ \land E \neq C) \land q \in P) \land (q \in (S (C) (Y) I C) \land q \in (A I B))) \land S (C) (Y) = C) \to q \in (S (C) (Y) I C)$
168		simpr	$⊢ ((((φ \land E \neq C) \land q \in P) \land (q \in (S (C) (Y) I C) \land q \in (A I B))) \land S (C) (Y) = C) \to S (C) (Y) = C$
169	168	oveq2d	$⊢ ((((φ \land E \neq C) \land q \in P) \land (q \in (S (C) (Y) I C) \land q \in (A I B))) \land S (C) (Y) = C) \to S (C) (Y) I S (C) (Y) = S (C) (Y) I C$
170	167 169	eleqtrrd	$⊢ ((((φ \land E \neq C) \land q \in P) \land (q \in (S (C) (Y) I C) \land q \in (A I B))) \land S (C) (Y) = C) \to q \in (S (C) (Y) I S (C) (Y))$
171	1 2 3 164 165 166 170	axtgbtwnid	$⊢ ((((φ \land E \neq C) \land q \in P) \land (q \in (S (C) (Y) I C) \land q \in (A I B))) \land S (C) (Y) = C) \to S (C) (Y) = q$
172	171	oveq1d	$⊢ ((((φ \land E \neq C) \land q \in P) \land (q \in (S (C) (Y) I C) \land q \in (A I B))) \land S (C) (Y) = C) \to S (C) (Y) \underset{˙}{-} A = q \underset{˙}{-} A$
173	171	oveq1d	$⊢ ((((φ \land E \neq C) \land q \in P) \land (q \in (S (C) (Y) I C) \land q \in (A I B))) \land S (C) (Y) = C) \to S (C) (Y) \underset{˙}{-} B = q \underset{˙}{-} B$
174	163 172 173	3eqtr3d	$⊢ ((((φ \land E \neq C) \land q \in P) \land (q \in (S (C) (Y) I C) \land q \in (A I B))) \land S (C) (Y) = C) \to q \underset{˙}{-} A = q \underset{˙}{-} B$
175	53	ad3antrrr	$⊢ ((((φ \land E \neq C) \land q \in P) \land (q \in (S (C) (Y) I C) \land q \in (A I B))) \land S (C) (Y) \neq C) \to G \in 𝒢_{Tarski}$
176	59	ad3antrrr	$⊢ ((((φ \land E \neq C) \land q \in P) \land (q \in (S (C) (Y) I C) \land q \in (A I B))) \land S (C) (Y) \neq C) \to S (C) (Y) \in P$
177	55	ad3antrrr	$⊢ ((((φ \land E \neq C) \land q \in P) \land (q \in (S (C) (Y) I C) \land q \in (A I B))) \land S (C) (Y) \neq C) \to C \in P$
178	61	adantr	$⊢ ((((φ \land E \neq C) \land q \in P) \land (q \in (S (C) (Y) I C) \land q \in (A I B))) \land S (C) (Y) \neq C) \to q \in P$
179		eqid	$⊢ \sim_{𝒢} (G) = \sim_{𝒢} (G)$
180	69	ad3antrrr	$⊢ ((((φ \land E \neq C) \land q \in P) \land (q \in (S (C) (Y) I C) \land q \in (A I B))) \land S (C) (Y) \neq C) \to A \in P$
181	71	ad3antrrr	$⊢ ((((φ \land E \neq C) \land q \in P) \land (q \in (S (C) (Y) I C) \land q \in (A I B))) \land S (C) (Y) \neq C) \to B \in P$
182		simpr	$⊢ ((((φ \land E \neq C) \land q \in P) \land (q \in (S (C) (Y) I C) \land q \in (A I B))) \land S (C) (Y) \neq C) \to S (C) (Y) \neq C$
183	60	adantr	$⊢ ((((φ \land E \neq C) \land q \in P) \land (q \in (S (C) (Y) I C) \land q \in (A I B))) \land S (C) (Y) \neq C) \to S (C) (Y) \in P$
184	64	adantr	$⊢ ((((φ \land E \neq C) \land q \in P) \land (q \in (S (C) (Y) I C) \land q \in (A I B))) \land S (C) (Y) \neq C) \to q \in (S (C) (Y) I C)$
185	1 4 3 175 183 178 177 184	btwncolg3	$⊢ ((((φ \land E \neq C) \land q \in P) \land (q \in (S (C) (Y) I C) \land q \in (A I B))) \land S (C) (Y) \neq C) \to (C \in (S (C) (Y) L q) \lor S (C) (Y) = q)$
186	162	ad3antrrr	$⊢ ((((φ \land E \neq C) \land q \in P) \land (q \in (S (C) (Y) I C) \land q \in (A I B))) \land S (C) (Y) \neq C) \to S (C) (Y) \underset{˙}{-} A = S (C) (Y) \underset{˙}{-} B$
187	146	ad3antrrr	$⊢ ((((φ \land E \neq C) \land q \in P) \land (q \in (S (C) (Y) I C) \land q \in (A I B))) \land S (C) (Y) \neq C) \to C \underset{˙}{-} A = C \underset{˙}{-} B$
188	1 4 3 175 176 177 178 179 180 181 2 182 185 186 187	lncgr	$⊢ ((((φ \land E \neq C) \land q \in P) \land (q \in (S (C) (Y) I C) \land q \in (A I B))) \land S (C) (Y) \neq C) \to q \underset{˙}{-} A = q \underset{˙}{-} B$
189	174 188	pm2.61dane	$⊢ (((φ \land E \neq C) \land q \in P) \land (q \in (S (C) (Y) I C) \land q \in (A I B))) \to q \underset{˙}{-} A = q \underset{˙}{-} B$
190	189	eqcomd	$⊢ (((φ \land E \neq C) \land q \in P) \land (q \in (S (C) (Y) I C) \land q \in (A I B))) \to q \underset{˙}{-} B = q \underset{˙}{-} A$
191		simprr	$⊢ (((φ \land E \neq C) \land q \in P) \land (q \in (S (C) (Y) I C) \land q \in (A I B))) \to q \in (A I B)$
192	1 2 3 54 70 61 72 191	tgbtwncom	$⊢ (((φ \land E \neq C) \land q \in P) \land (q \in (S (C) (Y) I C) \land q \in (A I B))) \to q \in (B I A)$
193	1 2 3 4 5 54 61 73 70 72 190 192	ismir	$⊢ (((φ \land E \neq C) \land q \in P) \land (q \in (S (C) (Y) I C) \land q \in (A I B))) \to B = S (q) (A)$
194	193	eqcomd	$⊢ (((φ \land E \neq C) \land q \in P) \land (q \in (S (C) (Y) I C) \land q \in (A I B))) \to S (q) (A) = B$
195	20	ad3antrrr	$⊢ (((φ \land E \neq C) \land q \in P) \land (q \in (S (C) (Y) I C) \land q \in (A I B))) \to B = M (A)$
196	7	fveq1i	$⊢ M (A) = S (X) (A)$
197	195 196	syl6req	$⊢ (((φ \land E \neq C) \land q \in P) \land (q \in (S (C) (Y) I C) \land q \in (A I B))) \to S (X) (A) = B$
198	1 2 3 4 5 54 61 68 70 72 194 197	miduniq	$⊢ (((φ \land E \neq C) \land q \in P) \land (q \in (S (C) (Y) I C) \land q \in (A I B))) \to q = X$
199	198	oveq1d	$⊢ (((φ \land E \neq C) \land q \in P) \land (q \in (S (C) (Y) I C) \land q \in (A I B))) \to q I Y = X I Y$
200	67 199	eleqtrd	$⊢ (((φ \land E \neq C) \land q \in P) \land (q \in (S (C) (Y) I C) \land q \in (A I B))) \to C \in (X I Y)$
201	1 2 3 4 5 53 58 8 74	mirbtwn	$⊢ (φ \land E \neq C) \to Y \in (N (E) I E)$
202	153	oveq1d	$⊢ (φ \land E \neq C) \to F I E = N (E) I E$
203	201 202	eleqtrrd	$⊢ (φ \land E \neq C) \to Y \in (F I E)$
204	1 2 3 53 76 58 74 203	tgbtwncom	$⊢ (φ \land E \neq C) \to Y \in (E I F)$
205	1 2 3 4 5 53 55 56 74 58 76 204	mirbtwni	$⊢ (φ \land E \neq C) \to S (C) (Y) \in (S (C) (E) I S (C) (F))$
206	1 2 3 53 75 69 55 77 71 59 102 142 205	tgtrisegint	$⊢ (φ \land E \neq C) \to \exists q \in P (q \in (S (C) (Y) I C) \land q \in (A I B))$
207	200 206	r19.29a	$⊢ (φ \land E \neq C) \to C \in (X I Y)$
208	52 207	pm2.61dane	$⊢ φ \to C \in (X I Y)$

Metamath Proof Explorer

Theorem krippenlem

Proof