bnj1172

Description: Technical lemma for bnj69 . This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

	Ref	Expression
Hypotheses	bnj1172.3	$⊢ C = trCl (X, A, R) \cap B$
	bnj1172.96	$⊢ \exists z \forall w ((φ \land ψ) \to ((φ \land ψ \land z \in C) \land (θ \to (w R z \to \neg w \in B))))$
	bnj1172.113	$⊢ (φ \land ψ \land z \in C) \to (θ \leftrightarrow w \in A)$
Assertion	bnj1172	$⊢ \exists z \forall w ((φ \land ψ) \to (z \in B \land (w \in A \to (w R z \to \neg w \in B))))$

Proof

Step	Hyp	Ref	Expression
1		bnj1172.3	$⊢ C = trCl (X, A, R) \cap B$
2		bnj1172.96	$⊢ \exists z \forall w ((φ \land ψ) \to ((φ \land ψ \land z \in C) \land (θ \to (w R z \to \neg w \in B))))$
3		bnj1172.113	$⊢ (φ \land ψ \land z \in C) \to (θ \leftrightarrow w \in A)$
4	3	imbi1d	$⊢ (φ \land ψ \land z \in C) \to ((θ \to (w R z \to \neg w \in B)) \leftrightarrow (w \in A \to (w R z \to \neg w \in B)))$
5	4	pm5.32i	$⊢ ((φ \land ψ \land z \in C) \land (θ \to (w R z \to \neg w \in B))) \leftrightarrow ((φ \land ψ \land z \in C) \land (w \in A \to (w R z \to \neg w \in B)))$
6	5	imbi2i	$⊢ ((φ \land ψ) \to ((φ \land ψ \land z \in C) \land (θ \to (w R z \to \neg w \in B)))) \leftrightarrow ((φ \land ψ) \to ((φ \land ψ \land z \in C) \land (w \in A \to (w R z \to \neg w \in B))))$
7	6	albii	$⊢ \forall w ((φ \land ψ) \to ((φ \land ψ \land z \in C) \land (θ \to (w R z \to \neg w \in B)))) \leftrightarrow \forall w ((φ \land ψ) \to ((φ \land ψ \land z \in C) \land (w \in A \to (w R z \to \neg w \in B))))$
8	7	exbii	$⊢ \exists z \forall w ((φ \land ψ) \to ((φ \land ψ \land z \in C) \land (θ \to (w R z \to \neg w \in B)))) \leftrightarrow \exists z \forall w ((φ \land ψ) \to ((φ \land ψ \land z \in C) \land (w \in A \to (w R z \to \neg w \in B))))$
9	2 8	mpbi	$⊢ \exists z \forall w ((φ \land ψ) \to ((φ \land ψ \land z \in C) \land (w \in A \to (w R z \to \neg w \in B))))$
10		simp3	$⊢ (φ \land ψ \land z \in C) \to z \in C$
11	10 1	eleqtrdi	$⊢ (φ \land ψ \land z \in C) \to z \in (trCl (X, A, R) \cap B)$
12	11	elin2d	$⊢ (φ \land ψ \land z \in C) \to z \in B$
13	12	anim1i	$⊢ ((φ \land ψ \land z \in C) \land (w \in A \to (w R z \to \neg w \in B))) \to (z \in B \land (w \in A \to (w R z \to \neg w \in B)))$
14	13	imim2i	$⊢ ((φ \land ψ) \to ((φ \land ψ \land z \in C) \land (w \in A \to (w R z \to \neg w \in B)))) \to ((φ \land ψ) \to (z \in B \land (w \in A \to (w R z \to \neg w \in B))))$
15	14	alimi	$⊢ \forall w ((φ \land ψ) \to ((φ \land ψ \land z \in C) \land (w \in A \to (w R z \to \neg w \in B)))) \to \forall w ((φ \land ψ) \to (z \in B \land (w \in A \to (w R z \to \neg w \in B))))$
16	9 15	bnj101	$⊢ \exists z \forall w ((φ \land ψ) \to (z \in B \land (w \in A \to (w R z \to \neg w \in B))))$

Metamath Proof Explorer

Theorem bnj1172

Proof