cdlemk39s

Description: Substitution version of cdlemk39 . TODO: Can any commonality with cdlemk35s be exploited? (Contributed by NM, 23-Jul-2013)

	Ref	Expression
Hypotheses	cdlemk5.b	$⊢ B = {Base}_{K}$
	cdlemk5.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdlemk5.j	$⊢ \underset{˙}{\lor} = join (K)$
	cdlemk5.m	$⊢ \underset{˙}{\land} = meet (K)$
	cdlemk5.a	$⊢ A = Atoms (K)$
	cdlemk5.h	$⊢ H = LHyp (K)$
	cdlemk5.t	$⊢ T = LTrn (K) (W)$
	cdlemk5.r	$⊢ R = trL (K) (W)$
	cdlemk5.z	$⊢ Z = (P \underset{˙}{\lor} R (b)) \underset{˙}{\land} (N (P) \underset{˙}{\lor} R (b \circ F^{-1}))$
	cdlemk5.y	$⊢ Y = (P \underset{˙}{\lor} R (g)) \underset{˙}{\land} (Z \underset{˙}{\lor} R (g \circ b^{-1}))$
	cdlemk5.x	$⊢ X = (ι z \in T \| \forall b \in T ((b \neq {I ↾}_{B} \land R (b) \neq R (F) \land R (b) \neq R (g)) \to z (P) = Y))$
Assertion	cdlemk39s	$⊢ ((K \in HL \land W \in H) \land ((F \in T \land F \neq {I ↾}_{B}) \land (G \in T \land G \neq {I ↾}_{B}) \land N \in T) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N))) \to R (⦋ G / g ⦌ X) \underset{˙}{\leq} R (G)$

Proof

