cdlemg6

	Ref	Expression
Hypotheses	cdlemg6.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdlemg6.a	$⊢ A = Atoms (K)$
	cdlemg6.h	$⊢ H = LHyp (K)$
	cdlemg6.t	$⊢ T = LTrn (K) (W)$
Assertion	cdlemg6	$⊢ ((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 F (G (P)) = P)) \to F (G (Q)) = Q$

Proof

Step	Hyp	Ref	Expression
1		cdlemg6.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		cdlemg6.a	$⊢ A = Atoms (K)$
3		cdlemg6.h	$⊢ H = LHyp (K)$
4		cdlemg6.t	$⊢ T = LTrn (K) (W)$
5		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 F (G (P)) = P)) \land Q \underset{˙}{\leq} (P join (K) trL (K) (W) (G))) \to (K \in HL \land W \in H)$
6		simpl2l	$⊢ (((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 F (G (P)) = P)) \land Q \underset{˙}{\leq} (P join (K) trL (K) (W) (G))) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
7		simpl2r	$⊢ (((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 F (G (P)) = P)) \land Q \underset{˙}{\leq} (P join (K) trL (K) (W) (G))) \to (Q \in A \land \neg Q \underset{˙}{\leq} W)$
8		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 F (G (P)) = P)) \land Q \underset{˙}{\leq} (P join (K) trL (K) (W) (G))) \to F \in T$
9		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 F (G (P)) = P)) \land Q \underset{˙}{\leq} (P join (K) trL (K) (W) (G))) \to G \in T$
10		simpr	$⊢ (((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 F (G (P)) = P)) \land Q \underset{˙}{\leq} (P join (K) trL (K) (W) (G))) \to Q \underset{˙}{\leq} (P join (K) trL (K) (W) (G))$
11		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 F (G (P)) = P)) \land Q \underset{˙}{\leq} (P join (K) trL (K) (W) (G))) \to F (G (P)) = P$
12		eqid	$⊢ trL (K) (W) = trL (K) (W)$
13		eqid	$⊢ join (K) = join (K)$
14		eqid	$⊢ trL (K) (W) (G) = trL (K) (W) (G)$
15	1 2 3 4 12 13 14	cdlemg6e	$⊢ ((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 join (K) trL (K) (W) (G)) \land F (G (P)) = P)) \to F (G (Q)) = Q$
16	5 6 7 8 9 10 11 15	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 F (G (P)) = P)) \land Q \underset{˙}{\leq} (P join (K) trL (K) (W) (G))) \to F (G (Q)) = Q$
17		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 F (G (P)) = P)) \land \neg Q \underset{˙}{\leq} (P join (K) trL (K) (W) (G))) \to (K \in HL \land W \in H)$
18		simpl2l	$⊢ (((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 F (G (P)) = P)) \land \neg Q \underset{˙}{\leq} (P join (K) trL (K) (W) (G))) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
19		simpl2r	$⊢ (((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 F (G (P)) = P)) \land \neg Q \underset{˙}{\leq} (P join (K) trL (K) (W) (G))) \to (Q \in A \land \neg Q \underset{˙}{\leq} W)$
20		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 F (G (P)) = P)) \land \neg Q \underset{˙}{\leq} (P join (K) trL (K) (W) (G))) \to F \in T$
21		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 F (G (P)) = P)) \land \neg Q \underset{˙}{\leq} (P join (K) trL (K) (W) (G))) \to G \in T$
22		simpr	$⊢ (((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 F (G (P)) = P)) \land \neg Q \underset{˙}{\leq} (P join (K) trL (K) (W) (G))) \to \neg Q \underset{˙}{\leq} (P join (K) trL (K) (W) (G))$
23		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 F (G (P)) = P)) \land \neg Q \underset{˙}{\leq} (P join (K) trL (K) (W) (G))) \to F (G (P)) = P$
24	1 2 3 4 12 13 14	cdlemg4	$⊢ ((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 \neg Q \underset{˙}{\leq} (P join (K) trL (K) (W) (G)) \land F (G (P)) = P)) \to F (G (Q)) = Q$
25	17 18 19 20 21 22 23 24	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 F (G (P)) = P)) \land \neg Q \underset{˙}{\leq} (P join (K) trL (K) (W) (G))) \to F (G (Q)) = Q$
26	16 25	pm2.61dan	$⊢ ((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 F (G (P)) = P)) \to F (G (Q)) = Q$

Metamath Proof Explorer

Theorem cdlemg6

Proof