cdlemk7u

Description: Part of proof of Lemma K of Crawley p. 118. Line 5, p. 119 for the sigma_1 case. (Contributed by NM, 3-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}))))$
	cdlemk1.v	$⊢ V = (G (P) \underset{˙}{\lor} X (P)) \underset{˙}{\land} (R (G \circ D^{-1}) \underset{˙}{\lor} R (X \circ D^{-1}))$
Assertion	cdlemk7u	$⊢ (((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} V)$

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		cdlemk1.v	$⊢ V = (G (P) \underset{˙}{\lor} X (P)) \underset{˙}{\land} (R (G \circ D^{-1}) \underset{˙}{\lor} R (X \circ D^{-1}))$
13		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 (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})$
14		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 (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))$
15	13 14	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 (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}) \land (R (D) \neq R (F) \land R (G) \neq R (D) \land R (X) \neq R (D)))$
16	1 2 3 4 5 6 7 8 9 10	cdlemk6u	$⊢ (((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 (R (D) \neq R (F) \land R (G) \neq R (D) \land R (X) \neq R (D)))) \to ((P \underset{˙}{\lor} G (P)) \underset{˙}{\land} (O (P) \underset{˙}{\lor} R (G \circ D^{-1}))) \underset{˙}{\leq} (((G (P) \underset{˙}{\lor} X (P)) \underset{˙}{\land} (R (G \circ D^{-1}) \underset{˙}{\lor} R (X \circ D^{-1}))) \underset{˙}{\lor} ((X (P) \underset{˙}{\lor} P) \underset{˙}{\land} (R (X \circ D^{-1}) \underset{˙}{\lor} O (P))))$
17	15 16	syld3an3	$⊢ (((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 ((P \underset{˙}{\lor} G (P)) \underset{˙}{\land} (O (P) \underset{˙}{\lor} R (G \circ D^{-1}))) \underset{˙}{\leq} (((G (P) \underset{˙}{\lor} X (P)) \underset{˙}{\land} (R (G \circ D^{-1}) \underset{˙}{\lor} R (X \circ D^{-1}))) \underset{˙}{\lor} ((X (P) \underset{˙}{\lor} P) \underset{˙}{\land} (R (X \circ D^{-1}) \underset{˙}{\lor} O (P))))$
18		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 (D) \neq R (F) \land R (G) \neq R (D) \land R (X) \neq R (D)))) \to K \in HL$
19		simp11r	$⊢ (((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 W \in H$
20	18 19	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 (D) \neq R (F) \land R (G) \neq R (D) \land R (X) \neq R (D)))) \to (K \in HL \land W \in H)$
21		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 (D) \neq R (F) \land R (G) \neq R (D) \land R (X) \neq R (D)))) \to R (F) = R (N)$
22		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 (D) \neq R (F) \land R (G) \neq R (D) \land R (X) \neq R (D)))) \to G \in T$
23		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 (D) \neq R (F) \land R (G) \neq R (D) \land R (X) \neq R (D)))) \to F \in T$
24		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 (D) \neq R (F) \land R (G) \neq R (D) \land R (X) \neq R (D)))) \to D \in T$
25		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 (D) \neq R (F) \land R (G) \neq R (D) \land R (X) \neq R (D)))) \to N \in T$
26	23 24 25	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 (D) \neq R (F) \land R (G) \neq R (D) \land R (X) \neq R (D)))) \to (F \in T \land D \in T \land N \in T)$
27		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 (D) \neq R (F) \land R (G) \neq R (D) \land R (X) \neq R (D)))) \to R (D) \neq R (F)$
28		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 (D) \neq R (F) \land R (G) \neq R (D) \land R (X) \neq R (D)))) \to R (G) \neq R (D)$
29	28	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 (D) \neq R (F) \land R (G) \neq R (D) \land R (X) \neq R (D)))) \to R (D) \neq R (G)$
30	27 29	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 (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))$
31		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 (D) \neq R (F) \land R (G) \neq R (D) \land R (X) \neq R (D)))) \to F \neq {I ↾}_{B}$
32		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 (D) \neq R (F) \land R (G) \neq R (D) \land R (X) \neq R (D)))) \to G \neq {I ↾}_{B}$
33		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 (D) \neq R (F) \land R (G) \neq R (D) \land R (X) \neq R (D)))) \to D \neq {I ↾}_{B}$
34	31 32 33	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 (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})$
35		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 (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)$
36	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}))$
37	20 21 22 26 30 34 35 36	syl313anc	$⊢ (((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) = (P \underset{˙}{\lor} R (G)) \underset{˙}{\land} (O (P) \underset{˙}{\lor} R (G \circ D^{-1}))$
38	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)$
39	20 22 35 38	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 (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)$
40	39	oveq1d	$⊢ (((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 (P \underset{˙}{\lor} R (G)) \underset{˙}{\land} (O (P) \underset{˙}{\lor} R (G \circ D^{-1})) = (P \underset{˙}{\lor} G (P)) \underset{˙}{\land} (O (P) \underset{˙}{\lor} R (G \circ D^{-1}))$
41	37 40	eqtrd	$⊢ (((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) = (P \underset{˙}{\lor} G (P)) \underset{˙}{\land} (O (P) \underset{˙}{\lor} R (G \circ D^{-1}))$
42	18	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 (D) \neq R (F) \land R (G) \neq R (D) \land R (X) \neq R (D)))) \to K \in Lat$
43		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 (D) \neq R (F) \land R (G) \neq R (D) \land R (X) \neq R (D)))) \to X \in T$
44		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 (D) \neq R (F) \land R (G) \neq R (D) \land R (X) \neq R (D)))) \to R (X) \neq R (D)$
45	44	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 (D) \neq R (F) \land R (G) \neq R (D) \land R (X) \neq R (D)))) \to R (D) \neq R (X)$
46	27 45	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 (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))$
47		simp32	$⊢ (((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 X \neq {I ↾}_{B}$
48	31 47 33	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 (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})$
49	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$
50	20 21 43 26 46 48 35 49	syl313anc	$⊢ (((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 (X) (P) \in A$
51	1 5	atbase	$⊢ U (X) (P) \in A \to U (X) (P) \in B$
52	50 51	syl	$⊢ (((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 (X) (P) \in B$
53		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 (D) \neq R (F) \land R (G) \neq R (D) \land R (X) \neq R (D)))) \to P \in A$
54	1 2 3 5 6 7 8 4 12	cdlemkvcl	$⊢ ((K \in HL \land W \in H) \land (D \in T \land G \in T \land X \in T) \land P \in A) \to V \in B$
55	18 19 24 22 43 53 54	syl231anc	$⊢ (((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 V \in B$
56	1 3	latjcom	$⊢ (K \in Lat \land U (X) (P) \in B \land V \in B) \to U (X) (P) \underset{˙}{\lor} V = V \underset{˙}{\lor} U (X) (P)$
57	42 52 55 56	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 (D) \neq R (F) \land R (G) \neq R (D) \land R (X) \neq R (D)))) \to U (X) (P) \underset{˙}{\lor} V = V \underset{˙}{\lor} U (X) (P)$
58	12	a1i	$⊢ (((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 V = (G (P) \underset{˙}{\lor} X (P)) \underset{˙}{\land} (R (G \circ D^{-1}) \underset{˙}{\lor} R (X \circ D^{-1}))$
59	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 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) = (P \underset{˙}{\lor} R (X)) \underset{˙}{\land} (O (P) \underset{˙}{\lor} R (X \circ D^{-1}))$
60	20 21 43 26 46 48 35 59	syl313anc	$⊢ (((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 (X) (P) = (P \underset{˙}{\lor} R (X)) \underset{˙}{\land} (O (P) \underset{˙}{\lor} R (X \circ D^{-1}))$
61	2 3 5 6 7 8	trljat1	$⊢ ((K \in HL \land W \in H) \land X \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to P \underset{˙}{\lor} R (X) = P \underset{˙}{\lor} X (P)$
62	20 43 35 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 (D) \neq R (F) \land R (G) \neq R (D) \land R (X) \neq R (D)))) \to P \underset{˙}{\lor} R (X) = P \underset{˙}{\lor} X (P)$
63	2 5 6 7	ltrnat	$⊢ ((K \in HL \land W \in H) \land X \in T \land P \in A) \to X (P) \in A$
64	20 43 53 63	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 (D) \neq R (F) \land R (G) \neq R (D) \land R (X) \neq R (D)))) \to X (P) \in A$
65	3 5	hlatjcom	$⊢ (K \in HL \land X (P) \in A \land P \in A) \to X (P) \underset{˙}{\lor} P = P \underset{˙}{\lor} X (P)$
66	18 64 53 65	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 (D) \neq R (F) \land R (G) \neq R (D) \land R (X) \neq R (D)))) \to X (P) \underset{˙}{\lor} P = P \underset{˙}{\lor} X (P)$
67	62 66	eqtr4d	$⊢ (((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 P \underset{˙}{\lor} R (X) = X (P) \underset{˙}{\lor} P$
68		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 (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)$
69	25 35 21	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 (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))$
70	31 33 27	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 (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 R (D) \neq R (F))$
71	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)$
72	71	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$
73	68 69 70 72	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 (D) \neq R (F) \land R (G) \neq R (D) \land R (X) \neq R (D)))) \to O (P) \in A$
74	43 24	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 (D) \neq R (F) \land R (G) \neq R (D) \land R (X) \neq R (D)))) \to (X \in T \land D \in T)$
75	5 6 7 8	trlcocnvat	$⊢ ((K \in HL \land W \in H) \land (X \in T \land D \in T) \land R (X) \neq R (D)) \to R (X \circ D^{-1}) \in A$
76	20 74 44 75	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 (D) \neq R (F) \land R (G) \neq R (D) \land R (X) \neq R (D)))) \to R (X \circ D^{-1}) \in A$
77	3 5	hlatjcom	$⊢ (K \in HL \land O (P) \in A \land R (X \circ D^{-1}) \in A) \to O (P) \underset{˙}{\lor} R (X \circ D^{-1}) = R (X \circ D^{-1}) \underset{˙}{\lor} O (P)$
78	18 73 76 77	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 (D) \neq R (F) \land R (G) \neq R (D) \land R (X) \neq R (D)))) \to O (P) \underset{˙}{\lor} R (X \circ D^{-1}) = R (X \circ D^{-1}) \underset{˙}{\lor} O (P)$
79	67 78	oveq12d	$⊢ (((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 (P \underset{˙}{\lor} R (X)) \underset{˙}{\land} (O (P) \underset{˙}{\lor} R (X \circ D^{-1})) = (X (P) \underset{˙}{\lor} P) \underset{˙}{\land} (R (X \circ D^{-1}) \underset{˙}{\lor} O (P))$
80	60 79	eqtrd	$⊢ (((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 (X) (P) = (X (P) \underset{˙}{\lor} P) \underset{˙}{\land} (R (X \circ D^{-1}) \underset{˙}{\lor} O (P))$
81	58 80	oveq12d	$⊢ (((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 V \underset{˙}{\lor} U (X) (P) = ((G (P) \underset{˙}{\lor} X (P)) \underset{˙}{\land} (R (G \circ D^{-1}) \underset{˙}{\lor} R (X \circ D^{-1}))) \underset{˙}{\lor} ((X (P) \underset{˙}{\lor} P) \underset{˙}{\land} (R (X \circ D^{-1}) \underset{˙}{\lor} O (P)))$
82	57 81	eqtrd	$⊢ (((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 (X) (P) \underset{˙}{\lor} V = ((G (P) \underset{˙}{\lor} X (P)) \underset{˙}{\land} (R (G \circ D^{-1}) \underset{˙}{\lor} R (X \circ D^{-1}))) \underset{˙}{\lor} ((X (P) \underset{˙}{\lor} P) \underset{˙}{\land} (R (X \circ D^{-1}) \underset{˙}{\lor} O (P)))$
83	17 41 82	3brtr4d	$⊢ (((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} V)$

Metamath Proof Explorer

Theorem cdlemk7u

Proof