bnj1173

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	bnj1173.3	$⊢ C = trCl (X, A, R) \cap B$
	bnj1173.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)$
	bnj1173.9	$⊢ (φ \land ψ) \to R FrSe A$
	bnj1173.17	$⊢ (φ \land ψ) \to X \in A$
Assertion	bnj1173	$⊢ (φ \land ψ \land z \in C) \to (θ \leftrightarrow w \in A)$

Proof

Step	Hyp	Ref	Expression
1		bnj1173.3	$⊢ C = trCl (X, A, R) \cap B$
2		bnj1173.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)$
3		bnj1173.9	$⊢ (φ \land ψ) \to R FrSe A$
4		bnj1173.17	$⊢ (φ \land ψ) \to X \in A$
5		3simpc	$⊢ ((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) \to ((R FrSe A \land z \in A) \land w \in A)$
6	3	3adant3	$⊢ (φ \land ψ \land z \in C) \to R FrSe A$
7	4	3adant3	$⊢ (φ \land ψ \land z \in C) \to X \in A$
8		elin	$⊢ z \in (trCl (X, A, R) \cap B) \leftrightarrow (z \in trCl (X, A, R) \land z \in B)$
9	8	simplbi	$⊢ z \in (trCl (X, A, R) \cap B) \to z \in trCl (X, A, R)$
10	9 1	eleq2s	$⊢ z \in C \to z \in trCl (X, A, R)$
11	10	3ad2ant3	$⊢ (φ \land ψ \land z \in C) \to z \in trCl (X, A, R)$
12		pm3.21	$⊢ (R FrSe A \land X \in A \land z \in trCl (X, A, R)) \to (((R FrSe A \land z \in A) \land w \in A) \to (((R FrSe A \land z \in A) \land w \in A) \land (R FrSe A \land X \in A \land z \in trCl (X, A, R))))$
13	6 7 11 12	syl3anc	$⊢ (φ \land ψ \land z \in C) \to (((R FrSe A \land z \in A) \land w \in A) \to (((R FrSe A \land z \in A) \land w \in A) \land (R FrSe A \land X \in A \land z \in trCl (X, A, R))))$
14		bnj170	$⊢ ((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) \leftrightarrow (((R FrSe A \land z \in A) \land w \in A) \land (R FrSe A \land X \in A \land z \in trCl (X, A, R)))$
15	13 14	imbitrrdi	$⊢ (φ \land ψ \land z \in C) \to (((R FrSe A \land z \in A) \land w \in A) \to ((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))$
16	5 15	impbid2	$⊢ (φ \land ψ \land z \in C) \to (((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) \leftrightarrow ((R FrSe A \land z \in A) \land w \in A))$
17	2 16	bitrid	$⊢ (φ \land ψ \land z \in C) \to (θ \leftrightarrow ((R FrSe A \land z \in A) \land w \in A))$
18		bnj1147	$⊢ trCl (X, A, R) \subseteq A$
19	18 11	bnj1213	$⊢ (φ \land ψ \land z \in C) \to z \in A$
20	6 19	jca	$⊢ (φ \land ψ \land z \in C) \to (R FrSe A \land z \in A)$
21	20	biantrurd	$⊢ (φ \land ψ \land z \in C) \to (w \in A \leftrightarrow ((R FrSe A \land z \in A) \land w \in A))$
22	17 21	bitr4d	$⊢ (φ \land ψ \land z \in C) \to (θ \leftrightarrow w \in A)$

Metamath Proof Explorer

Theorem bnj1173

Proof