cdlemk12u

Description: Part of proof of Lemma K of Crawley p. 118. Line 18, p. 119, showing Eq. 4 (line 10, p. 119) for the sigma_1 ( U ) case. (Contributed by NM, 4-Jul-2013)

	Ref	Expression
Hypotheses	cdlemk1.b	$⊢ B = {Base}_{K}$
	cdlemk1.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdlemk1.j	$⊢ \underset{˙}{\lor} = join (K)$
	cdlemk1.m	$⊢ \underset{˙}{\land} = meet (K)$
	cdlemk1.a	$⊢ A = Atoms (K)$
	cdlemk1.h	$⊢ H = LHyp (K)$
	cdlemk1.t	$⊢ T = LTrn (K) (W)$
	cdlemk1.r	$⊢ R = trL (K) (W)$
	cdlemk1.s	$⊢ S = (f \in T ⟼ (ι i \in T \| i (P) = (P \underset{˙}{\lor} R (f)) \underset{˙}{\land} (N (P) \underset{˙}{\lor} R (f \circ F^{-1}))))$
	cdlemk1.o	$⊢ O = S (D)$
	cdlemk1.u	$⊢ U = (e \in T ⟼ (ι j \in T \| j (P) = (P \underset{˙}{\lor} R (e)) \underset{˙}{\land} (O (P) \underset{˙}{\lor} R (e \circ D^{-1}))))$
