bnj1177

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	bnj1177.2	$⊢ ψ \leftrightarrow (X \in B \land y \in B \land y R X)$
	bnj1177.3	$⊢ C = trCl (X, A, R) \cap B$
	bnj1177.9	$⊢ (φ \land ψ) \to R FrSe A$
	bnj1177.13	$⊢ (φ \land ψ) \to B \subseteq A$
	bnj1177.17	$⊢ (φ \land ψ) \to X \in A$
Assertion	bnj1177	$⊢ (φ \land ψ) \to (R Fr A \land C \subseteq A \land C \neq \emptyset \land C \in V)$

Proof

Step	Hyp	Ref	Expression
1		bnj1177.2	$⊢ ψ \leftrightarrow (X \in B \land y \in B \land y R X)$
2		bnj1177.3	$⊢ C = trCl (X, A, R) \cap B$
3		bnj1177.9	$⊢ (φ \land ψ) \to R FrSe A$
4		bnj1177.13	$⊢ (φ \land ψ) \to B \subseteq A$
5		bnj1177.17	$⊢ (φ \land ψ) \to X \in A$
6		df-bnj15	$⊢ R FrSe A \leftrightarrow (R Fr A \land R Se A)$
7	6	simplbi	$⊢ R FrSe A \to R Fr A$
8	3 7	syl	$⊢ (φ \land ψ) \to R Fr A$
9		bnj1147	$⊢ trCl (X, A, R) \subseteq A$
10		ssinss1	$⊢ trCl (X, A, R) \subseteq A \to trCl (X, A, R) \cap B \subseteq A$
11	9 10	ax-mp	$⊢ trCl (X, A, R) \cap B \subseteq A$
12	2 11	eqsstri	$⊢ C \subseteq A$
13	12	a1i	$⊢ (φ \land ψ) \to C \subseteq A$
14		bnj906	$⊢ (R FrSe A \land X \in A) \to pred (X, A, R) \subseteq trCl (X, A, R)$
15	3 5 14	syl2anc	$⊢ (φ \land ψ) \to pred (X, A, R) \subseteq trCl (X, A, R)$
16	15	ssrind	$⊢ (φ \land ψ) \to pred (X, A, R) \cap B \subseteq trCl (X, A, R) \cap B$
17	1	simp2bi	$⊢ ψ \to y \in B$
18	17	adantl	$⊢ (φ \land ψ) \to y \in B$
19	4 18	sseldd	$⊢ (φ \land ψ) \to y \in A$
20	1	simp3bi	$⊢ ψ \to y R X$
21	20	adantl	$⊢ (φ \land ψ) \to y R X$
22		bnj1152	$⊢ y \in pred (X, A, R) \leftrightarrow (y \in A \land y R X)$
23	19 21 22	sylanbrc	$⊢ (φ \land ψ) \to y \in pred (X, A, R)$
24	23 18	elind	$⊢ (φ \land ψ) \to y \in (pred (X, A, R) \cap B)$
25	16 24	sseldd	$⊢ (φ \land ψ) \to y \in (trCl (X, A, R) \cap B)$
26	25	ne0d	$⊢ (φ \land ψ) \to trCl (X, A, R) \cap B \neq \emptyset$
27	2	neeq1i	$⊢ C \neq \emptyset \leftrightarrow trCl (X, A, R) \cap B \neq \emptyset$
28	26 27	sylibr	$⊢ (φ \land ψ) \to C \neq \emptyset$
29		bnj893	$⊢ (R FrSe A \land X \in A) \to trCl (X, A, R) \in V$
30	3 5 29	syl2anc	$⊢ (φ \land ψ) \to trCl (X, A, R) \in V$
31		inex1g	$⊢ trCl (X, A, R) \in V \to trCl (X, A, R) \cap B \in V$
32	2 31	eqeltrid	$⊢ trCl (X, A, R) \in V \to C \in V$
33	30 32	syl	$⊢ (φ \land ψ) \to C \in V$
34	8 13 28 33	bnj951	$⊢ (φ \land ψ) \to (R Fr A \land C \subseteq A \land C \neq \emptyset \land C \in V)$

Metamath Proof Explorer

Theorem bnj1177

Proof