opphllem3

Description: Lemma for opphl : We assume opphllem3.l "without loss of generality". (Contributed by Thierry Arnoux, 21-Feb-2020)

	Ref	Expression
Hypotheses	hpg.p	$⊢ P = {Base}_{G}$
	hpg.d	$⊢ \underset{˙}{-} = dist (G)$
	hpg.i	$⊢ I = Itv (G)$
	hpg.o	$⊢ O = \{⟨a, b⟩ \| ((a \in (P ∖ D) \land b \in (P ∖ D)) \land \exists t \in D t \in (a I b))\}$
	opphl.l	$⊢ L = {Line}_{𝒢} (G)$
	opphl.d	$⊢ φ \to D \in ran L$
	opphl.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	opphl.k	$⊢ K = {hl}_{𝒢} (G)$
	opphllem5.n	$⊢ N = {pInv}_{𝒢} (G) (M)$
	opphllem5.a	$⊢ φ \to A \in P$
	opphllem5.c	$⊢ φ \to C \in P$
	opphllem5.r	$⊢ φ \to R \in D$
	opphllem5.s	$⊢ φ \to S \in D$
	opphllem5.m	$⊢ φ \to M \in P$
	opphllem5.o	$⊢ φ \to A O C$
	opphllem5.p	$⊢ φ \to D ⟂_{𝒢} (G) (A L R)$
	opphllem5.q	$⊢ φ \to D ⟂_{𝒢} (G) (C L S)$
	opphllem3.t	$⊢ φ \to R \neq S$
	opphllem3.l	$⊢ φ \to (S \underset{˙}{-} C) \leq_{𝒢} (G) (R \underset{˙}{-} A)$
	opphllem3.u	$⊢ φ \to U \in P$
	opphllem3.v	$⊢ φ \to N (R) = S$
Assertion	opphllem3	$⊢ φ \to (U K (R) A \leftrightarrow N (U) K (S) C)$

Proof

