cdlemg6c

	Ref	Expression
Hypotheses	cdlemg4.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdlemg4.a	$⊢ A = Atoms (K)$
	cdlemg4.h	$⊢ H = LHyp (K)$
	cdlemg4.t	$⊢ T = LTrn (K) (W)$
	cdlemg4.r	$⊢ R = trL (K) (W)$
	cdlemg4.j	$⊢ \underset{˙}{\lor} = join (K)$
	cdlemg4b.v	$⊢ V = R (G)$
Assertion	cdlemg6c	$⊢ ((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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land F (G (P)) = P)) \to (((r \in A \land \neg r \underset{˙}{\leq} W) \land \neg r \underset{˙}{\leq} (P \underset{˙}{\lor} V)) \to F (G (Q)) = Q)$

Proof

Step	Hyp	Ref	Expression
1		cdlemg4.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		cdlemg4.a	$⊢ A = Atoms (K)$
3		cdlemg4.h	$⊢ H = LHyp (K)$
4		cdlemg4.t	$⊢ T = LTrn (K) (W)$
5		cdlemg4.r	$⊢ R = trL (K) (W)$
6		cdlemg4.j	$⊢ \underset{˙}{\lor} = join (K)$
7		cdlemg4b.v	$⊢ V = R (G)$
8		simpl1	$⊢ (((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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land F (G (P)) = P)) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land \neg r \underset{˙}{\leq} (P \underset{˙}{\lor} V))) \to (K \in HL \land W \in H)$
9		simprl	$⊢ (((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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land F (G (P)) = P)) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land \neg r \underset{˙}{\leq} (P \underset{˙}{\lor} V))) \to (r \in A \land \neg r \underset{˙}{\leq} W)$
10		simpl22	$⊢ (((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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land F (G (P)) = P)) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land \neg r \underset{˙}{\leq} (P \underset{˙}{\lor} V))) \to (Q \in A \land \neg Q \underset{˙}{\leq} W)$
11		simpl23	$⊢ (((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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land F (G (P)) = P)) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land \neg r \underset{˙}{\leq} (P \underset{˙}{\lor} V))) \to F \in T$
12		simpl31	$⊢ (((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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land F (G (P)) = P)) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land \neg r \underset{˙}{\leq} (P \underset{˙}{\lor} V))) \to G \in T$
13		simprr	$⊢ (((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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land F (G (P)) = P)) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land \neg r \underset{˙}{\leq} (P \underset{˙}{\lor} V))) \to \neg r \underset{˙}{\leq} (P \underset{˙}{\lor} V)$
14		simpl1l	$⊢ (((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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land F (G (P)) = P)) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land \neg r \underset{˙}{\leq} (P \underset{˙}{\lor} V))) \to K \in HL$
15		simp22l	$⊢ ((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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land F (G (P)) = P)) \to Q \in A$
16	15	adantr	$⊢ (((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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land F (G (P)) = P)) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land \neg r \underset{˙}{\leq} (P \underset{˙}{\lor} V))) \to Q \in A$
17		simprll	$⊢ (((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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land F (G (P)) = P)) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land \neg r \underset{˙}{\leq} (P \underset{˙}{\lor} V))) \to r \in A$
18		eqid	$⊢ {Base}_{K} = {Base}_{K}$
19	18 3 4 5	trlcl	$⊢ ((K \in HL \land W \in H) \land G \in T) \to R (G) \in {Base}_{K}$
20	8 12 19	syl2anc	$⊢ (((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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land F (G (P)) = P)) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land \neg r \underset{˙}{\leq} (P \underset{˙}{\lor} V))) \to R (G) \in {Base}_{K}$
21	7 20	eqeltrid	$⊢ (((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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land F (G (P)) = P)) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land \neg r \underset{˙}{\leq} (P \underset{˙}{\lor} V))) \to V \in {Base}_{K}$
22		simp22r	$⊢ ((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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land F (G (P)) = P)) \to \neg Q \underset{˙}{\leq} W$
23	22	adantr	$⊢ (((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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land F (G (P)) = P)) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land \neg r \underset{˙}{\leq} (P \underset{˙}{\lor} V))) \to \neg Q \underset{˙}{\leq} W$
24	1 3 4 5	trlle	$⊢ ((K \in HL \land W \in H) \land G \in T) \to R (G) \underset{˙}{\leq} W$
25	8 12 24	syl2anc	$⊢ (((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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land F (G (P)) = P)) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land \neg r \underset{˙}{\leq} (P \underset{˙}{\lor} V))) \to R (G) \underset{˙}{\leq} W$
26	7 25	eqbrtrid	$⊢ (((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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land F (G (P)) = P)) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land \neg r \underset{˙}{\leq} (P \underset{˙}{\lor} V))) \to V \underset{˙}{\leq} W$
27		simp1l	$⊢ ((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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land F (G (P)) = P)) \to K \in HL$
28	27	hllatd	$⊢ ((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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land F (G (P)) = P)) \to K \in Lat$
29	28	adantr	$⊢ (((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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land F (G (P)) = P)) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land \neg r \underset{˙}{\leq} (P \underset{˙}{\lor} V))) \to K \in Lat$
30	18 2	atbase	$⊢ Q \in A \to Q \in {Base}_{K}$
31	15 30	syl	$⊢ ((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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land F (G (P)) = P)) \to Q \in {Base}_{K}$
32	31	adantr	$⊢ (((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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land F (G (P)) = P)) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land \neg r \underset{˙}{\leq} (P \underset{˙}{\lor} V))) \to Q \in {Base}_{K}$
33		simp1r	$⊢ ((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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land F (G (P)) = P)) \to W \in H$
34	18 3	lhpbase	$⊢ W \in H \to W \in {Base}_{K}$
35	33 34	syl	$⊢ ((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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land F (G (P)) = P)) \to W \in {Base}_{K}$
36	35	adantr	$⊢ (((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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land F (G (P)) = P)) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land \neg r \underset{˙}{\leq} (P \underset{˙}{\lor} V))) \to W \in {Base}_{K}$
37	18 1	lattr	$⊢ (K \in Lat \land (Q \in {Base}_{K} \land V \in {Base}_{K} \land W \in {Base}_{K})) \to ((Q \underset{˙}{\leq} V \land V \underset{˙}{\leq} W) \to Q \underset{˙}{\leq} W)$
38	29 32 21 36 37	syl13anc	$⊢ (((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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land F (G (P)) = P)) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land \neg r \underset{˙}{\leq} (P \underset{˙}{\lor} V))) \to ((Q \underset{˙}{\leq} V \land V \underset{˙}{\leq} W) \to Q \underset{˙}{\leq} W)$
39	26 38	mpan2d	$⊢ (((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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land F (G (P)) = P)) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land \neg r \underset{˙}{\leq} (P \underset{˙}{\lor} V))) \to (Q \underset{˙}{\leq} V \to Q \underset{˙}{\leq} W)$
40	23 39	mtod	$⊢ (((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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land F (G (P)) = P)) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land \neg r \underset{˙}{\leq} (P \underset{˙}{\lor} V))) \to \neg Q \underset{˙}{\leq} V$
41	18 1 6 2	hlexch2	$⊢ (K \in HL \land (Q \in A \land r \in A \land V \in {Base}_{K}) \land \neg Q \underset{˙}{\leq} V) \to (Q \underset{˙}{\leq} (r \underset{˙}{\lor} V) \to r \underset{˙}{\leq} (Q \underset{˙}{\lor} V))$
42	14 16 17 21 40 41	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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land F (G (P)) = P)) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land \neg r \underset{˙}{\leq} (P \underset{˙}{\lor} V))) \to (Q \underset{˙}{\leq} (r \underset{˙}{\lor} V) \to r \underset{˙}{\leq} (Q \underset{˙}{\lor} V))$
43		simpl32	$⊢ (((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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land F (G (P)) = P)) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land \neg r \underset{˙}{\leq} (P \underset{˙}{\lor} V))) \to Q \underset{˙}{\leq} (P \underset{˙}{\lor} V)$
44		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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land F (G (P)) = P)) \to P \in A$
45	44	adantr	$⊢ (((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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land F (G (P)) = P)) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land \neg r \underset{˙}{\leq} (P \underset{˙}{\lor} V))) \to P \in A$
46	18 2	atbase	$⊢ P \in A \to P \in {Base}_{K}$
47	45 46	syl	$⊢ (((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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land F (G (P)) = P)) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land \neg r \underset{˙}{\leq} (P \underset{˙}{\lor} V))) \to P \in {Base}_{K}$
48	18 1 6	latlej2	$⊢ (K \in Lat \land P \in {Base}_{K} \land V \in {Base}_{K}) \to V \underset{˙}{\leq} (P \underset{˙}{\lor} V)$
49	29 47 21 48	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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land F (G (P)) = P)) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land \neg r \underset{˙}{\leq} (P \underset{˙}{\lor} V))) \to V \underset{˙}{\leq} (P \underset{˙}{\lor} V)$
50	18 6	latjcl	$⊢ (K \in Lat \land P \in {Base}_{K} \land V \in {Base}_{K}) \to P \underset{˙}{\lor} V \in {Base}_{K}$
51	29 47 21 50	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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land F (G (P)) = P)) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land \neg r \underset{˙}{\leq} (P \underset{˙}{\lor} V))) \to P \underset{˙}{\lor} V \in {Base}_{K}$
52	18 1 6	latjle12	$⊢ (K \in Lat \land (Q \in {Base}_{K} \land V \in {Base}_{K} \land P \underset{˙}{\lor} V \in {Base}_{K})) \to ((Q \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land V \underset{˙}{\leq} (P \underset{˙}{\lor} V)) \leftrightarrow (Q \underset{˙}{\lor} V) \underset{˙}{\leq} (P \underset{˙}{\lor} V))$
53	29 32 21 51 52	syl13anc	$⊢ (((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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land F (G (P)) = P)) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land \neg r \underset{˙}{\leq} (P \underset{˙}{\lor} V))) \to ((Q \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land V \underset{˙}{\leq} (P \underset{˙}{\lor} V)) \leftrightarrow (Q \underset{˙}{\lor} V) \underset{˙}{\leq} (P \underset{˙}{\lor} V))$
54	43 49 53	mpbi2and	$⊢ (((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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land F (G (P)) = P)) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land \neg r \underset{˙}{\leq} (P \underset{˙}{\lor} V))) \to (Q \underset{˙}{\lor} V) \underset{˙}{\leq} (P \underset{˙}{\lor} V)$
55	18 2	atbase	$⊢ r \in A \to r \in {Base}_{K}$
56	17 55	syl	$⊢ (((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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land F (G (P)) = P)) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land \neg r \underset{˙}{\leq} (P \underset{˙}{\lor} V))) \to r \in {Base}_{K}$
57	18 6	latjcl	$⊢ (K \in Lat \land Q \in {Base}_{K} \land V \in {Base}_{K}) \to Q \underset{˙}{\lor} V \in {Base}_{K}$
58	29 32 21 57	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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land F (G (P)) = P)) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land \neg r \underset{˙}{\leq} (P \underset{˙}{\lor} V))) \to Q \underset{˙}{\lor} V \in {Base}_{K}$
59	18 1	lattr	$⊢ (K \in Lat \land (r \in {Base}_{K} \land Q \underset{˙}{\lor} V \in {Base}_{K} \land P \underset{˙}{\lor} V \in {Base}_{K})) \to ((r \underset{˙}{\leq} (Q \underset{˙}{\lor} V) \land (Q \underset{˙}{\lor} V) \underset{˙}{\leq} (P \underset{˙}{\lor} V)) \to r \underset{˙}{\leq} (P \underset{˙}{\lor} V))$
60	29 56 58 51 59	syl13anc	$⊢ (((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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land F (G (P)) = P)) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land \neg r \underset{˙}{\leq} (P \underset{˙}{\lor} V))) \to ((r \underset{˙}{\leq} (Q \underset{˙}{\lor} V) \land (Q \underset{˙}{\lor} V) \underset{˙}{\leq} (P \underset{˙}{\lor} V)) \to r \underset{˙}{\leq} (P \underset{˙}{\lor} V))$
61	54 60	mpan2d	$⊢ (((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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land F (G (P)) = P)) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land \neg r \underset{˙}{\leq} (P \underset{˙}{\lor} V))) \to (r \underset{˙}{\leq} (Q \underset{˙}{\lor} V) \to r \underset{˙}{\leq} (P \underset{˙}{\lor} V))$
62	42 61	syld	$⊢ (((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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land F (G (P)) = P)) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land \neg r \underset{˙}{\leq} (P \underset{˙}{\lor} V))) \to (Q \underset{˙}{\leq} (r \underset{˙}{\lor} V) \to r \underset{˙}{\leq} (P \underset{˙}{\lor} V))$
63	13 62	mtod	$⊢ (((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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land F (G (P)) = P)) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land \neg r \underset{˙}{\leq} (P \underset{˙}{\lor} V))) \to \neg Q \underset{˙}{\leq} (r \underset{˙}{\lor} V)$
64		simpl21	$⊢ (((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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land F (G (P)) = P)) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land \neg r \underset{˙}{\leq} (P \underset{˙}{\lor} V))) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
65		simpl33	$⊢ (((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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land F (G (P)) = P)) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land \neg r \underset{˙}{\leq} (P \underset{˙}{\lor} V))) \to F (G (P)) = P$
66	1 2 3 4 5 6 7	cdlemg6a	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (r \in A \land \neg r \underset{˙}{\leq} W) \land F \in T) \land (G \in T \land \neg r \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land F (G (P)) = P)) \to F (G (r)) = r$
67	8 64 9 11 12 13 65 66	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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land F (G (P)) = P)) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land \neg r \underset{˙}{\leq} (P \underset{˙}{\lor} V))) \to F (G (r)) = r$
68	1 2 3 4 5 6 7	cdlemg6b	$⊢ ((K \in HL \land W \in H) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land F \in T) \land (G \in T \land \neg Q \underset{˙}{\leq} (r \underset{˙}{\lor} V) \land F (G (r)) = r)) \to F (G (Q)) = Q$
69	8 9 10 11 12 63 67 68	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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land F (G (P)) = P)) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land \neg r \underset{˙}{\leq} (P \underset{˙}{\lor} V))) \to F (G (Q)) = Q$
70	69	ex	$⊢ ((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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} V) \land F (G (P)) = P)) \to (((r \in A \land \neg r \underset{˙}{\leq} W) \land \neg r \underset{˙}{\leq} (P \underset{˙}{\lor} V)) \to F (G (Q)) = Q)$

Metamath Proof Explorer

Theorem cdlemg6c

Proof