cdlemg7N

Description: TODO: FIX COMMENT. (Contributed by NM, 28-Apr-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	cdlemg7.b	$⊢ B = {Base}_{K}$
	cdlemg7.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdlemg7.a	$⊢ A = Atoms (K)$
	cdlemg7.h	$⊢ H = LHyp (K)$
	cdlemg7.t	$⊢ T = LTrn (K) (W)$
Assertion	cdlemg7N	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land X \in B) \land (F \in T \land G \in T \land F (G (P)) = P)) \to F (G (X)) = X$

Proof

Step	Hyp	Ref	Expression
1		cdlemg7.b	$⊢ B = {Base}_{K}$
2		cdlemg7.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		cdlemg7.a	$⊢ A = Atoms (K)$
4		cdlemg7.h	$⊢ H = LHyp (K)$
5		cdlemg7.t	$⊢ T = LTrn (K) (W)$
6		simpl1	$⊢ (((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land X \in B) \land (F \in T \land G \in T \land F (G (P)) = P)) \land X \underset{˙}{\leq} W) \to (K \in HL \land W \in H)$
7		simpl31	$⊢ (((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land X \in B) \land (F \in T \land G \in T \land F (G (P)) = P)) \land X \underset{˙}{\leq} W) \to F \in T$
8		simpl32	$⊢ (((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land X \in B) \land (F \in T \land G \in T \land F (G (P)) = P)) \land X \underset{˙}{\leq} W) \to G \in T$
9		simpl2r	$⊢ (((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land X \in B) \land (F \in T \land G \in T \land F (G (P)) = P)) \land X \underset{˙}{\leq} W) \to X \in B$
10	1 4 5	ltrncl	$⊢ ((K \in HL \land W \in H) \land G \in T \land X \in B) \to G (X) \in B$
11	6 8 9 10	syl3anc	$⊢ (((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land X \in B) \land (F \in T \land G \in T \land F (G (P)) = P)) \land X \underset{˙}{\leq} W) \to G (X) \in B$
12		simpr	$⊢ (((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land X \in B) \land (F \in T \land G \in T \land F (G (P)) = P)) \land X \underset{˙}{\leq} W) \to X \underset{˙}{\leq} W$
13	1 2 4 5	ltrnval1	$⊢ ((K \in HL \land W \in H) \land G \in T \land (X \in B \land X \underset{˙}{\leq} W)) \to G (X) = X$
14	6 8 9 12 13	syl112anc	$⊢ (((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land X \in B) \land (F \in T \land G \in T \land F (G (P)) = P)) \land X \underset{˙}{\leq} W) \to G (X) = X$
15	14 12	eqbrtrd	$⊢ (((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land X \in B) \land (F \in T \land G \in T \land F (G (P)) = P)) \land X \underset{˙}{\leq} W) \to G (X) \underset{˙}{\leq} W$
16	1 2 4 5	ltrnval1	$⊢ ((K \in HL \land W \in H) \land F \in T \land (G (X) \in B \land G (X) \underset{˙}{\leq} W)) \to F (G (X)) = G (X)$
17	6 7 11 15 16	syl112anc	$⊢ (((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land X \in B) \land (F \in T \land G \in T \land F (G (P)) = P)) \land X \underset{˙}{\leq} W) \to F (G (X)) = G (X)$
18	17 14	eqtrd	$⊢ (((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land X \in B) \land (F \in T \land G \in T \land F (G (P)) = P)) \land X \underset{˙}{\leq} W) \to F (G (X)) = X$
19		simpl1	$⊢ (((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land X \in B) \land (F \in T \land G \in T \land F (G (P)) = P)) \land \neg X \underset{˙}{\leq} W) \to (K \in HL \land W \in H)$
20		simpl2l	$⊢ (((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land X \in B) \land (F \in T \land G \in T \land F (G (P)) = P)) \land \neg X \underset{˙}{\leq} W) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
21		simpl2r	$⊢ (((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land X \in B) \land (F \in T \land G \in T \land F (G (P)) = P)) \land \neg X \underset{˙}{\leq} W) \to X \in B$
22		simpr	$⊢ (((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land X \in B) \land (F \in T \land G \in T \land F (G (P)) = P)) \land \neg X \underset{˙}{\leq} W) \to \neg X \underset{˙}{\leq} W$
23	21 22	jca	$⊢ (((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land X \in B) \land (F \in T \land G \in T \land F (G (P)) = P)) \land \neg X \underset{˙}{\leq} W) \to (X \in B \land \neg X \underset{˙}{\leq} W)$
24		simpl31	$⊢ (((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land X \in B) \land (F \in T \land G \in T \land F (G (P)) = P)) \land \neg X \underset{˙}{\leq} W) \to F \in T$
25		simpl32	$⊢ (((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land X \in B) \land (F \in T \land G \in T \land F (G (P)) = P)) \land \neg X \underset{˙}{\leq} W) \to G \in T$
26		simpl33	$⊢ (((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land X \in B) \land (F \in T \land G \in T \land F (G (P)) = P)) \land \neg X \underset{˙}{\leq} W) \to F (G (P)) = P$
27	1 2 3 4 5	cdlemg7aN	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (X \in B \land \neg X \underset{˙}{\leq} W)) \land (F \in T \land G \in T \land F (G (P)) = P)) \to F (G (X)) = X$
28	19 20 23 24 25 26 27	syl123anc	$⊢ (((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land X \in B) \land (F \in T \land G \in T \land F (G (P)) = P)) \land \neg X \underset{˙}{\leq} W) \to F (G (X)) = X$
29	18 28	pm2.61dan	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land X \in B) \land (F \in T \land G \in T \land F (G (P)) = P)) \to F (G (X)) = X$

Metamath Proof Explorer

Theorem cdlemg7N

Proof