cdlemk35s

Description: Substitution version of cdlemk35 . (Contributed by NM, 22-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	cdlemk35s	$⊢ ((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 / g ⦌ X \in T$

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	cdlemk35	$⊢ ((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 X \in T$
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 X \in T)$
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 X \in T) \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{˙}{]} X \in T))$
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{˙}{]} X \in T)$
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		sbcel1g	$⊢ G \in T \to (\underset{˙}{[} G / g \underset{˙}{]} X \in T \leftrightarrow ⦋ G / g ⦌ X \in T)$
24	16 22 23	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 ⦋ G / g ⦌ X \in T)$
25	12 24	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 ⦋ G / g ⦌ X \in T$

Metamath Proof Explorer

Theorem cdlemk35s

Proof