Assertion	cdlemk12u	$⊢ (((K \in HL \land W \in H) \land F \in T \land D \in T) \land ((N \in T \land G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land D \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (X \neq {I ↾}_{B} \land R (G) \neq R (X)) \land (R (D) \neq R (F) \land R (G) \neq R (D) \land R (X) \neq R (D)))) \to U (G) (P) = (P \underset{˙}{\lor} G (P)) \underset{˙}{\land} (U (X) (P) \underset{˙}{\lor} R (X \circ G^{-1}))$

Proof

Step	Hyp	Ref	Expression
1		cdlemk1.b	$⊢ B = {Base}_{K}$
2		cdlemk1.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		cdlemk1.j	$⊢ \underset{˙}{\lor} = join (K)$
4		cdlemk1.m	$⊢ \underset{˙}{\land} = meet (K)$
5		cdlemk1.a	$⊢ A = Atoms (K)$
6		cdlemk1.h	$⊢ H = LHyp (K)$
7		cdlemk1.t	$⊢ T = LTrn (K) (W)$
8		cdlemk1.r	$⊢ R = trL (K) (W)$
9		cdlemk1.s	$⊢ S = (f \in T ⟼ (ι i \in T \| i (P) = (P \underset{˙}{\lor} R (f)) \underset{˙}{\land} (N (P) \underset{˙}{\lor} R (f \circ F^{-1}))))$
10		cdlemk1.o	$⊢ O = S (D)$
11		cdlemk1.u	$⊢ U = (e \in T ⟼ (ι j \in T \| j (P) = (P \underset{˙}{\lor} R (e)) \underset{˙}{\land} (O (P) \underset{˙}{\lor} R (e \circ D^{-1}))))$
12		simp11l	$⊢ (((K \in HL \land W \in H) \land F \in T \land D \in T) \land ((N \in T \land G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land D \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (X \neq {I ↾}_{B} \land R (G) \neq R (X)) \land (R (D) \neq R (F) \land R (G) \neq R (D) \land R (X) \neq R (D)))) \to K \in HL$
13		simp22l	$⊢ (((K \in HL \land W \in H) \land F \in T \land D \in T) \land ((N \in T \land G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land D \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (X \neq {I ↾}_{B} \land R (G) \neq R (X)) \land (R (D) \neq R (F) \land R (G) \neq R (D) \land R (X) \neq R (D)))) \to P \in A$
14		simp11	$⊢ (((K \in HL \land W \in H) \land F \in T \land D \in T) \land ((N \in T \land G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land D \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (X \neq {I ↾}_{B} \land R (G) \neq R (X)) \land (R (D) \neq R (F) \land R (G) \neq R (D) \land R (X) \neq R (D)))) \to (K \in HL \land W \in H)$
15		simp212	$⊢ (((K \in HL \land W \in H) \land F \in T \land D \in T) \land ((N \in T \land G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land D \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (X \neq {I ↾}_{B} \land R (G) \neq R (X)) \land (R (D) \neq R (F) \land R (G) \neq R (D) \land R (X) \neq R (D)))) \to G \in T$
16	2 5 6 7	ltrnat	$⊢ ((K \in HL \land W \in H) \land G \in T \land P \in A) \to G (P) \in A$
17	14 15 13 16	syl3anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land D \in T) \land ((N \in T \land G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land D \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (X \neq {I ↾}_{B} \land R (G) \neq R (X)) \land (R (D) \neq R (F) \land R (G) \neq R (D) \land R (X) \neq R (D)))) \to G (P) \in A$
18		simp23	$⊢ (((K \in HL \land W \in H) \land F \in T \land D \in T) \land ((N \in T \land G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land D \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (X \neq {I ↾}_{B} \land R (G) \neq R (X)) \land (R (D) \neq R (F) \land R (G) \neq R (D) \land R (X) \neq R (D)))) \to R (F) = R (N)$
19		simp213	$⊢ (((K \in HL \land W \in H) \land F \in T \land D \in T) \land ((N \in T \land G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land D \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (X \neq {I ↾}_{B} \land R (G) \neq R (X)) \land (R (D) \neq R (F) \land R (G) \neq R (D) \land R (X) \neq R (D)))) \to X \in T$
20		simp12	$⊢ (((K \in HL \land W \in H) \land F \in T \land D \in T) \land ((N \in T \land G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land D \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (X \neq {I ↾}_{B} \land R (G) \neq R (X)) \land (R (D) \neq R (F) \land R (G) \neq R (D) \land R (X) \neq R (D)))) \to F \in T$
21		simp13	$⊢ (((K \in HL \land W \in H) \land F \in T \land D \in T) \land ((N \in T \land G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land D \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (X \neq {I ↾}_{B} \land R (G) \neq R (X)) \land (R (D) \neq R (F) \land R (G) \neq R (D) \land R (X) \neq R (D)))) \to D \in T$
22		simp211	$⊢ (((K \in HL \land W \in H) \land F \in T \land D \in T) \land ((N \in T \land G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land D \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (X \neq {I ↾}_{B} \land R (G) \neq R (X)) \land (R (D) \neq R (F) \land R (G) \neq R (D) \land R (X) \neq R (D)))) \to N \in T$
23		simp331	$⊢ (((K \in HL \land W \in H) \land F \in T \land D \in T) \land ((N \in T \land G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land D \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (X \neq {I ↾}_{B} \land R (G) \neq R (X)) \land (R (D) \neq R (F) \land R (G) \neq R (D) \land R (X) \neq R (D)))) \to R (D) \neq R (F)$
24		simp333	$⊢ (((K \in HL \land W \in H) \land F \in T \land D \in T) \land ((N \in T \land G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land D \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (X \neq {I ↾}_{B} \land R (G) \neq R (X)) \land (R (D) \neq R (F) \land R (G) \neq R (D) \land R (X) \neq R (D)))) \to R (X) \neq R (D)$
25	24	necomd	$⊢ (((K \in HL \land W \in H) \land F \in T \land D \in T) \land ((N \in T \land G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land D \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (X \neq {I ↾}_{B} \land R (G) \neq R (X)) \land (R (D) \neq R (F) \land R (G) \neq R (D) \land R (X) \neq R (D)))) \to R (D) \neq R (X)$
26	23 25	jca	$⊢ (((K \in HL \land W \in H) \land F \in T \land D \in T) \land ((N \in T \land G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land D \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (X \neq {I ↾}_{B} \land R (G) \neq R (X)) \land (R (D) \neq R (F) \land R (G) \neq R (D) \land R (X) \neq R (D)))) \to (R (D) \neq R (F) \land R (D) \neq R (X))$
27		simp311	$⊢ (((K \in HL \land W \in H) \land F \in T \land D \in T) \land ((N \in T \land G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land D \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (X \neq {I ↾}_{B} \land R (G) \neq R (X)) \land (R (D) \neq R (F) \land R (G) \neq R (D) \land R (X) \neq R (D)))) \to F \neq {I ↾}_{B}$
28		simp32l	$⊢ (((K \in HL \land W \in H) \land F \in T \land D \in T) \land ((N \in T \land G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land D \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (X \neq {I ↾}_{B} \land R (G) \neq R (X)) \land (R (D) \neq R (F) \land R (G) \neq R (D) \land R (X) \neq R (D)))) \to X \neq {I ↾}_{B}$
29		simp312	$⊢ (((K \in HL \land W \in H) \land F \in T \land D \in T) \land ((N \in T \land G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land D \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (X \neq {I ↾}_{B} \land R (G) \neq R (X)) \land (R (D) \neq R (F) \land R (G) \neq R (D) \land R (X) \neq R (D)))) \to D \neq {I ↾}_{B}$
30	27 28 29	3jca	$⊢ (((K \in HL \land W \in H) \land F \in T \land D \in T) \land ((N \in T \land G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land D \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (X \neq {I ↾}_{B} \land R (G) \neq R (X)) \land (R (D) \neq R (F) \land R (G) \neq R (D) \land R (X) \neq R (D)))) \to (F \neq {I ↾}_{B} \land X \neq {I ↾}_{B} \land D \neq {I ↾}_{B})$
31		simp22	$⊢ (((K \in HL \land W \in H) \land F \in T \land D \in T) \land ((N \in T \land G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land D \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (X \neq {I ↾}_{B} \land R (G) \neq R (X)) \land (R (D) \neq R (F) \land R (G) \neq R (D) \land R (X) \neq R (D)))) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
32	1 2 3 4 5 6 7 8 9 10 11	cdlemkuat	$⊢ (((K \in HL \land W \in H) \land R (F) = R (N) \land X \in T) \land (F \in T \land D \in T \land N \in T) \land ((R (D) \neq R (F) \land R (D) \neq R (X)) \land (F \neq {I ↾}_{B} \land X \neq {I ↾}_{B} \land D \neq {I ↾}_{B}) \land (P \in A \land \neg P \underset{˙}{\leq} W))) \to U (X) (P) \in A$
33	14 18 19 20 21 22 26 30 31 32	syl333anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land D \in T) \land ((N \in T \land G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land D \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (X \neq {I ↾}_{B} \land R (G) \neq R (X)) \land (R (D) \neq R (F) \land R (G) \neq R (D) \land R (X) \neq R (D)))) \to U (X) (P) \in A$
34		simp32r	$⊢ (((K \in HL \land W \in H) \land F \in T \land D \in T) \land ((N \in T \land G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land D \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (X \neq {I ↾}_{B} \land R (G) \neq R (X)) \land (R (D) \neq R (F) \land R (G) \neq R (D) \land R (X) \neq R (D)))) \to R (G) \neq R (X)$
35	34	necomd	$⊢ (((K \in HL \land W \in H) \land F \in T \land D \in T) \land ((N \in T \land G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land D \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (X \neq {I ↾}_{B} \land R (G) \neq R (X)) \land (R (D) \neq R (F) \land R (G) \neq R (D) \land R (X) \neq R (D)))) \to R (X) \neq R (G)$
36	5 6 7 8	trlcocnvat	$⊢ ((K \in HL \land W \in H) \land (X \in T \land G \in T) \land R (X) \neq R (G)) \to R (X \circ G^{-1}) \in A$
37	14 19 15 35 36	syl121anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land D \in T) \land ((N \in T \land G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land D \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (X \neq {I ↾}_{B} \land R (G) \neq R (X)) \land (R (D) \neq R (F) \land R (G) \neq R (D) \land R (X) \neq R (D)))) \to R (X \circ G^{-1}) \in A$
38		simp332	$⊢ (((K \in HL \land W \in H) \land F \in T \land D \in T) \land ((N \in T \land G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land D \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (X \neq {I ↾}_{B} \land R (G) \neq R (X)) \land (R (D) \neq R (F) \land R (G) \neq R (D) \land R (X) \neq R (D)))) \to R (G) \neq R (D)$
39	38	necomd	$⊢ (((K \in HL \land W \in H) \land F \in T \land D \in T) \land ((N \in T \land G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land D \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (X \neq {I ↾}_{B} \land R (G) \neq R (X)) \land (R (D) \neq R (F) \land R (G) \neq R (D) \land R (X) \neq R (D)))) \to R (D) \neq R (G)$
40	23 39	jca	$⊢ (((K \in HL \land W \in H) \land F \in T \land D \in T) \land ((N \in T \land G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land D \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (X \neq {I ↾}_{B} \land R (G) \neq R (X)) \land (R (D) \neq R (F) \land R (G) \neq R (D) \land R (X) \neq R (D)))) \to (R (D) \neq R (F) \land R (D) \neq R (G))$
41		simp313	$⊢ (((K \in HL \land W \in H) \land F \in T \land D \in T) \land ((N \in T \land G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land D \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (X \neq {I ↾}_{B} \land R (G) \neq R (X)) \land (R (D) \neq R (F) \land R (G) \neq R (D) \land R (X) \neq R (D)))) \to G \neq {I ↾}_{B}$
42	27 41 29	3jca	$⊢ (((K \in HL \land W \in H) \land F \in T \land D \in T) \land ((N \in T \land G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land D \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (X \neq {I ↾}_{B} \land R (G) \neq R (X)) \land (R (D) \neq R (F) \land R (G) \neq R (D) \land R (X) \neq R (D)))) \to (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land D \neq {I ↾}_{B})$
43	1 2 3 4 5 6 7 8 9 10 11	cdlemkuat	$⊢ (((K \in HL \land W \in H) \land R (F) = R (N) \land G \in T) \land (F \in T \land D \in T \land N \in T) \land ((R (D) \neq R (F) \land R (D) \neq R (G)) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land D \neq {I ↾}_{B}) \land (P \in A \land \neg P \underset{˙}{\leq} W))) \to U (G) (P) \in A$
44	14 18 15 20 21 22 40 42 31 43	syl333anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land D \in T) \land ((N \in T \land G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land D \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (X \neq {I ↾}_{B} \land R (G) \neq R (X)) \land (R (D) \neq R (F) \land R (G) \neq R (D) \land R (X) \neq R (D)))) \to U (G) (P) \in A$
45	1 2 3 4 5 6 7 8 9 10 11	cdlemkuv2	$⊢ (((K \in HL \land W \in H) \land R (F) = R (N) \land G \in T) \land (F \in T \land D \in T \land N \in T) \land ((R (D) \neq R (F) \land R (D) \neq R (G)) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land D \neq {I ↾}_{B}) \land (P \in A \land \neg P \underset{˙}{\leq} W))) \to U (G) (P) = (P \underset{˙}{\lor} R (G)) \underset{˙}{\land} (O (P) \underset{˙}{\lor} R (G \circ D^{-1}))$
46	14 18 15 20 21 22 40 42 31 45	syl333anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land D \in T) \land ((N \in T \land G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land D \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (X \neq {I ↾}_{B} \land R (G) \neq R (X)) \land (R (D) \neq R (F) \land R (G) \neq R (D) \land R (X) \neq R (D)))) \to U (G) (P) = (P \underset{˙}{\lor} R (G)) \underset{˙}{\land} (O (P) \underset{˙}{\lor} R (G \circ D^{-1}))$
47	12	hllatd	$⊢ (((K \in HL \land W \in H) \land F \in T \land D \in T) \land ((N \in T \land G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land D \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (X \neq {I ↾}_{B} \land R (G) \neq R (X)) \land (R (D) \neq R (F) \land R (G) \neq R (D) \land R (X) \neq R (D)))) \to K \in Lat$
48	1 5 6 7 8	trlnidat	$⊢ ((K \in HL \land W \in H) \land G \in T \land G \neq {I ↾}_{B}) \to R (G) \in A$
49	14 15 41 48	syl3anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land D \in T) \land ((N \in T \land G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land D \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (X \neq {I ↾}_{B} \land R (G) \neq R (X)) \land (R (D) \neq R (F) \land R (G) \neq R (D) \land R (X) \neq R (D)))) \to R (G) \in A$
50	1 3 5	hlatjcl	$⊢ (K \in HL \land P \in A \land R (G) \in A) \to P \underset{˙}{\lor} R (G) \in B$
51	12 13 49 50	syl3anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land D \in T) \land ((N \in T \land G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land D \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (X \neq {I ↾}_{B} \land R (G) \neq R (X)) \land (R (D) \neq R (F) \land R (G) \neq R (D) \land R (X) \neq R (D)))) \to P \underset{˙}{\lor} R (G) \in B$
52		simp1	$⊢ (((K \in HL \land W \in H) \land F \in T \land D \in T) \land ((N \in T \land G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land D \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (X \neq {I ↾}_{B} \land R (G) \neq R (X)) \land (R (D) \neq R (F) \land R (G) \neq R (D) \land R (X) \neq R (D)))) \to ((K \in HL \land W \in H) \land F \in T \land D \in T)$
53	22 31 18	3jca	$⊢ (((K \in HL \land W \in H) \land F \in T \land D \in T) \land ((N \in T \land G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land D \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (X \neq {I ↾}_{B} \land R (G) \neq R (X)) \land (R (D) \neq R (F) \land R (G) \neq R (D) \land R (X) \neq R (D)))) \to (N \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N))$
54	1 2 3 4 5 6 7 8 9 10	cdlemkoatnle	$⊢ (((K \in HL \land W \in H) \land F \in T \land D \in T) \land (N \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land (F \neq {I ↾}_{B} \land D \neq {I ↾}_{B} \land R (D) \neq R (F))) \to (O (P) \in A \land \neg O (P) \underset{˙}{\leq} W)$
55	54	simpld	$⊢ (((K \in HL \land W \in H) \land F \in T \land D \in T) \land (N \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land (F \neq {I ↾}_{B} \land D \neq {I ↾}_{B} \land R (D) \neq R (F))) \to O (P) \in A$
56	52 53 27 29 23 55	syl113anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land D \in T) \land ((N \in T \land G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land D \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (X \neq {I ↾}_{B} \land R (G) \neq R (X)) \land (R (D) \neq R (F) \land R (G) \neq R (D) \land R (X) \neq R (D)))) \to O (P) \in A$
57	5 6 7 8	trlcocnvat	$⊢ ((K \in HL \land W \in H) \land (G \in T \land D \in T) \land R (G) \neq R (D)) \to R (G \circ D^{-1}) \in A$
58	14 15 21 38 57	syl121anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land D \in T) \land ((N \in T \land G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land D \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (X \neq {I ↾}_{B} \land R (G) \neq R (X)) \land (R (D) \neq R (F) \land R (G) \neq R (D) \land R (X) \neq R (D)))) \to R (G \circ D^{-1}) \in A$
59	1 3 5	hlatjcl	$⊢ (K \in HL \land O (P) \in A \land R (G \circ D^{-1}) \in A) \to O (P) \underset{˙}{\lor} R (G \circ D^{-1}) \in B$
60	12 56 58 59	syl3anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land D \in T) \land ((N \in T \land G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land D \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (X \neq {I ↾}_{B} \land R (G) \neq R (X)) \land (R (D) \neq R (F) \land R (G) \neq R (D) \land R (X) \neq R (D)))) \to O (P) \underset{˙}{\lor} R (G \circ D^{-1}) \in B$
61	1 2 4	latmle1	$⊢ (K \in Lat \land P \underset{˙}{\lor} R (G) \in B \land O (P) \underset{˙}{\lor} R (G \circ D^{-1}) \in B) \to ((P \underset{˙}{\lor} R (G)) \underset{˙}{\land} (O (P) \underset{˙}{\lor} R (G \circ D^{-1}))) \underset{˙}{\leq} (P \underset{˙}{\lor} R (G))$
62	47 51 60 61	syl3anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land D \in T) \land ((N \in T \land G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land D \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (X \neq {I ↾}_{B} \land R (G) \neq R (X)) \land (R (D) \neq R (F) \land R (G) \neq R (D) \land R (X) \neq R (D)))) \to ((P \underset{˙}{\lor} R (G)) \underset{˙}{\land} (O (P) \underset{˙}{\lor} R (G \circ D^{-1}))) \underset{˙}{\leq} (P \underset{˙}{\lor} R (G))$
63	46 62	eqbrtrd	$⊢ (((K \in HL \land W \in H) \land F \in T \land D \in T) \land ((N \in T \land G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land D \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (X \neq {I ↾}_{B} \land R (G) \neq R (X)) \land (R (D) \neq R (F) \land R (G) \neq R (D) \land R (X) \neq R (D)))) \to U (G) (P) \underset{˙}{\leq} (P \underset{˙}{\lor} R (G))$
64	2 3 5 6 7 8	trljat1	$⊢ ((K \in HL \land W \in H) \land G \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to P \underset{˙}{\lor} R (G) = P \underset{˙}{\lor} G (P)$
65	14 15 31 64	syl3anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land D \in T) \land ((N \in T \land G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land D \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (X \neq {I ↾}_{B} \land R (G) \neq R (X)) \land (R (D) \neq R (F) \land R (G) \neq R (D) \land R (X) \neq R (D)))) \to P \underset{˙}{\lor} R (G) = P \underset{˙}{\lor} G (P)$
66	63 65	breqtrd	$⊢ (((K \in HL \land W \in H) \land F \in T \land D \in T) \land ((N \in T \land G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land D \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (X \neq {I ↾}_{B} \land R (G) \neq R (X)) \land (R (D) \neq R (F) \land R (G) \neq R (D) \land R (X) \neq R (D)))) \to U (G) (P) \underset{˙}{\leq} (P \underset{˙}{\lor} G (P))$
67		simp2	$⊢ (((K \in HL \land W \in H) \land F \in T \land D \in T) \land ((N \in T \land G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land D \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (X \neq {I ↾}_{B} \land R (G) \neq R (X)) \land (R (D) \neq R (F) \land R (G) \neq R (D) \land R (X) \neq R (D)))) \to ((N \in T \land G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N))$
68		simp31	$⊢ (((K \in HL \land W \in H) \land F \in T \land D \in T) \land ((N \in T \land G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land D \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (X \neq {I ↾}_{B} \land R (G) \neq R (X)) \land (R (D) \neq R (F) \land R (G) \neq R (D) \land R (X) \neq R (D)))) \to (F \neq {I ↾}_{B} \land D \neq {I ↾}_{B} \land G \neq {I ↾}_{B})$
69		simp33	$⊢ (((K \in HL \land W \in H) \land F \in T \land D \in T) \land ((N \in T \land G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land D \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (X \neq {I ↾}_{B} \land R (G) \neq R (X)) \land (R (D) \neq R (F) \land R (G) \neq R (D) \land R (X) \neq R (D)))) \to (R (D) \neq R (F) \land R (G) \neq R (D) \land R (X) \neq R (D))$
70		eqid	$⊢ (G (P) \underset{˙}{\lor} X (P)) \underset{˙}{\land} (R (G \circ D^{-1}) \underset{˙}{\lor} R (X \circ D^{-1})) = (G (P) \underset{˙}{\lor} X (P)) \underset{˙}{\land} (R (G \circ D^{-1}) \underset{˙}{\lor} R (X \circ D^{-1}))$
71	1 2 3 4 5 6 7 8 9 10 11 70	cdlemk11u	$⊢ (((K \in HL \land W \in H) \land F \in T \land D \in T) \land ((N \in T \land G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land D \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land X \neq {I ↾}_{B} \land (R (D) \neq R (F) \land R (G) \neq R (D) \land R (X) \neq R (D)))) \to U (G) (P) \underset{˙}{\leq} (U (X) (P) \underset{˙}{\lor} R (X \circ G^{-1}))$
72	52 67 68 28 69 71	syl113anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land D \in T) \land ((N \in T \land G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land D \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (X \neq {I ↾}_{B} \land R (G) \neq R (X)) \land (R (D) \neq R (F) \land R (G) \neq R (D) \land R (X) \neq R (D)))) \to U (G) (P) \underset{˙}{\leq} (U (X) (P) \underset{˙}{\lor} R (X \circ G^{-1}))$
73	2 3 5	hlatlej2	$⊢ (K \in HL \land P \in A \land R (G) \in A) \to R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} R (G))$
74	12 13 49 73	syl3anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land D \in T) \land ((N \in T \land G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land D \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (X \neq {I ↾}_{B} \land R (G) \neq R (X)) \land (R (D) \neq R (F) \land R (G) \neq R (D) \land R (X) \neq R (D)))) \to R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} R (G))$
75	74 65	breqtrd	$⊢ (((K \in HL \land W \in H) \land F \in T \land D \in T) \land ((N \in T \land G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land D \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (X \neq {I ↾}_{B} \land R (G) \neq R (X)) \land (R (D) \neq R (F) \land R (G) \neq R (D) \land R (X) \neq R (D)))) \to R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} G (P))$
76	1 2 3 4 5 6 7 8 9 10 11	cdlemkuel	$⊢ (((K \in HL \land W \in H) \land R (F) = R (N) \land X \in T) \land (F \in T \land D \in T \land N \in T) \land ((R (D) \neq R (F) \land R (D) \neq R (X)) \land (F \neq {I ↾}_{B} \land X \neq {I ↾}_{B} \land D \neq {I ↾}_{B}) \land (P \in A \land \neg P \underset{˙}{\leq} W))) \to U (X) \in T$
77	14 18 19 20 21 22 26 30 31 76	syl333anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land D \in T) \land ((N \in T \land G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land D \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (X \neq {I ↾}_{B} \land R (G) \neq R (X)) \land (R (D) \neq R (F) \land R (G) \neq R (D) \land R (X) \neq R (D)))) \to U (X) \in T$
78	2 5 6 7	ltrnel	$⊢ ((K \in HL \land W \in H) \land U (X) \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to (U (X) (P) \in A \land \neg U (X) (P) \underset{˙}{\leq} W)$
79	14 77 31 78	syl3anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land D \in T) \land ((N \in T \land G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land D \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (X \neq {I ↾}_{B} \land R (G) \neq R (X)) \land (R (D) \neq R (F) \land R (G) \neq R (D) \land R (X) \neq R (D)))) \to (U (X) (P) \in A \land \neg U (X) (P) \underset{˙}{\leq} W)$
80	6 7	ltrncnv	$⊢ ((K \in HL \land W \in H) \land G \in T) \to G^{-1} \in T$
81	14 15 80	syl2anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land D \in T) \land ((N \in T \land G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land D \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (X \neq {I ↾}_{B} \land R (G) \neq R (X)) \land (R (D) \neq R (F) \land R (G) \neq R (D) \land R (X) \neq R (D)))) \to G^{-1} \in T$
82	6 7 8	trlcnv	$⊢ ((K \in HL \land W \in H) \land G \in T) \to R (G^{-1}) = R (G)$
83	14 15 82	syl2anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land D \in T) \land ((N \in T \land G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land D \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (X \neq {I ↾}_{B} \land R (G) \neq R (X)) \land (R (D) \neq R (F) \land R (G) \neq R (D) \land R (X) \neq R (D)))) \to R (G^{-1}) = R (G)$
84	83 34	eqnetrd	$⊢ (((K \in HL \land W \in H) \land F \in T \land D \in T) \land ((N \in T \land G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land D \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (X \neq {I ↾}_{B} \land R (G) \neq R (X)) \land (R (D) \neq R (F) \land R (G) \neq R (D) \land R (X) \neq R (D)))) \to R (G^{-1}) \neq R (X)$
85	1 6 7 8	trlcone	$⊢ ((K \in HL \land W \in H) \land (G^{-1} \in T \land X \in T) \land (R (G^{-1}) \neq R (X) \land X \neq {I ↾}_{B})) \to R (G^{-1}) \neq R (G^{-1} \circ X)$
86	14 81 19 84 28 85	syl122anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land D \in T) \land ((N \in T \land G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land D \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (X \neq {I ↾}_{B} \land R (G) \neq R (X)) \land (R (D) \neq R (F) \land R (G) \neq R (D) \land R (X) \neq R (D)))) \to R (G^{-1}) \neq R (G^{-1} \circ X)$
87	86	necomd	$⊢ (((K \in HL \land W \in H) \land F \in T \land D \in T) \land ((N \in T \land G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land D \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (X \neq {I ↾}_{B} \land R (G) \neq R (X)) \land (R (D) \neq R (F) \land R (G) \neq R (D) \land R (X) \neq R (D)))) \to R (G^{-1} \circ X) \neq R (G^{-1})$
88	6 7	ltrncom	$⊢ ((K \in HL \land W \in H) \land G^{-1} \in T \land X \in T) \to G^{-1} \circ X = X \circ G^{-1}$
89	14 81 19 88	syl3anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land D \in T) \land ((N \in T \land G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land D \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (X \neq {I ↾}_{B} \land R (G) \neq R (X)) \land (R (D) \neq R (F) \land R (G) \neq R (D) \land R (X) \neq R (D)))) \to G^{-1} \circ X = X \circ G^{-1}$
90	89	fveq2d	$⊢ (((K \in HL \land W \in H) \land F \in T \land D \in T) \land ((N \in T \land G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land D \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (X \neq {I ↾}_{B} \land R (G) \neq R (X)) \land (R (D) \neq R (F) \land R (G) \neq R (D) \land R (X) \neq R (D)))) \to R (G^{-1} \circ X) = R (X \circ G^{-1})$
91	87 90 83	3netr3d	$⊢ (((K \in HL \land W \in H) \land F \in T \land D \in T) \land ((N \in T \land G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land D \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (X \neq {I ↾}_{B} \land R (G) \neq R (X)) \land (R (D) \neq R (F) \land R (G) \neq R (D) \land R (X) \neq R (D)))) \to R (X \circ G^{-1}) \neq R (G)$
92	6 7	ltrnco	$⊢ ((K \in HL \land W \in H) \land X \in T \land G^{-1} \in T) \to X \circ G^{-1} \in T$
93	14 19 81 92	syl3anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land D \in T) \land ((N \in T \land G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land D \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (X \neq {I ↾}_{B} \land R (G) \neq R (X)) \land (R (D) \neq R (F) \land R (G) \neq R (D) \land R (X) \neq R (D)))) \to X \circ G^{-1} \in T$
94	2 6 7 8	trlle	$⊢ ((K \in HL \land W \in H) \land X \circ G^{-1} \in T) \to R (X \circ G^{-1}) \underset{˙}{\leq} W$
95	14 93 94	syl2anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land D \in T) \land ((N \in T \land G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land D \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (X \neq {I ↾}_{B} \land R (G) \neq R (X)) \land (R (D) \neq R (F) \land R (G) \neq R (D) \land R (X) \neq R (D)))) \to R (X \circ G^{-1}) \underset{˙}{\leq} W$
96	2 6 7 8	trlle	$⊢ ((K \in HL \land W \in H) \land G \in T) \to R (G) \underset{˙}{\leq} W$
97	14 15 96	syl2anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land D \in T) \land ((N \in T \land G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land D \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (X \neq {I ↾}_{B} \land R (G) \neq R (X)) \land (R (D) \neq R (F) \land R (G) \neq R (D) \land R (X) \neq R (D)))) \to R (G) \underset{˙}{\leq} W$
98	2 3 5 6	lhp2atnle	$⊢ (((K \in HL \land W \in H) \land (U (X) (P) \in A \land \neg U (X) (P) \underset{˙}{\leq} W) \land R (X \circ G^{-1}) \neq R (G)) \land (R (X \circ G^{-1}) \in A \land R (X \circ G^{-1}) \underset{˙}{\leq} W) \land (R (G) \in A \land R (G) \underset{˙}{\leq} W)) \to \neg R (G) \underset{˙}{\leq} (U (X) (P) \underset{˙}{\lor} R (X \circ G^{-1}))$
99	14 79 91 37 95 49 97 98	syl322anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land D \in T) \land ((N \in T \land G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land D \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (X \neq {I ↾}_{B} \land R (G) \neq R (X)) \land (R (D) \neq R (F) \land R (G) \neq R (D) \land R (X) \neq R (D)))) \to \neg R (G) \underset{˙}{\leq} (U (X) (P) \underset{˙}{\lor} R (X \circ G^{-1}))$
100		nbrne1	$⊢ (R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} G (P)) \land \neg R (G) \underset{˙}{\leq} (U (X) (P) \underset{˙}{\lor} R (X \circ G^{-1}))) \to P \underset{˙}{\lor} G (P) \neq U (X) (P) \underset{˙}{\lor} R (X \circ G^{-1})$
101	75 99 100	syl2anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land D \in T) \land ((N \in T \land G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land D \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (X \neq {I ↾}_{B} \land R (G) \neq R (X)) \land (R (D) \neq R (F) \land R (G) \neq R (D) \land R (X) \neq R (D)))) \to P \underset{˙}{\lor} G (P) \neq U (X) (P) \underset{˙}{\lor} R (X \circ G^{-1})$
102	2 3 4 5	2atm	$⊢ ((K \in HL \land P \in A \land G (P) \in A) \land (U (X) (P) \in A \land R (X \circ G^{-1}) \in A \land U (G) (P) \in A) \land (U (G) (P) \underset{˙}{\leq} (P \underset{˙}{\lor} G (P)) \land U (G) (P) \underset{˙}{\leq} (U (X) (P) \underset{˙}{\lor} R (X \circ G^{-1})) \land P \underset{˙}{\lor} G (P) \neq U (X) (P) \underset{˙}{\lor} R (X \circ G^{-1}))) \to U (G) (P) = (P \underset{˙}{\lor} G (P)) \underset{˙}{\land} (U (X) (P) \underset{˙}{\lor} R (X \circ G^{-1}))$
103	12 13 17 33 37 44 66 72 101 102	syl333anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land D \in T) \land ((N \in T \land G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land D \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (X \neq {I ↾}_{B} \land R (G) \neq R (X)) \land (R (D) \neq R (F) \land R (G) \neq R (D) \land R (X) \neq R (D)))) \to U (G) (P) = (P \underset{˙}{\lor} G (P)) \underset{˙}{\land} (U (X) (P) \underset{˙}{\lor} R (X \circ G^{-1}))$

Metamath Proof Explorer

Theorem cdlemk12u

Proof