cdlemd4

Description: Part of proof of Lemma D in Crawley p. 113. (Contributed by NM, 30-May-2012)

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

Proof

Step	Hyp	Ref	Expression
1		cdlemd4.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		cdlemd4.j	$⊢ \underset{˙}{\lor} = join (K)$
3		cdlemd4.a	$⊢ A = Atoms (K)$
4		cdlemd4.h	$⊢ H = LHyp (K)$
5		cdlemd4.t	$⊢ T = LTrn (K) (W)$
6		simp11l	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (P \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \neq P)) \land (F (P) = G (P) \land F (Q) = G (Q))) \to K \in HL$
7		simp11r	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (P \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \neq P)) \land (F (P) = G (P) \land F (Q) = G (Q))) \to W \in H$
8		simp21	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (P \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \neq P)) \land (F (P) = G (P) \land F (Q) = G (Q))) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
9		simp22	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (P \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \neq P)) \land (F (P) = G (P) \land F (Q) = G (Q))) \to (Q \in A \land \neg Q \underset{˙}{\leq} W)$
10		simp231	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (P \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \neq P)) \land (F (P) = G (P) \land F (Q) = G (Q))) \to P \neq Q$
11	1 2 3 4	cdlemb2	$⊢ ((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 P \neq Q) \to \exists s \in A (\neg s \underset{˙}{\leq} W \land \neg s \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$
12	6 7 8 9 10 11	syl221anc	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (P \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \neq P)) \land (F (P) = G (P) \land F (Q) = G (Q))) \to \exists s \in A (\neg s \underset{˙}{\leq} W \land \neg s \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$
13		simpl11	$⊢ ((((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (P \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \neq P)) \land (F (P) = G (P) \land F (Q) = G (Q))) \land (s \in A \land (\neg s \underset{˙}{\leq} W \land \neg s \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to (K \in HL \land W \in H)$
14		simpl12	$⊢ ((((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (P \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \neq P)) \land (F (P) = G (P) \land F (Q) = G (Q))) \land (s \in A \land (\neg s \underset{˙}{\leq} W \land \neg s \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to (F \in T \land G \in T)$
15		simpl13	$⊢ ((((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (P \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \neq P)) \land (F (P) = G (P) \land F (Q) = G (Q))) \land (s \in A \land (\neg s \underset{˙}{\leq} W \land \neg s \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to R \in A$
16		simpl21	$⊢ ((((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (P \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \neq P)) \land (F (P) = G (P) \land F (Q) = G (Q))) \land (s \in A \land (\neg s \underset{˙}{\leq} W \land \neg s \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
17		simprl	$⊢ ((((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (P \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \neq P)) \land (F (P) = G (P) \land F (Q) = G (Q))) \land (s \in A \land (\neg s \underset{˙}{\leq} W \land \neg s \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to s \in A$
18		simprrl	$⊢ ((((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (P \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \neq P)) \land (F (P) = G (P) \land F (Q) = G (Q))) \land (s \in A \land (\neg s \underset{˙}{\leq} W \land \neg s \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to \neg s \underset{˙}{\leq} W$
19	17 18	jca	$⊢ ((((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (P \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \neq P)) \land (F (P) = G (P) \land F (Q) = G (Q))) \land (s \in A \land (\neg s \underset{˙}{\leq} W \land \neg s \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to (s \in A \land \neg s \underset{˙}{\leq} W)$
20	6	hllatd	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (P \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \neq P)) \land (F (P) = G (P) \land F (Q) = G (Q))) \to K \in Lat$
21	20	adantr	$⊢ ((((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (P \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \neq P)) \land (F (P) = G (P) \land F (Q) = G (Q))) \land (s \in A \land (\neg s \underset{˙}{\leq} W \land \neg s \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to K \in Lat$
22		eqid	$⊢ {Base}_{K} = {Base}_{K}$
23	22 3	atbase	$⊢ s \in A \to s \in {Base}_{K}$
24	23	ad2antrl	$⊢ ((((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (P \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \neq P)) \land (F (P) = G (P) \land F (Q) = G (Q))) \land (s \in A \land (\neg s \underset{˙}{\leq} W \land \neg s \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to s \in {Base}_{K}$
25		simp21l	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (P \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \neq P)) \land (F (P) = G (P) \land F (Q) = G (Q))) \to P \in A$
26	22 3	atbase	$⊢ P \in A \to P \in {Base}_{K}$
27	25 26	syl	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (P \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \neq P)) \land (F (P) = G (P) \land F (Q) = G (Q))) \to P \in {Base}_{K}$
28	27	adantr	$⊢ ((((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (P \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \neq P)) \land (F (P) = G (P) \land F (Q) = G (Q))) \land (s \in A \land (\neg s \underset{˙}{\leq} W \land \neg s \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to P \in {Base}_{K}$
29		simp22l	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (P \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \neq P)) \land (F (P) = G (P) \land F (Q) = G (Q))) \to Q \in A$
30	22 3	atbase	$⊢ Q \in A \to Q \in {Base}_{K}$
31	29 30	syl	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (P \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \neq P)) \land (F (P) = G (P) \land F (Q) = G (Q))) \to Q \in {Base}_{K}$
32	31	adantr	$⊢ ((((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (P \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \neq P)) \land (F (P) = G (P) \land F (Q) = G (Q))) \land (s \in A \land (\neg s \underset{˙}{\leq} W \land \neg s \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to Q \in {Base}_{K}$
33		simprrr	$⊢ ((((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (P \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \neq P)) \land (F (P) = G (P) \land F (Q) = G (Q))) \land (s \in A \land (\neg s \underset{˙}{\leq} W \land \neg s \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to \neg s \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
34	22 1 2	latnlej1l	$⊢ (K \in Lat \land (s \in {Base}_{K} \land P \in {Base}_{K} \land Q \in {Base}_{K}) \land \neg s \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to s \neq P$
35	34	necomd	$⊢ (K \in Lat \land (s \in {Base}_{K} \land P \in {Base}_{K} \land Q \in {Base}_{K}) \land \neg s \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to P \neq s$
36	21 24 28 32 33 35	syl131anc	$⊢ ((((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (P \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \neq P)) \land (F (P) = G (P) \land F (Q) = G (Q))) \land (s \in A \land (\neg s \underset{˙}{\leq} W \land \neg s \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to P \neq s$
37		simpl22	$⊢ ((((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (P \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \neq P)) \land (F (P) = G (P) \land F (Q) = G (Q))) \land (s \in A \land (\neg s \underset{˙}{\leq} W \land \neg s \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to (Q \in A \land \neg Q \underset{˙}{\leq} W)$
38		simpl23	$⊢ ((((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (P \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \neq P)) \land (F (P) = G (P) \land F (Q) = G (Q))) \land (s \in A \land (\neg s \underset{˙}{\leq} W \land \neg s \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to (P \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \neq P)$
39	1 2 3 4	cdlemd3	$⊢ ((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 (P \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \neq P)) \land (R \in A \land s \in A \land \neg s \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} s)$
40	13 16 37 38 15 17 33 39	syl133anc	$⊢ ((((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (P \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \neq P)) \land (F (P) = G (P) \land F (Q) = G (Q))) \land (s \in A \land (\neg s \underset{˙}{\leq} W \land \neg s \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} s)$
41	36 40	jca	$⊢ ((((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (P \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \neq P)) \land (F (P) = G (P) \land F (Q) = G (Q))) \land (s \in A \land (\neg s \underset{˙}{\leq} W \land \neg s \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to (P \neq s \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} s))$
42		simpl3l	$⊢ ((((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (P \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \neq P)) \land (F (P) = G (P) \land F (Q) = G (Q))) \land (s \in A \land (\neg s \underset{˙}{\leq} W \land \neg s \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to F (P) = G (P)$
43	10	adantr	$⊢ ((((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (P \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \neq P)) \land (F (P) = G (P) \land F (Q) = G (Q))) \land (s \in A \land (\neg s \underset{˙}{\leq} W \land \neg s \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to P \neq Q$
44	43 33	jca	$⊢ ((((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (P \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \neq P)) \land (F (P) = G (P) \land F (Q) = G (Q))) \land (s \in A \land (\neg s \underset{˙}{\leq} W \land \neg s \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to (P \neq Q \land \neg s \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$
45		simpl3	$⊢ ((((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (P \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \neq P)) \land (F (P) = G (P) \land F (Q) = G (Q))) \land (s \in A \land (\neg s \underset{˙}{\leq} W \land \neg s \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to (F (P) = G (P) \land F (Q) = G (Q))$
46	1 2 3 4 5	cdlemd2	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land s \in A) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (P \neq Q \land \neg s \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land (F (P) = G (P) \land F (Q) = G (Q))) \to F (s) = G (s)$
47	13 14 17 16 37 44 45 46	syl331anc	$⊢ ((((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (P \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \neq P)) \land (F (P) = G (P) \land F (Q) = G (Q))) \land (s \in A \land (\neg s \underset{˙}{\leq} W \land \neg s \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to F (s) = G (s)$
48	1 2 3 4 5	cdlemd2	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (s \in A \land \neg s \underset{˙}{\leq} W) \land (P \neq s \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} s))) \land (F (P) = G (P) \land F (s) = G (s))) \to F (R) = G (R)$
49	13 14 15 16 19 41 42 47 48	syl332anc	$⊢ ((((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (P \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \neq P)) \land (F (P) = G (P) \land F (Q) = G (Q))) \land (s \in A \land (\neg s \underset{˙}{\leq} W \land \neg s \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to F (R) = G (R)$
50	12 49	rexlimddv	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R \in A) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (P \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \neq P)) \land (F (P) = G (P) \land F (Q) = G (Q))) \to F (R) = G (R)$

Metamath Proof Explorer

Theorem cdlemd4

Proof