Step	Hyp	Ref	Expression
1		hpg.p	$⊢ P = {Base}_{G}$
2		hpg.d	$⊢ \underset{˙}{-} = dist (G)$
3		hpg.i	$⊢ I = Itv (G)$
4		hpg.o	$⊢ O = \{⟨a, b⟩ \| ((a \in (P ∖ D) \land b \in (P ∖ D)) \land \exists t \in D t \in (a I b))\}$
5		opphl.l	$⊢ L = {Line}_{𝒢} (G)$
6		opphl.d	$⊢ φ \to D \in ran L$
7		opphl.g	$⊢ φ \to G \in 𝒢_{Tarski}$
8		opphl.k	$⊢ K = {hl}_{𝒢} (G)$
9		opphllem5.n	$⊢ N = {pInv}_{𝒢} (G) (M)$
10		opphllem5.a	$⊢ φ \to A \in P$
11		opphllem5.c	$⊢ φ \to C \in P$
12		opphllem5.r	$⊢ φ \to R \in D$
13		opphllem5.s	$⊢ φ \to S \in D$
14		opphllem5.m	$⊢ φ \to M \in P$
15		opphllem5.o	$⊢ φ \to A O C$
16		opphllem5.p	$⊢ φ \to D ⟂_{𝒢} (G) (A L R)$
17		opphllem5.q	$⊢ φ \to D ⟂_{𝒢} (G) (C L S)$
18		opphllem3.t	$⊢ φ \to R \neq S$
19		opphllem3.l	$⊢ φ \to (S \underset{˙}{-} C) \leq_{𝒢} (G) (R \underset{˙}{-} A)$
20		opphllem3.u	$⊢ φ \to U \in P$
21		opphllem3.v	$⊢ φ \to N (R) = S$
22	20	ad4antr	$⊢ ((((φ \land t \in D) \land t \in (A I C)) \land p \in P) \land (p \in (R I A) \land S \underset{˙}{-} C = R \underset{˙}{-} p)) \to U \in P$
23	10	ad4antr	$⊢ ((((φ \land t \in D) \land t \in (A I C)) \land p \in P) \land (p \in (R I A) \land S \underset{˙}{-} C = R \underset{˙}{-} p)) \to A \in P$
24	1 5 3 7 6 12	tglnpt	$⊢ φ \to R \in P$
25	24	ad4antr	$⊢ ((((φ \land t \in D) \land t \in (A I C)) \land p \in P) \land (p \in (R I A) \land S \underset{˙}{-} C = R \underset{˙}{-} p)) \to R \in P$
26	7	ad4antr	$⊢ ((((φ \land t \in D) \land t \in (A I C)) \land p \in P) \land (p \in (R I A) \land S \underset{˙}{-} C = R \underset{˙}{-} p)) \to G \in 𝒢_{Tarski}$
27		simplr	$⊢ ((((φ \land t \in D) \land t \in (A I C)) \land p \in P) \land (p \in (R I A) \land S \underset{˙}{-} C = R \underset{˙}{-} p)) \to p \in P$
28		simprl	$⊢ ((((φ \land t \in D) \land t \in (A I C)) \land p \in P) \land (p \in (R I A) \land S \underset{˙}{-} C = R \underset{˙}{-} p)) \to p \in (R I A)$
29	5 7 16	perpln2	$⊢ φ \to A L R \in ran L$
30	1 3 5 7 10 24 29	tglnne	$⊢ φ \to A \neq R$
31	30	ad4antr	$⊢ ((((φ \land t \in D) \land t \in (A I C)) \land p \in P) \land (p \in (R I A) \land S \underset{˙}{-} C = R \underset{˙}{-} p)) \to A \neq R$
32	11	ad4antr	$⊢ ((((φ \land t \in D) \land t \in (A I C)) \land p \in P) \land (p \in (R I A) \land S \underset{˙}{-} C = R \underset{˙}{-} p)) \to C \in P$
33	1 5 3 7 6 13	tglnpt	$⊢ φ \to S \in P$
34	33	ad4antr	$⊢ ((((φ \land t \in D) \land t \in (A I C)) \land p \in P) \land (p \in (R I A) \land S \underset{˙}{-} C = R \underset{˙}{-} p)) \to S \in P$
35		simprr	$⊢ ((((φ \land t \in D) \land t \in (A I C)) \land p \in P) \land (p \in (R I A) \land S \underset{˙}{-} C = R \underset{˙}{-} p)) \to S \underset{˙}{-} C = R \underset{˙}{-} p$
36	1 2 3 26 34 32 25 27 35	tgcgrcomlr	$⊢ ((((φ \land t \in D) \land t \in (A I C)) \land p \in P) \land (p \in (R I A) \land S \underset{˙}{-} C = R \underset{˙}{-} p)) \to C \underset{˙}{-} S = p \underset{˙}{-} R$
37	17	ad4antr	$⊢ ((((φ \land t \in D) \land t \in (A I C)) \land p \in P) \land (p \in (R I A) \land S \underset{˙}{-} C = R \underset{˙}{-} p)) \to D ⟂_{𝒢} (G) (C L S)$
38	5 26 37	perpln2	$⊢ ((((φ \land t \in D) \land t \in (A I C)) \land p \in P) \land (p \in (R I A) \land S \underset{˙}{-} C = R \underset{˙}{-} p)) \to C L S \in ran L$
39	1 3 5 26 32 34 38	tglnne	$⊢ ((((φ \land t \in D) \land t \in (A I C)) \land p \in P) \land (p \in (R I A) \land S \underset{˙}{-} C = R \underset{˙}{-} p)) \to C \neq S$
40	1 2 3 26 32 34 27 25 36 39	tgcgrneq	$⊢ ((((φ \land t \in D) \land t \in (A I C)) \land p \in P) \land (p \in (R I A) \land S \underset{˙}{-} C = R \underset{˙}{-} p)) \to p \neq R$
41	1 3 8 22 23 25 26 27 28 31 40	hlbtwn	$⊢ ((((φ \land t \in D) \land t \in (A I C)) \land p \in P) \land (p \in (R I A) \land S \underset{˙}{-} C = R \underset{˙}{-} p)) \to (U K (R) A \leftrightarrow U K (R) p)$
42		eqid	$⊢ {pInv}_{𝒢} (G) = {pInv}_{𝒢} (G)$
43	26	adantr	$⊢ (((((φ \land t \in D) \land t \in (A I C)) \land p \in P) \land (p \in (R I A) \land S \underset{˙}{-} C = R \underset{˙}{-} p)) \land U K (R) p) \to G \in 𝒢_{Tarski}$
44	14	ad5antr	$⊢ (((((φ \land t \in D) \land t \in (A I C)) \land p \in P) \land (p \in (R I A) \land S \underset{˙}{-} C = R \underset{˙}{-} p)) \land U K (R) p) \to M \in P$
45	22	adantr	$⊢ (((((φ \land t \in D) \land t \in (A I C)) \land p \in P) \land (p \in (R I A) \land S \underset{˙}{-} C = R \underset{˙}{-} p)) \land U K (R) p) \to U \in P$
46		simpllr	$⊢ (((((φ \land t \in D) \land t \in (A I C)) \land p \in P) \land (p \in (R I A) \land S \underset{˙}{-} C = R \underset{˙}{-} p)) \land U K (R) p) \to p \in P$
47	25	adantr	$⊢ (((((φ \land t \in D) \land t \in (A I C)) \land p \in P) \land (p \in (R I A) \land S \underset{˙}{-} C = R \underset{˙}{-} p)) \land U K (R) p) \to R \in P$
48		simpr	$⊢ (((((φ \land t \in D) \land t \in (A I C)) \land p \in P) \land (p \in (R I A) \land S \underset{˙}{-} C = R \underset{˙}{-} p)) \land U K (R) p) \to U K (R) p$
49	1 2 3 5 42 43 9 8 44 45 46 47 48	mirhl	$⊢ (((((φ \land t \in D) \land t \in (A I C)) \land p \in P) \land (p \in (R I A) \land S \underset{˙}{-} C = R \underset{˙}{-} p)) \land U K (R) p) \to N (U) K (N (R)) N (p)$
50		eqidd	$⊢ (((((φ \land t \in D) \land t \in (A I C)) \land p \in P) \land (p \in (R I A) \land S \underset{˙}{-} C = R \underset{˙}{-} p)) \land U K (R) p) \to N (U) = N (U)$
51	21	ad5antr	$⊢ (((((φ \land t \in D) \land t \in (A I C)) \land p \in P) \land (p \in (R I A) \land S \underset{˙}{-} C = R \underset{˙}{-} p)) \land U K (R) p) \to N (R) = S$
52	51	fveq2d	$⊢ (((((φ \land t \in D) \land t \in (A I C)) \land p \in P) \land (p \in (R I A) \land S \underset{˙}{-} C = R \underset{˙}{-} p)) \land U K (R) p) \to K (N (R)) = K (S)$
53		simprr	$⊢ ((((((φ \land t \in D) \land t \in (A I C)) \land p \in P) \land (p \in (R I A) \land S \underset{˙}{-} C = R \underset{˙}{-} p)) \land m \in P) \land (R = {pInv}_{𝒢} (G) (m) (S) \land C = {pInv}_{𝒢} (G) (m) (p))) \to C = {pInv}_{𝒢} (G) (m) (p)$
54	26	ad2antrr	$⊢ ((((((φ \land t \in D) \land t \in (A I C)) \land p \in P) \land (p \in (R I A) \land S \underset{˙}{-} C = R \underset{˙}{-} p)) \land m \in P) \land (R = {pInv}_{𝒢} (G) (m) (S) \land C = {pInv}_{𝒢} (G) (m) (p))) \to G \in 𝒢_{Tarski}$
55		simplr	$⊢ ((((((φ \land t \in D) \land t \in (A I C)) \land p \in P) \land (p \in (R I A) \land S \underset{˙}{-} C = R \underset{˙}{-} p)) \land m \in P) \land (R = {pInv}_{𝒢} (G) (m) (S) \land C = {pInv}_{𝒢} (G) (m) (p))) \to m \in P$
56	14	ad6antr	$⊢ ((((((φ \land t \in D) \land t \in (A I C)) \land p \in P) \land (p \in (R I A) \land S \underset{˙}{-} C = R \underset{˙}{-} p)) \land m \in P) \land (R = {pInv}_{𝒢} (G) (m) (S) \land C = {pInv}_{𝒢} (G) (m) (p))) \to M \in P$
57	34	ad2antrr	$⊢ ((((((φ \land t \in D) \land t \in (A I C)) \land p \in P) \land (p \in (R I A) \land S \underset{˙}{-} C = R \underset{˙}{-} p)) \land m \in P) \land (R = {pInv}_{𝒢} (G) (m) (S) \land C = {pInv}_{𝒢} (G) (m) (p))) \to S \in P$
58	25	ad2antrr	$⊢ ((((((φ \land t \in D) \land t \in (A I C)) \land p \in P) \land (p \in (R I A) \land S \underset{˙}{-} C = R \underset{˙}{-} p)) \land m \in P) \land (R = {pInv}_{𝒢} (G) (m) (S) \land C = {pInv}_{𝒢} (G) (m) (p))) \to R \in P$
59		simprl	$⊢ ((((((φ \land t \in D) \land t \in (A I C)) \land p \in P) \land (p \in (R I A) \land S \underset{˙}{-} C = R \underset{˙}{-} p)) \land m \in P) \land (R = {pInv}_{𝒢} (G) (m) (S) \land C = {pInv}_{𝒢} (G) (m) (p))) \to R = {pInv}_{𝒢} (G) (m) (S)$
60	59	eqcomd	$⊢ ((((((φ \land t \in D) \land t \in (A I C)) \land p \in P) \land (p \in (R I A) \land S \underset{˙}{-} C = R \underset{˙}{-} p)) \land m \in P) \land (R = {pInv}_{𝒢} (G) (m) (S) \land C = {pInv}_{𝒢} (G) (m) (p))) \to {pInv}_{𝒢} (G) (m) (S) = R$
61	9	fveq1i	$⊢ N (S) = {pInv}_{𝒢} (G) (M) (S)$
62	1 2 3 5 42 7 14 9 24 21	mircom	$⊢ φ \to N (S) = R$
63	61 62	eqtr3id	$⊢ φ \to {pInv}_{𝒢} (G) (M) (S) = R$
64	63	ad6antr	$⊢ ((((((φ \land t \in D) \land t \in (A I C)) \land p \in P) \land (p \in (R I A) \land S \underset{˙}{-} C = R \underset{˙}{-} p)) \land m \in P) \land (R = {pInv}_{𝒢} (G) (m) (S) \land C = {pInv}_{𝒢} (G) (m) (p))) \to {pInv}_{𝒢} (G) (M) (S) = R$
65	1 2 3 5 42 54 55 56 57 58 60 64	miduniq	$⊢ ((((((φ \land t \in D) \land t \in (A I C)) \land p \in P) \land (p \in (R I A) \land S \underset{˙}{-} C = R \underset{˙}{-} p)) \land m \in P) \land (R = {pInv}_{𝒢} (G) (m) (S) \land C = {pInv}_{𝒢} (G) (m) (p))) \to m = M$
66	65	fveq2d	$⊢ ((((((φ \land t \in D) \land t \in (A I C)) \land p \in P) \land (p \in (R I A) \land S \underset{˙}{-} C = R \underset{˙}{-} p)) \land m \in P) \land (R = {pInv}_{𝒢} (G) (m) (S) \land C = {pInv}_{𝒢} (G) (m) (p))) \to {pInv}_{𝒢} (G) (m) = {pInv}_{𝒢} (G) (M)$
67	66 9	eqtr4di	$⊢ ((((((φ \land t \in D) \land t \in (A I C)) \land p \in P) \land (p \in (R I A) \land S \underset{˙}{-} C = R \underset{˙}{-} p)) \land m \in P) \land (R = {pInv}_{𝒢} (G) (m) (S) \land C = {pInv}_{𝒢} (G) (m) (p))) \to {pInv}_{𝒢} (G) (m) = N$
68	67	fveq1d	$⊢ ((((((φ \land t \in D) \land t \in (A I C)) \land p \in P) \land (p \in (R I A) \land S \underset{˙}{-} C = R \underset{˙}{-} p)) \land m \in P) \land (R = {pInv}_{𝒢} (G) (m) (S) \land C = {pInv}_{𝒢} (G) (m) (p))) \to {pInv}_{𝒢} (G) (m) (p) = N (p)$
69	53 68	eqtr2d	$⊢ ((((((φ \land t \in D) \land t \in (A I C)) \land p \in P) \land (p \in (R I A) \land S \underset{˙}{-} C = R \underset{˙}{-} p)) \land m \in P) \land (R = {pInv}_{𝒢} (G) (m) (S) \land C = {pInv}_{𝒢} (G) (m) (p))) \to N (p) = C$
70	18	ad4antr	$⊢ ((((φ \land t \in D) \land t \in (A I C)) \land p \in P) \land (p \in (R I A) \land S \underset{˙}{-} C = R \underset{˙}{-} p)) \to R \neq S$
71	70	necomd	$⊢ ((((φ \land t \in D) \land t \in (A I C)) \land p \in P) \land (p \in (R I A) \land S \underset{˙}{-} C = R \underset{˙}{-} p)) \to S \neq R$
72	6	ad4antr	$⊢ ((((φ \land t \in D) \land t \in (A I C)) \land p \in P) \land (p \in (R I A) \land S \underset{˙}{-} C = R \underset{˙}{-} p)) \to D \in ran L$
73		simp-4r	$⊢ ((((φ \land t \in D) \land t \in (A I C)) \land p \in P) \land (p \in (R I A) \land S \underset{˙}{-} C = R \underset{˙}{-} p)) \to t \in D$
74	1 5 3 26 72 73	tglnpt	$⊢ ((((φ \land t \in D) \land t \in (A I C)) \land p \in P) \land (p \in (R I A) \land S \underset{˙}{-} C = R \underset{˙}{-} p)) \to t \in P$
75	13	ad4antr	$⊢ ((((φ \land t \in D) \land t \in (A I C)) \land p \in P) \land (p \in (R I A) \land S \underset{˙}{-} C = R \underset{˙}{-} p)) \to S \in D$
76	12	ad4antr	$⊢ ((((φ \land t \in D) \land t \in (A I C)) \land p \in P) \land (p \in (R I A) \land S \underset{˙}{-} C = R \underset{˙}{-} p)) \to R \in D$
77	1 3 5 26 34 25 71 71 72 75 76	tglinethru	$⊢ ((((φ \land t \in D) \land t \in (A I C)) \land p \in P) \land (p \in (R I A) \land S \underset{˙}{-} C = R \underset{˙}{-} p)) \to D = S L R$
78	16	ad4antr	$⊢ ((((φ \land t \in D) \land t \in (A I C)) \land p \in P) \land (p \in (R I A) \land S \underset{˙}{-} C = R \underset{˙}{-} p)) \to D ⟂_{𝒢} (G) (A L R)$
79	77 78	eqbrtrrd	$⊢ ((((φ \land t \in D) \land t \in (A I C)) \land p \in P) \land (p \in (R I A) \land S \underset{˙}{-} C = R \underset{˙}{-} p)) \to (S L R) ⟂_{𝒢} (G) (A L R)$
80	1 3 5 26 32 34 39	tglinecom	$⊢ ((((φ \land t \in D) \land t \in (A I C)) \land p \in P) \land (p \in (R I A) \land S \underset{˙}{-} C = R \underset{˙}{-} p)) \to C L S = S L C$
81	37 77 80	3brtr3d	$⊢ ((((φ \land t \in D) \land t \in (A I C)) \land p \in P) \land (p \in (R I A) \land S \underset{˙}{-} C = R \underset{˙}{-} p)) \to (S L R) ⟂_{𝒢} (G) (S L C)$
82	73 77	eleqtrd	$⊢ ((((φ \land t \in D) \land t \in (A I C)) \land p \in P) \land (p \in (R I A) \land S \underset{˙}{-} C = R \underset{˙}{-} p)) \to t \in (S L R)$
83		simpllr	$⊢ ((((φ \land t \in D) \land t \in (A I C)) \land p \in P) \land (p \in (R I A) \land S \underset{˙}{-} C = R \underset{˙}{-} p)) \to t \in (A I C)$
84	1 2 3 5 26 42 34 25 71 23 32 74 79 81 82 83 27 28 35	opphllem	$⊢ ((((φ \land t \in D) \land t \in (A I C)) \land p \in P) \land (p \in (R I A) \land S \underset{˙}{-} C = R \underset{˙}{-} p)) \to \exists m \in P (R = {pInv}_{𝒢} (G) (m) (S) \land C = {pInv}_{𝒢} (G) (m) (p))$
85	69 84	r19.29a	$⊢ ((((φ \land t \in D) \land t \in (A I C)) \land p \in P) \land (p \in (R I A) \land S \underset{˙}{-} C = R \underset{˙}{-} p)) \to N (p) = C$
86	85	adantr	$⊢ (((((φ \land t \in D) \land t \in (A I C)) \land p \in P) \land (p \in (R I A) \land S \underset{˙}{-} C = R \underset{˙}{-} p)) \land U K (R) p) \to N (p) = C$
87	50 52 86	breq123d	$⊢ (((((φ \land t \in D) \land t \in (A I C)) \land p \in P) \land (p \in (R I A) \land S \underset{˙}{-} C = R \underset{˙}{-} p)) \land U K (R) p) \to (N (U) K (N (R)) N (p) \leftrightarrow N (U) K (S) C)$
88	49 87	mpbid	$⊢ (((((φ \land t \in D) \land t \in (A I C)) \land p \in P) \land (p \in (R I A) \land S \underset{˙}{-} C = R \underset{˙}{-} p)) \land U K (R) p) \to N (U) K (S) C$
89	26	adantr	$⊢ (((((φ \land t \in D) \land t \in (A I C)) \land p \in P) \land (p \in (R I A) \land S \underset{˙}{-} C = R \underset{˙}{-} p)) \land N (U) K (S) C) \to G \in 𝒢_{Tarski}$
90	14	ad5antr	$⊢ (((((φ \land t \in D) \land t \in (A I C)) \land p \in P) \land (p \in (R I A) \land S \underset{˙}{-} C = R \underset{˙}{-} p)) \land N (U) K (S) C) \to M \in P$
91	1 2 3 5 42 7 14 9 20	mircl	$⊢ φ \to N (U) \in P$
92	91	ad5antr	$⊢ (((((φ \land t \in D) \land t \in (A I C)) \land p \in P) \land (p \in (R I A) \land S \underset{˙}{-} C = R \underset{˙}{-} p)) \land N (U) K (S) C) \to N (U) \in P$
93	32	adantr	$⊢ (((((φ \land t \in D) \land t \in (A I C)) \land p \in P) \land (p \in (R I A) \land S \underset{˙}{-} C = R \underset{˙}{-} p)) \land N (U) K (S) C) \to C \in P$
94	34	adantr	$⊢ (((((φ \land t \in D) \land t \in (A I C)) \land p \in P) \land (p \in (R I A) \land S \underset{˙}{-} C = R \underset{˙}{-} p)) \land N (U) K (S) C) \to S \in P$
95		simpr	$⊢ (((((φ \land t \in D) \land t \in (A I C)) \land p \in P) \land (p \in (R I A) \land S \underset{˙}{-} C = R \underset{˙}{-} p)) \land N (U) K (S) C) \to N (U) K (S) C$
96	1 2 3 5 42 89 9 8 90 92 93 94 95	mirhl	$⊢ (((((φ \land t \in D) \land t \in (A I C)) \land p \in P) \land (p \in (R I A) \land S \underset{˙}{-} C = R \underset{˙}{-} p)) \land N (U) K (S) C) \to N (N (U)) K (N (S)) N (C)$
97	22	adantr	$⊢ (((((φ \land t \in D) \land t \in (A I C)) \land p \in P) \land (p \in (R I A) \land S \underset{˙}{-} C = R \underset{˙}{-} p)) \land N (U) K (S) C) \to U \in P$
98	1 2 3 5 42 89 90 9 97	mirmir	$⊢ (((((φ \land t \in D) \land t \in (A I C)) \land p \in P) \land (p \in (R I A) \land S \underset{˙}{-} C = R \underset{˙}{-} p)) \land N (U) K (S) C) \to N (N (U)) = U$
99	25	adantr	$⊢ (((((φ \land t \in D) \land t \in (A I C)) \land p \in P) \land (p \in (R I A) \land S \underset{˙}{-} C = R \underset{˙}{-} p)) \land N (U) K (S) C) \to R \in P$
100	21	ad5antr	$⊢ (((((φ \land t \in D) \land t \in (A I C)) \land p \in P) \land (p \in (R I A) \land S \underset{˙}{-} C = R \underset{˙}{-} p)) \land N (U) K (S) C) \to N (R) = S$
101	1 2 3 5 42 89 90 9 99 100	mircom	$⊢ (((((φ \land t \in D) \land t \in (A I C)) \land p \in P) \land (p \in (R I A) \land S \underset{˙}{-} C = R \underset{˙}{-} p)) \land N (U) K (S) C) \to N (S) = R$
102	101	fveq2d	$⊢ (((((φ \land t \in D) \land t \in (A I C)) \land p \in P) \land (p \in (R I A) \land S \underset{˙}{-} C = R \underset{˙}{-} p)) \land N (U) K (S) C) \to K (N (S)) = K (R)$
103		simpllr	$⊢ (((((φ \land t \in D) \land t \in (A I C)) \land p \in P) \land (p \in (R I A) \land S \underset{˙}{-} C = R \underset{˙}{-} p)) \land N (U) K (S) C) \to p \in P$
104	85	adantr	$⊢ (((((φ \land t \in D) \land t \in (A I C)) \land p \in P) \land (p \in (R I A) \land S \underset{˙}{-} C = R \underset{˙}{-} p)) \land N (U) K (S) C) \to N (p) = C$
105	1 2 3 5 42 89 90 9 103 104	mircom	$⊢ (((((φ \land t \in D) \land t \in (A I C)) \land p \in P) \land (p \in (R I A) \land S \underset{˙}{-} C = R \underset{˙}{-} p)) \land N (U) K (S) C) \to N (C) = p$
106	98 102 105	breq123d	$⊢ (((((φ \land t \in D) \land t \in (A I C)) \land p \in P) \land (p \in (R I A) \land S \underset{˙}{-} C = R \underset{˙}{-} p)) \land N (U) K (S) C) \to (N (N (U)) K (N (S)) N (C) \leftrightarrow U K (R) p)$
107	96 106	mpbid	$⊢ (((((φ \land t \in D) \land t \in (A I C)) \land p \in P) \land (p \in (R I A) \land S \underset{˙}{-} C = R \underset{˙}{-} p)) \land N (U) K (S) C) \to U K (R) p$
108	88 107	impbida	$⊢ ((((φ \land t \in D) \land t \in (A I C)) \land p \in P) \land (p \in (R I A) \land S \underset{˙}{-} C = R \underset{˙}{-} p)) \to (U K (R) p \leftrightarrow N (U) K (S) C)$
109	41 108	bitrd	$⊢ ((((φ \land t \in D) \land t \in (A I C)) \land p \in P) \land (p \in (R I A) \land S \underset{˙}{-} C = R \underset{˙}{-} p)) \to (U K (R) A \leftrightarrow N (U) K (S) C)$
110		eqid	$⊢ \leq_{𝒢} (G) = \leq_{𝒢} (G)$
111	1 2 3 110 7 33 11 24 10	legov	$⊢ φ \to ((S \underset{˙}{-} C) \leq_{𝒢} (G) (R \underset{˙}{-} A) \leftrightarrow \exists p \in P (p \in (R I A) \land S \underset{˙}{-} C = R \underset{˙}{-} p))$
112	19 111	mpbid	$⊢ φ \to \exists p \in P (p \in (R I A) \land S \underset{˙}{-} C = R \underset{˙}{-} p)$
113	112	ad2antrr	$⊢ ((φ \land t \in D) \land t \in (A I C)) \to \exists p \in P (p \in (R I A) \land S \underset{˙}{-} C = R \underset{˙}{-} p)$
114	109 113	r19.29a	$⊢ ((φ \land t \in D) \land t \in (A I C)) \to (U K (R) A \leftrightarrow N (U) K (S) C)$
115	1 2 3 4 10 11	islnopp	$⊢ φ \to (A O C \leftrightarrow ((\neg A \in D \land \neg C \in D) \land \exists t \in D t \in (A I C)))$
116	15 115	mpbid	$⊢ φ \to ((\neg A \in D \land \neg C \in D) \land \exists t \in D t \in (A I C))$
117	116	simprd	$⊢ φ \to \exists t \in D t \in (A I C)$
118	114 117	r19.29a	$⊢ φ \to (U K (R) A \leftrightarrow N (U) K (S) C)$

Metamath Proof Explorer

Theorem opphllem3

Proof