cdlemg21

Description: Version of cdlemg19 with ( RF ) .<_ ( P .\/ Q ) instead of ( RG ) .<_ ( P .\/ Q ) as a condition. (Contributed by NM, 23-May-2013)

	Ref	Expression
Hypotheses	cdlemg12.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdlemg12.j	$⊢ \underset{˙}{\lor} = join (K)$
	cdlemg12.m	$⊢ \underset{˙}{\land} = meet (K)$
	cdlemg12.a	$⊢ A = Atoms (K)$
	cdlemg12.h	$⊢ H = LHyp (K)$
	cdlemg12.t	$⊢ T = LTrn (K) (W)$
	cdlemg12b.r	$⊢ R = trL (K) (W)$
Assertion	cdlemg21	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((F \in T \land G \in T) \land P \neq Q \land F (P) \neq P) \land (R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land F (G (P)) \underset{˙}{\lor} F (G (Q)) \neq P \underset{˙}{\lor} Q \land \neg \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to (P \underset{˙}{\lor} F (G (P))) \underset{˙}{\land} W = (Q \underset{˙}{\lor} F (G (Q))) \underset{˙}{\land} W$

Proof

Step	Hyp	Ref	Expression
1		cdlemg12.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		cdlemg12.j	$⊢ \underset{˙}{\lor} = join (K)$
3		cdlemg12.m	$⊢ \underset{˙}{\land} = meet (K)$
4		cdlemg12.a	$⊢ A = Atoms (K)$
5		cdlemg12.h	$⊢ H = LHyp (K)$
6		cdlemg12.t	$⊢ T = LTrn (K) (W)$
7		cdlemg12b.r	$⊢ R = trL (K) (W)$
8		simp1	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((F \in T \land G \in T) \land P \neq Q \land F (P) \neq P) \land (R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land F (G (P)) \underset{˙}{\lor} F (G (Q)) \neq P \underset{˙}{\lor} Q \land \neg \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W))$
9		simp21r	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((F \in T \land G \in T) \land P \neq Q \land F (P) \neq P) \land (R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land F (G (P)) \underset{˙}{\lor} F (G (Q)) \neq P \underset{˙}{\lor} Q \land \neg \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to G \in T$
10		simp21l	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((F \in T \land G \in T) \land P \neq Q \land F (P) \neq P) \land (R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land F (G (P)) \underset{˙}{\lor} F (G (Q)) \neq P \underset{˙}{\lor} Q \land \neg \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to F \in T$
11	9 10	jca	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((F \in T \land G \in T) \land P \neq Q \land F (P) \neq P) \land (R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land F (G (P)) \underset{˙}{\lor} F (G (Q)) \neq P \underset{˙}{\lor} Q \land \neg \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to (G \in T \land F \in T)$
12		simp22	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((F \in T \land G \in T) \land P \neq Q \land F (P) \neq P) \land (R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land F (G (P)) \underset{˙}{\lor} F (G (Q)) \neq P \underset{˙}{\lor} Q \land \neg \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to P \neq Q$
13		simp23	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((F \in T \land G \in T) \land P \neq Q \land F (P) \neq P) \land (R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land F (G (P)) \underset{˙}{\lor} F (G (Q)) \neq P \underset{˙}{\lor} Q \land \neg \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to F (P) \neq P$
14		simp31	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((F \in T \land G \in T) \land P \neq Q \land F (P) \neq P) \land (R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land F (G (P)) \underset{˙}{\lor} F (G (Q)) \neq P \underset{˙}{\lor} Q \land \neg \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
15		simp33	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((F \in T \land G \in T) \land P \neq Q \land F (P) \neq P) \land (R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land F (G (P)) \underset{˙}{\lor} F (G (Q)) \neq P \underset{˙}{\lor} Q \land \neg \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to \neg \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r)$
16	1 2 3 4 5 6 7	cdlemg17j	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (G \in T \land F \in T \land P \neq Q) \land (F (P) \neq P \land R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to F (G (P)) = G (F (P))$
17	8 9 10 12 13 14 15 16	syl133anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((F \in T \land G \in T) \land P \neq Q \land F (P) \neq P) \land (R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land F (G (P)) \underset{˙}{\lor} F (G (Q)) \neq P \underset{˙}{\lor} Q \land \neg \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to F (G (P)) = G (F (P))$
18		simp11	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((F \in T \land G \in T) \land P \neq Q \land F (P) \neq P) \land (R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land F (G (P)) \underset{˙}{\lor} F (G (Q)) \neq P \underset{˙}{\lor} Q \land \neg \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to (K \in HL \land W \in H)$
19		simp13	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((F \in T \land G \in T) \land P \neq Q \land F (P) \neq P) \land (R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land F (G (P)) \underset{˙}{\lor} F (G (Q)) \neq P \underset{˙}{\lor} Q \land \neg \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to (Q \in A \land \neg Q \underset{˙}{\leq} W)$
20		simp12	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((F \in T \land G \in T) \land P \neq Q \land F (P) \neq P) \land (R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land F (G (P)) \underset{˙}{\lor} F (G (Q)) \neq P \underset{˙}{\lor} Q \land \neg \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
21	12	necomd	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((F \in T \land G \in T) \land P \neq Q \land F (P) \neq P) \land (R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land F (G (P)) \underset{˙}{\lor} F (G (Q)) \neq P \underset{˙}{\lor} Q \land \neg \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to Q \neq P$
22	1 4 5 6	ltrnatneq	$⊢ ((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land F (P) \neq P) \to F (Q) \neq Q$
23	18 10 20 19 13 22	syl131anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((F \in T \land G \in T) \land P \neq Q \land F (P) \neq P) \land (R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land F (G (P)) \underset{˙}{\lor} F (G (Q)) \neq P \underset{˙}{\lor} Q \land \neg \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to F (Q) \neq Q$
24		simp11l	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((F \in T \land G \in T) \land P \neq Q \land F (P) \neq P) \land (R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land F (G (P)) \underset{˙}{\lor} F (G (Q)) \neq P \underset{˙}{\lor} Q \land \neg \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to K \in HL$
25		simp12l	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((F \in T \land G \in T) \land P \neq Q \land F (P) \neq P) \land (R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land F (G (P)) \underset{˙}{\lor} F (G (Q)) \neq P \underset{˙}{\lor} Q \land \neg \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to P \in A$
26		simp13l	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((F \in T \land G \in T) \land P \neq Q \land F (P) \neq P) \land (R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land F (G (P)) \underset{˙}{\lor} F (G (Q)) \neq P \underset{˙}{\lor} Q \land \neg \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to Q \in A$
27	2 4	hlatjcom	$⊢ (K \in HL \land P \in A \land Q \in A) \to P \underset{˙}{\lor} Q = Q \underset{˙}{\lor} P$
28	24 25 26 27	syl3anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((F \in T \land G \in T) \land P \neq Q \land F (P) \neq P) \land (R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land F (G (P)) \underset{˙}{\lor} F (G (Q)) \neq P \underset{˙}{\lor} Q \land \neg \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to P \underset{˙}{\lor} Q = Q \underset{˙}{\lor} P$
29	14 28	breqtrd	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((F \in T \land G \in T) \land P \neq Q \land F (P) \neq P) \land (R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land F (G (P)) \underset{˙}{\lor} F (G (Q)) \neq P \underset{˙}{\lor} Q \land \neg \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to R (F) \underset{˙}{\leq} (Q \underset{˙}{\lor} P)$
30		eqcom	$⊢ P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r \leftrightarrow Q \underset{˙}{\lor} r = P \underset{˙}{\lor} r$
31	30	anbi2i	$⊢ (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r) \leftrightarrow (\neg r \underset{˙}{\leq} W \land Q \underset{˙}{\lor} r = P \underset{˙}{\lor} r)$
32	31	rexbii	$⊢ \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r) \leftrightarrow \exists r \in A (\neg r \underset{˙}{\leq} W \land Q \underset{˙}{\lor} r = P \underset{˙}{\lor} r)$
33	15 32	sylnib	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((F \in T \land G \in T) \land P \neq Q \land F (P) \neq P) \land (R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land F (G (P)) \underset{˙}{\lor} F (G (Q)) \neq P \underset{˙}{\lor} Q \land \neg \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to \neg \exists r \in A (\neg r \underset{˙}{\leq} W \land Q \underset{˙}{\lor} r = P \underset{˙}{\lor} r)$
34	1 2 3 4 5 6 7	cdlemg17j	$⊢ (((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (G \in T \land F \in T \land Q \neq P) \land (F (Q) \neq Q \land R (F) \underset{˙}{\leq} (Q \underset{˙}{\lor} P) \land \neg \exists r \in A (\neg r \underset{˙}{\leq} W \land Q \underset{˙}{\lor} r = P \underset{˙}{\lor} r))) \to F (G (Q)) = G (F (Q))$
35	18 19 20 9 10 21 23 29 33 34	syl333anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((F \in T \land G \in T) \land P \neq Q \land F (P) \neq P) \land (R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land F (G (P)) \underset{˙}{\lor} F (G (Q)) \neq P \underset{˙}{\lor} Q \land \neg \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to F (G (Q)) = G (F (Q))$
36	17 35	oveq12d	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((F \in T \land G \in T) \land P \neq Q \land F (P) \neq P) \land (R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land F (G (P)) \underset{˙}{\lor} F (G (Q)) \neq P \underset{˙}{\lor} Q \land \neg \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to F (G (P)) \underset{˙}{\lor} F (G (Q)) = G (F (P)) \underset{˙}{\lor} G (F (Q))$
37		simp32	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((F \in T \land G \in T) \land P \neq Q \land F (P) \neq P) \land (R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land F (G (P)) \underset{˙}{\lor} F (G (Q)) \neq P \underset{˙}{\lor} Q \land \neg \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to F (G (P)) \underset{˙}{\lor} F (G (Q)) \neq P \underset{˙}{\lor} Q$
38	36 37	eqnetrrd	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((F \in T \land G \in T) \land P \neq Q \land F (P) \neq P) \land (R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land F (G (P)) \underset{˙}{\lor} F (G (Q)) \neq P \underset{˙}{\lor} Q \land \neg \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to G (F (P)) \underset{˙}{\lor} G (F (Q)) \neq P \underset{˙}{\lor} Q$
39	1 2 3 4 5 6 7	cdlemg19	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((G \in T \land F \in T) \land P \neq Q \land F (P) \neq P) \land (R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land G (F (P)) \underset{˙}{\lor} G (F (Q)) \neq P \underset{˙}{\lor} Q \land \neg \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to (P \underset{˙}{\lor} G (F (P))) \underset{˙}{\land} W = (Q \underset{˙}{\lor} G (F (Q))) \underset{˙}{\land} W$
40	8 11 12 13 14 38 15 39	syl133anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((F \in T \land G \in T) \land P \neq Q \land F (P) \neq P) \land (R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land F (G (P)) \underset{˙}{\lor} F (G (Q)) \neq P \underset{˙}{\lor} Q \land \neg \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to (P \underset{˙}{\lor} G (F (P))) \underset{˙}{\land} W = (Q \underset{˙}{\lor} G (F (Q))) \underset{˙}{\land} W$
41	17	oveq2d	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((F \in T \land G \in T) \land P \neq Q \land F (P) \neq P) \land (R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land F (G (P)) \underset{˙}{\lor} F (G (Q)) \neq P \underset{˙}{\lor} Q \land \neg \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to P \underset{˙}{\lor} F (G (P)) = P \underset{˙}{\lor} G (F (P))$
42	41	oveq1d	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((F \in T \land G \in T) \land P \neq Q \land F (P) \neq P) \land (R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land F (G (P)) \underset{˙}{\lor} F (G (Q)) \neq P \underset{˙}{\lor} Q \land \neg \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to (P \underset{˙}{\lor} F (G (P))) \underset{˙}{\land} W = (P \underset{˙}{\lor} G (F (P))) \underset{˙}{\land} W$
43	35	oveq2d	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((F \in T \land G \in T) \land P \neq Q \land F (P) \neq P) \land (R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land F (G (P)) \underset{˙}{\lor} F (G (Q)) \neq P \underset{˙}{\lor} Q \land \neg \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to Q \underset{˙}{\lor} F (G (Q)) = Q \underset{˙}{\lor} G (F (Q))$
44	43	oveq1d	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((F \in T \land G \in T) \land P \neq Q \land F (P) \neq P) \land (R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land F (G (P)) \underset{˙}{\lor} F (G (Q)) \neq P \underset{˙}{\lor} Q \land \neg \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to (Q \underset{˙}{\lor} F (G (Q))) \underset{˙}{\land} W = (Q \underset{˙}{\lor} G (F (Q))) \underset{˙}{\land} W$
45	40 42 44	3eqtr4d	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((F \in T \land G \in T) \land P \neq Q \land F (P) \neq P) \land (R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land F (G (P)) \underset{˙}{\lor} F (G (Q)) \neq P \underset{˙}{\lor} Q \land \neg \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to (P \underset{˙}{\lor} F (G (P))) \underset{˙}{\land} W = (Q \underset{˙}{\lor} F (G (Q))) \underset{˙}{\land} W$

Metamath Proof Explorer

Theorem cdlemg21

Proof