Step	Hyp	Ref	Expression
1		cdlemk5.b	$⊢ B = {Base}_{K}$
2		cdlemk5.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		cdlemk5.j	$⊢ \underset{˙}{\lor} = join (K)$
4		cdlemk5.m	$⊢ \underset{˙}{\land} = meet (K)$
5		cdlemk5.a	$⊢ A = Atoms (K)$
6		cdlemk5.h	$⊢ H = LHyp (K)$
7		cdlemk5.t	$⊢ T = LTrn (K) (W)$
8		cdlemk5.r	$⊢ R = trL (K) (W)$
9		cdlemk5.z	$⊢ Z = (P \underset{˙}{\lor} R (b)) \underset{˙}{\land} (N (P) \underset{˙}{\lor} R (b \circ F^{-1}))$
10		cdlemk5.y	$⊢ Y = (P \underset{˙}{\lor} R (g)) \underset{˙}{\land} (Z \underset{˙}{\lor} R (g \circ b^{-1}))$
11		cdlemk5.x	$⊢ X = (ι z \in T \| \forall b \in T ((b \neq {I ↾}_{B} \land R (b) \neq R (F) \land R (b) \neq R (g)) \to z (P) = Y))$
12		simp22l	$⊢ ((K \in HL \land W \in H) \land ((F \in T \land F \neq {I ↾}_{B}) \land (G \in T \land G \neq {I ↾}_{B}) \land N \in T) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N))) \to G \in T$
13	1 2 3 4 5 6 7 8 9 10 11	cdlemk39	$⊢ ((K \in HL \land W \in H) \land ((F \in T \land F \neq {I ↾}_{B}) \land (g \in T \land g \neq {I ↾}_{B}) \land N \in T) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N))) \to R (X) \underset{˙}{\leq} R (g)$
14	13	sbcth	$⊢ G \in T \to \underset{˙}{[} G / g \underset{˙}{]} (((K \in HL \land W \in H) \land ((F \in T \land F \neq {I ↾}_{B}) \land (g \in T \land g \neq {I ↾}_{B}) \land N \in T) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N))) \to R (X) \underset{˙}{\leq} R (g))$
15		sbcimg	$⊢ G \in T \to (\underset{˙}{[} G / g \underset{˙}{]} (((K \in HL \land W \in H) \land ((F \in T \land F \neq {I ↾}_{B}) \land (g \in T \land g \neq {I ↾}_{B}) \land N \in T) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N))) \to R (X) \underset{˙}{\leq} R (g)) \leftrightarrow (\underset{˙}{[} G / g \underset{˙}{]} ((K \in HL \land W \in H) \land ((F \in T \land F \neq {I ↾}_{B}) \land (g \in T \land g \neq {I ↾}_{B}) \land N \in T) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N))) \to \underset{˙}{[} G / g \underset{˙}{]} R (X) \underset{˙}{\leq} R (g)))$
16	14 15	mpbid	$⊢ G \in T \to (\underset{˙}{[} G / g \underset{˙}{]} ((K \in HL \land W \in H) \land ((F \in T \land F \neq {I ↾}_{B}) \land (g \in T \land g \neq {I ↾}_{B}) \land N \in T) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N))) \to \underset{˙}{[} G / g \underset{˙}{]} R (X) \underset{˙}{\leq} R (g))$
17		eleq1	$⊢ g = G \to (g \in T \leftrightarrow G \in T)$
18		neeq1	$⊢ g = G \to (g \neq {I ↾}_{B} \leftrightarrow G \neq {I ↾}_{B})$
19	17 18	anbi12d	$⊢ g = G \to ((g \in T \land g \neq {I ↾}_{B}) \leftrightarrow (G \in T \land G \neq {I ↾}_{B}))$
20	19	3anbi2d	$⊢ g = G \to (((F \in T \land F \neq {I ↾}_{B}) \land (g \in T \land g \neq {I ↾}_{B}) \land N \in T) \leftrightarrow ((F \in T \land F \neq {I ↾}_{B}) \land (G \in T \land G \neq {I ↾}_{B}) \land N \in T))$
21	20	3anbi2d	$⊢ g = G \to (((K \in HL \land W \in H) \land ((F \in T \land F \neq {I ↾}_{B}) \land (g \in T \land g \neq {I ↾}_{B}) \land N \in T) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N))) \leftrightarrow ((K \in HL \land W \in H) \land ((F \in T \land F \neq {I ↾}_{B}) \land (G \in T \land G \neq {I ↾}_{B}) \land N \in T) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N))))$
22	21	sbcieg	$⊢ G \in T \to (\underset{˙}{[} G / g \underset{˙}{]} ((K \in HL \land W \in H) \land ((F \in T \land F \neq {I ↾}_{B}) \land (g \in T \land g \neq {I ↾}_{B}) \land N \in T) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N))) \leftrightarrow ((K \in HL \land W \in H) \land ((F \in T \land F \neq {I ↾}_{B}) \land (G \in T \land G \neq {I ↾}_{B}) \land N \in T) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N))))$
23		sbcbr12g	$⊢ G \in T \to (\underset{˙}{[} G / g \underset{˙}{]} R (X) \underset{˙}{\leq} R (g) \leftrightarrow ⦋ G / g ⦌ R (X) \underset{˙}{\leq} ⦋ G / g ⦌ R (g))$
24		csbfv2g	$⊢ G \in T \to ⦋ G / g ⦌ R (X) = R (⦋ G / g ⦌ X)$
25		csbfv	$⊢ ⦋ G / g ⦌ R (g) = R (G)$
26	25	a1i	$⊢ G \in T \to ⦋ G / g ⦌ R (g) = R (G)$
27	24 26	breq12d	$⊢ G \in T \to (⦋ G / g ⦌ R (X) \underset{˙}{\leq} ⦋ G / g ⦌ R (g) \leftrightarrow R (⦋ G / g ⦌ X) \underset{˙}{\leq} R (G))$
28	23 27	bitrd	$⊢ G \in T \to (\underset{˙}{[} G / g \underset{˙}{]} R (X) \underset{˙}{\leq} R (g) \leftrightarrow R (⦋ G / g ⦌ X) \underset{˙}{\leq} R (G))$
29	16 22 28	3imtr3d	$⊢ G \in T \to (((K \in HL \land W \in H) \land ((F \in T \land F \neq {I ↾}_{B}) \land (G \in T \land G \neq {I ↾}_{B}) \land N \in T) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N))) \to R (⦋ G / g ⦌ X) \underset{˙}{\leq} R (G))$
30	12 29	mpcom	$⊢ ((K \in HL \land W \in H) \land ((F \in T \land F \neq {I ↾}_{B}) \land (G \in T \land G \neq {I ↾}_{B}) \land N \in T) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N))) \to R (⦋ G / g ⦌ X) \underset{˙}{\leq} R (G)$

Metamath Proof Explorer

Theorem cdlemk39s

Proof