cdlemkid

Description: The value of the tau function (in Lemma K of Crawley p. 118) on the identity relation. (Contributed by NM, 25-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	cdlemkid	$⊢ ((K \in HL \land W \in H) \land (F \in T \land N \in T \land R (F) = R (N)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land G = {I ↾}_{B})) \to ⦋ G / g ⦌ X = {I ↾}_{B}$

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	7	fvexi	$⊢ T \in V$
13		nfv	$⊢ Ⅎ b ((K \in HL \land W \in H) \land (F \in T \land N \in T \land R (F) = R (N)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land G = {I ↾}_{B}))$
14		nfcv	$⊢ \underline{Ⅎ} b G$
15		nfra1	$⊢ Ⅎ b \forall b \in T ((b \neq {I ↾}_{B} \land R (b) \neq R (F) \land R (b) \neq R (g)) \to z (P) = Y)$
16		nfcv	$⊢ \underline{Ⅎ} b T$
17	15 16	nfriota	$⊢ \underline{Ⅎ} b (ι 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))$
18	11 17	nfcxfr	$⊢ \underline{Ⅎ} b X$
19	14 18	nfcsbw	$⊢ \underline{Ⅎ} b ⦋ G / g ⦌ X$
20	19	nfeq1	$⊢ Ⅎ b ⦋ G / g ⦌ X = {I ↾}_{B}$
21	20	a1i	$⊢ ((K \in HL \land W \in H) \land (F \in T \land N \in T \land R (F) = R (N)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land G = {I ↾}_{B})) \to Ⅎ b ⦋ G / g ⦌ X = {I ↾}_{B}$
22	1 2 3 4 5 6 7 8 9 10 11	cdlemkid4	$⊢ ((K \in HL \land W \in H) \land (F \in T \land N \in T \land R (F) = R (N)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land G = {I ↾}_{B})) \to ⦋ G / g ⦌ 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 = {I ↾}_{B}))$
23		eqeq1	$⊢ {I ↾}_{B} = ⦋ G / g ⦌ X \to ({I ↾}_{B} = {I ↾}_{B} \leftrightarrow ⦋ G / g ⦌ X = {I ↾}_{B})$
24	23	adantl	$⊢ (((K \in HL \land W \in H) \land (F \in T \land N \in T \land R (F) = R (N)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land G = {I ↾}_{B})) \land {I ↾}_{B} = ⦋ G / g ⦌ X) \to ({I ↾}_{B} = {I ↾}_{B} \leftrightarrow ⦋ G / g ⦌ X = {I ↾}_{B})$
25		eqidd	$⊢ (b \in T \land (b \neq {I ↾}_{B} \land R (b) \neq R (F) \land R (b) \neq R (G))) \to {I ↾}_{B} = {I ↾}_{B}$
26	25	a1i	$⊢ ((K \in HL \land W \in H) \land (F \in T \land N \in T \land R (F) = R (N)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land G = {I ↾}_{B})) \to ((b \in T \land (b \neq {I ↾}_{B} \land R (b) \neq R (F) \land R (b) \neq R (G))) \to {I ↾}_{B} = {I ↾}_{B})$
27	1 2 3 4 5 6 7 8 9 10 11	cdlemkid5	$⊢ ((K \in HL \land W \in H) \land (F \in T \land N \in T \land R (F) = R (N)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land G = {I ↾}_{B})) \to ⦋ G / g ⦌ X \in T$
28	1 6 7 8	cdlemftr2	$⊢ (K \in HL \land W \in H) \to \exists b \in T (b \neq {I ↾}_{B} \land R (b) \neq R (F) \land R (b) \neq R (G))$
29	28	3ad2ant1	$⊢ ((K \in HL \land W \in H) \land (F \in T \land N \in T \land R (F) = R (N)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land G = {I ↾}_{B})) \to \exists b \in T (b \neq {I ↾}_{B} \land R (b) \neq R (F) \land R (b) \neq R (G))$
30	13 21 22 24 26 27 29	riotasv3d	$⊢ (((K \in HL \land W \in H) \land (F \in T \land N \in T \land R (F) = R (N)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land G = {I ↾}_{B})) \land T \in V) \to ⦋ G / g ⦌ X = {I ↾}_{B}$
31	12 30	mpan2	$⊢ ((K \in HL \land W \in H) \land (F \in T \land N \in T \land R (F) = R (N)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land G = {I ↾}_{B})) \to ⦋ G / g ⦌ X = {I ↾}_{B}$

Metamath Proof Explorer

Theorem cdlemkid

Proof