bnj1175

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	bnj1175.3	$⊢ C = trCl (X, A, R) \cap B$
	bnj1175.4	$⊢ χ \leftrightarrow ((R FrSe A \land X \in A \land z \in trCl (X, A, R)) \land (R FrSe A \land z \in A) \land (w \in A \land w R z))$
	bnj1175.5	$⊢ θ \leftrightarrow ((R FrSe A \land X \in A \land z \in trCl (X, A, R)) \land (R FrSe A \land z \in A) \land w \in A)$
Assertion	bnj1175	$⊢ θ \to (w R z \to w \in trCl (X, A, R))$

Proof

Step	Hyp	Ref	Expression
1		bnj1175.3	$⊢ C = trCl (X, A, R) \cap B$
2		bnj1175.4	$⊢ χ \leftrightarrow ((R FrSe A \land X \in A \land z \in trCl (X, A, R)) \land (R FrSe A \land z \in A) \land (w \in A \land w R z))$
3		bnj1175.5	$⊢ θ \leftrightarrow ((R FrSe A \land X \in A \land z \in trCl (X, A, R)) \land (R FrSe A \land z \in A) \land w \in A)$
4		bnj255	$⊢ ((R FrSe A \land X \in A \land z \in trCl (X, A, R)) \land (R FrSe A \land z \in A) \land w \in A \land w R z) \leftrightarrow ((R FrSe A \land X \in A \land z \in trCl (X, A, R)) \land (R FrSe A \land z \in A) \land (w \in A \land w R z))$
5		df-bnj17	$⊢ ((R FrSe A \land X \in A \land z \in trCl (X, A, R)) \land (R FrSe A \land z \in A) \land w \in A \land w R z) \leftrightarrow (((R FrSe A \land X \in A \land z \in trCl (X, A, R)) \land (R FrSe A \land z \in A) \land w \in A) \land w R z)$
6	2 4 5	3bitr2i	$⊢ χ \leftrightarrow (((R FrSe A \land X \in A \land z \in trCl (X, A, R)) \land (R FrSe A \land z \in A) \land w \in A) \land w R z)$
7	3	anbi1i	$⊢ (θ \land w R z) \leftrightarrow (((R FrSe A \land X \in A \land z \in trCl (X, A, R)) \land (R FrSe A \land z \in A) \land w \in A) \land w R z)$
8	6 7	bitr4i	$⊢ χ \leftrightarrow (θ \land w R z)$
9		bnj1125	$⊢ (R FrSe A \land X \in A \land z \in trCl (X, A, R)) \to trCl (z, A, R) \subseteq trCl (X, A, R)$
10	2 9	bnj835	$⊢ χ \to trCl (z, A, R) \subseteq trCl (X, A, R)$
11		bnj906	$⊢ (R FrSe A \land z \in A) \to pred (z, A, R) \subseteq trCl (z, A, R)$
12	2 11	bnj836	$⊢ χ \to pred (z, A, R) \subseteq trCl (z, A, R)$
13		bnj1152	$⊢ w \in pred (z, A, R) \leftrightarrow (w \in A \land w R z)$
14	13	biimpri	$⊢ (w \in A \land w R z) \to w \in pred (z, A, R)$
15	2 14	bnj837	$⊢ χ \to w \in pred (z, A, R)$
16	12 15	sseldd	$⊢ χ \to w \in trCl (z, A, R)$
17	10 16	sseldd	$⊢ χ \to w \in trCl (X, A, R)$
18	8 17	sylbir	$⊢ (θ \land w R z) \to w \in trCl (X, A, R)$
19	18	ex	$⊢ θ \to (w R z \to w \in trCl (X, A, R))$

Metamath Proof Explorer

Theorem bnj1175

Proof