cdlemefrs29clN

Description: TODO: NOT USED? Show closure of the unique element in cdlemefrs29cpre1 . (Contributed by NM, 29-Mar-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	cdlemefrs27.b	$⊢ B = {Base}_{K}$
	cdlemefrs27.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdlemefrs27.j	$⊢ \underset{˙}{\lor} = join (K)$
	cdlemefrs27.m	$⊢ \underset{˙}{\land} = meet (K)$
	cdlemefrs27.a	$⊢ A = Atoms (K)$
	cdlemefrs27.h	$⊢ H = LHyp (K)$
	cdlemefrs27.eq	$⊢ s = R \to (φ \leftrightarrow ψ)$
	cdlemefrs27.nb	$⊢ (((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 P \neq Q \land (s \in A \land (\neg s \underset{˙}{\leq} W \land φ))) \to N \in B$
	cdlemefrs27.rnb	$⊢ (((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 (P \neq Q \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land ψ) \to ⦋ R / s ⦌ N \in B$
	cdlemefrs29cl.o	$⊢ O = (ι z \in B \| \forall s \in A ((\neg s \underset{˙}{\leq} W \land s \underset{˙}{\lor} (R \underset{˙}{\land} W) = R) \to z = N \underset{˙}{\lor} (R \underset{˙}{\land} W)))$
Assertion	cdlemefrs29clN	$⊢ (((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 (P \neq Q \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land ψ) \to O \in B$

Proof

Step	Hyp	Ref	Expression
1		cdlemefrs27.b	$⊢ B = {Base}_{K}$
2		cdlemefrs27.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		cdlemefrs27.j	$⊢ \underset{˙}{\lor} = join (K)$
4		cdlemefrs27.m	$⊢ \underset{˙}{\land} = meet (K)$
5		cdlemefrs27.a	$⊢ A = Atoms (K)$
6		cdlemefrs27.h	$⊢ H = LHyp (K)$
7		cdlemefrs27.eq	$⊢ s = R \to (φ \leftrightarrow ψ)$
8		cdlemefrs27.nb	$⊢ (((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 P \neq Q \land (s \in A \land (\neg s \underset{˙}{\leq} W \land φ))) \to N \in B$
9		cdlemefrs27.rnb	$⊢ (((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 (P \neq Q \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land ψ) \to ⦋ R / s ⦌ N \in B$
10		cdlemefrs29cl.o	$⊢ O = (ι z \in B \| \forall s \in A ((\neg s \underset{˙}{\leq} W \land s \underset{˙}{\lor} (R \underset{˙}{\land} W) = R) \to z = N \underset{˙}{\lor} (R \underset{˙}{\land} W)))$
11		simpl11	$⊢ ((((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 (P \neq Q \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land ψ) \land s \in A) \to (K \in HL \land W \in H)$
12		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 (P \neq Q \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land ψ) \land s \in A) \to (R \in A \land \neg R \underset{˙}{\leq} W)$
13		simpl3	$⊢ ((((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 (P \neq Q \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land ψ) \land s \in A) \to ψ$
14		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 (P \neq Q \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land ψ) \land s \in A) \to s \in A$
15	1 2 3 4 5 6 7	cdlemefrs29pre00	$⊢ (((K \in HL \land W \in H) \land (R \in A \land \neg R \underset{˙}{\leq} W) \land ψ) \land s \in A) \to (((\neg s \underset{˙}{\leq} W \land φ) \land s \underset{˙}{\lor} (R \underset{˙}{\land} W) = R) \leftrightarrow (\neg s \underset{˙}{\leq} W \land s \underset{˙}{\lor} (R \underset{˙}{\land} W) = R))$
16	11 12 13 14 15	syl31anc	$⊢ ((((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 (P \neq Q \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land ψ) \land s \in A) \to (((\neg s \underset{˙}{\leq} W \land φ) \land s \underset{˙}{\lor} (R \underset{˙}{\land} W) = R) \leftrightarrow (\neg s \underset{˙}{\leq} W \land s \underset{˙}{\lor} (R \underset{˙}{\land} W) = R))$
17	16	imbi1d	$⊢ ((((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 (P \neq Q \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land ψ) \land s \in A) \to ((((\neg s \underset{˙}{\leq} W \land φ) \land s \underset{˙}{\lor} (R \underset{˙}{\land} W) = R) \to z = N \underset{˙}{\lor} (R \underset{˙}{\land} W)) \leftrightarrow ((\neg s \underset{˙}{\leq} W \land s \underset{˙}{\lor} (R \underset{˙}{\land} W) = R) \to z = N \underset{˙}{\lor} (R \underset{˙}{\land} W)))$
18	17	ralbidva	$⊢ (((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 (P \neq Q \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land ψ) \to (\forall s \in A (((\neg s \underset{˙}{\leq} W \land φ) \land s \underset{˙}{\lor} (R \underset{˙}{\land} W) = R) \to z = N \underset{˙}{\lor} (R \underset{˙}{\land} W)) \leftrightarrow \forall s \in A ((\neg s \underset{˙}{\leq} W \land s \underset{˙}{\lor} (R \underset{˙}{\land} W) = R) \to z = N \underset{˙}{\lor} (R \underset{˙}{\land} W)))$
19	18	riotabidv	$⊢ (((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 (P \neq Q \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land ψ) \to (ι z \in B \| \forall s \in A (((\neg s \underset{˙}{\leq} W \land φ) \land s \underset{˙}{\lor} (R \underset{˙}{\land} W) = R) \to z = N \underset{˙}{\lor} (R \underset{˙}{\land} W))) = (ι z \in B \| \forall s \in A ((\neg s \underset{˙}{\leq} W \land s \underset{˙}{\lor} (R \underset{˙}{\land} W) = R) \to z = N \underset{˙}{\lor} (R \underset{˙}{\land} W)))$
20	10 19	eqtr4id	$⊢ (((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 (P \neq Q \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land ψ) \to O = (ι z \in B \| \forall s \in A (((\neg s \underset{˙}{\leq} W \land φ) \land s \underset{˙}{\lor} (R \underset{˙}{\land} W) = R) \to z = N \underset{˙}{\lor} (R \underset{˙}{\land} W)))$
21	1 2 3 4 5 6 7 8 9	cdlemefrs29cpre1	$⊢ (((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 (P \neq Q \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land ψ) \to \exists! z \in B \forall s \in A (((\neg s \underset{˙}{\leq} W \land φ) \land s \underset{˙}{\lor} (R \underset{˙}{\land} W) = R) \to z = N \underset{˙}{\lor} (R \underset{˙}{\land} W))$
22		riotacl	$⊢ \exists! z \in B \forall s \in A (((\neg s \underset{˙}{\leq} W \land φ) \land s \underset{˙}{\lor} (R \underset{˙}{\land} W) = R) \to z = N \underset{˙}{\lor} (R \underset{˙}{\land} W)) \to (ι z \in B \| \forall s \in A (((\neg s \underset{˙}{\leq} W \land φ) \land s \underset{˙}{\lor} (R \underset{˙}{\land} W) = R) \to z = N \underset{˙}{\lor} (R \underset{˙}{\land} W))) \in B$
23	21 22	syl	$⊢ (((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 (P \neq Q \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land ψ) \to (ι z \in B \| \forall s \in A (((\neg s \underset{˙}{\leq} W \land φ) \land s \underset{˙}{\lor} (R \underset{˙}{\land} W) = R) \to z = N \underset{˙}{\lor} (R \underset{˙}{\land} W))) \in B$
24	20 23	eqeltrd	$⊢ (((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 (P \neq Q \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land ψ) \to O \in B$

Metamath Proof Explorer

Theorem cdlemefrs29clN

Proof