bnj1174

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	bnj1174.3	$⊢ C = trCl (X, A, R) \cap B$
	bnj1174.59	$⊢ \exists z \forall w ((φ \land ψ) \to (z \in C \land (θ \to (w R z \to \neg w \in C))))$
	bnj1174.74	$⊢ θ \to (w R z \to w \in trCl (X, A, R))$
Assertion	bnj1174	$⊢ \exists z \forall w ((φ \land ψ) \to ((φ \land ψ \land z \in C) \land (θ \to (w R z \to \neg w \in B))))$

Proof

Step	Hyp	Ref	Expression
1		bnj1174.3	$⊢ C = trCl (X, A, R) \cap B$
2		bnj1174.59	$⊢ \exists z \forall w ((φ \land ψ) \to (z \in C \land (θ \to (w R z \to \neg w \in C))))$
3		bnj1174.74	$⊢ θ \to (w R z \to w \in trCl (X, A, R))$
4	1	eleq2i	$⊢ w \in C \leftrightarrow w \in (trCl (X, A, R) \cap B)$
5	4	notbii	$⊢ \neg w \in C \leftrightarrow \neg w \in (trCl (X, A, R) \cap B)$
6		ianor	$⊢ \neg (w \in trCl (X, A, R) \land w \in B) \leftrightarrow (\neg w \in trCl (X, A, R) \lor \neg w \in B)$
7		elin	$⊢ w \in (trCl (X, A, R) \cap B) \leftrightarrow (w \in trCl (X, A, R) \land w \in B)$
8	7	notbii	$⊢ \neg w \in (trCl (X, A, R) \cap B) \leftrightarrow \neg (w \in trCl (X, A, R) \land w \in B)$
9		pm4.62	$⊢ (w \in trCl (X, A, R) \to \neg w \in B) \leftrightarrow (\neg w \in trCl (X, A, R) \lor \neg w \in B)$
10	6 8 9	3bitr4i	$⊢ \neg w \in (trCl (X, A, R) \cap B) \leftrightarrow (w \in trCl (X, A, R) \to \neg w \in B)$
11	10	biimpi	$⊢ \neg w \in (trCl (X, A, R) \cap B) \to (w \in trCl (X, A, R) \to \neg w \in B)$
12	11	impcom	$⊢ (w \in trCl (X, A, R) \land \neg w \in (trCl (X, A, R) \cap B)) \to \neg w \in B$
13	5 12	sylan2b	$⊢ (w \in trCl (X, A, R) \land \neg w \in C) \to \neg w \in B$
14	13	ex	$⊢ w \in trCl (X, A, R) \to (\neg w \in C \to \neg w \in B)$
15	3 14	syl6	$⊢ θ \to (w R z \to (\neg w \in C \to \neg w \in B))$
16	15	a2d	$⊢ θ \to ((w R z \to \neg w \in C) \to (w R z \to \neg w \in B))$
17	16	biantru	$⊢ (z \in C \land (θ \to (w R z \to \neg w \in C))) \leftrightarrow ((z \in C \land (θ \to (w R z \to \neg w \in C))) \land (θ \to ((w R z \to \neg w \in C) \to (w R z \to \neg w \in B))))$
18		df-3an	$⊢ (z \in C \land (θ \to (w R z \to \neg w \in C)) \land (θ \to ((w R z \to \neg w \in C) \to (w R z \to \neg w \in B)))) \leftrightarrow ((z \in C \land (θ \to (w R z \to \neg w \in C))) \land (θ \to ((w R z \to \neg w \in C) \to (w R z \to \neg w \in B))))$
19		3anass	$⊢ (z \in C \land (θ \to (w R z \to \neg w \in C)) \land (θ \to ((w R z \to \neg w \in C) \to (w R z \to \neg w \in B)))) \leftrightarrow (z \in C \land ((θ \to (w R z \to \neg w \in C)) \land (θ \to ((w R z \to \neg w \in C) \to (w R z \to \neg w \in B)))))$
20	17 18 19	3bitr2i	$⊢ (z \in C \land (θ \to (w R z \to \neg w \in C))) \leftrightarrow (z \in C \land ((θ \to (w R z \to \neg w \in C)) \land (θ \to ((w R z \to \neg w \in C) \to (w R z \to \neg w \in B)))))$
21	20	imbi2i	$⊢ ((φ \land ψ) \to (z \in C \land (θ \to (w R z \to \neg w \in C)))) \leftrightarrow ((φ \land ψ) \to (z \in C \land ((θ \to (w R z \to \neg w \in C)) \land (θ \to ((w R z \to \neg w \in C) \to (w R z \to \neg w \in B))))))$
22	21	albii	$⊢ \forall w ((φ \land ψ) \to (z \in C \land (θ \to (w R z \to \neg w \in C)))) \leftrightarrow \forall w ((φ \land ψ) \to (z \in C \land ((θ \to (w R z \to \neg w \in C)) \land (θ \to ((w R z \to \neg w \in C) \to (w R z \to \neg w \in B))))))$
23	22	exbii	$⊢ \exists z \forall w ((φ \land ψ) \to (z \in C \land (θ \to (w R z \to \neg w \in C)))) \leftrightarrow \exists z \forall w ((φ \land ψ) \to (z \in C \land ((θ \to (w R z \to \neg w \in C)) \land (θ \to ((w R z \to \neg w \in C) \to (w R z \to \neg w \in B))))))$
24	2 23	mpbi	$⊢ \exists z \forall w ((φ \land ψ) \to (z \in C \land ((θ \to (w R z \to \neg w \in C)) \land (θ \to ((w R z \to \neg w \in C) \to (w R z \to \neg w \in B))))))$
25		imdi	$⊢ (θ \to ((w R z \to \neg w \in C) \to (w R z \to \neg w \in B))) \leftrightarrow ((θ \to (w R z \to \neg w \in C)) \to (θ \to (w R z \to \neg w \in B)))$
26		pm3.35	$⊢ ((θ \to (w R z \to \neg w \in C)) \land ((θ \to (w R z \to \neg w \in C)) \to (θ \to (w R z \to \neg w \in B)))) \to (θ \to (w R z \to \neg w \in B))$
27	25 26	sylan2b	$⊢ ((θ \to (w R z \to \neg w \in C)) \land (θ \to ((w R z \to \neg w \in C) \to (w R z \to \neg w \in B)))) \to (θ \to (w R z \to \neg w \in B))$
28	27	anim2i	$⊢ (z \in C \land ((θ \to (w R z \to \neg w \in C)) \land (θ \to ((w R z \to \neg w \in C) \to (w R z \to \neg w \in B))))) \to (z \in C \land (θ \to (w R z \to \neg w \in B)))$
29	28	imim2i	$⊢ ((φ \land ψ) \to (z \in C \land ((θ \to (w R z \to \neg w \in C)) \land (θ \to ((w R z \to \neg w \in C) \to (w R z \to \neg w \in B)))))) \to ((φ \land ψ) \to (z \in C \land (θ \to (w R z \to \neg w \in B))))$
30	29	alimi	$⊢ \forall w ((φ \land ψ) \to (z \in C \land ((θ \to (w R z \to \neg w \in C)) \land (θ \to ((w R z \to \neg w \in C) \to (w R z \to \neg w \in B)))))) \to \forall w ((φ \land ψ) \to (z \in C \land (θ \to (w R z \to \neg w \in B))))$
31	24 30	bnj101	$⊢ \exists z \forall w ((φ \land ψ) \to (z \in C \land (θ \to (w R z \to \neg w \in B))))$
32		ancl	$⊢ ((φ \land ψ) \to (z \in C \land (θ \to (w R z \to \neg w \in B)))) \to ((φ \land ψ) \to ((φ \land ψ) \land (z \in C \land (θ \to (w R z \to \neg w \in B)))))$
33		bnj256	$⊢ (φ \land ψ \land z \in C \land (θ \to (w R z \to \neg w \in B))) \leftrightarrow ((φ \land ψ) \land (z \in C \land (θ \to (w R z \to \neg w \in B))))$
34	32 33	syl6ibr	$⊢ ((φ \land ψ) \to (z \in C \land (θ \to (w R z \to \neg w \in B)))) \to ((φ \land ψ) \to (φ \land ψ \land z \in C \land (θ \to (w R z \to \neg w \in B))))$
35	34	alimi	$⊢ \forall w ((φ \land ψ) \to (z \in C \land (θ \to (w R z \to \neg w \in B)))) \to \forall w ((φ \land ψ) \to (φ \land ψ \land z \in C \land (θ \to (w R z \to \neg w \in B))))$
36	31 35	bnj101	$⊢ \exists z \forall w ((φ \land ψ) \to (φ \land ψ \land z \in C \land (θ \to (w R z \to \neg w \in B))))$
37		df-bnj17	$⊢ (φ \land ψ \land z \in C \land (θ \to (w R z \to \neg w \in B))) \leftrightarrow ((φ \land ψ \land z \in C) \land (θ \to (w R z \to \neg w \in B)))$
38	37	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 (θ \to (w R z \to \neg w \in B))))$
39	38	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 (θ \to (w R z \to \neg w \in B))))$
40	39	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 (θ \to (w R z \to \neg w \in B))))$
41	36 40	mpbi	$⊢ \exists z \forall w ((φ \land ψ) \to ((φ \land ψ \land z \in C) \land (θ \to (w R z \to \neg w \in B))))$

Metamath Proof Explorer

Theorem bnj1174

Proof