bnj1190

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	bnj1190.1	$⊢ φ \leftrightarrow (R FrSe A \land B \subseteq A \land B \neq \emptyset)$
	bnj1190.2	$⊢ ψ \leftrightarrow (x \in B \land y \in B \land y R x)$
Assertion	bnj1190	$⊢ (φ \land ψ) \to \exists w \in B \forall z \in B \neg z R w$

Proof

Step	Hyp	Ref	Expression
1		bnj1190.1	$⊢ φ \leftrightarrow (R FrSe A \land B \subseteq A \land B \neq \emptyset)$
2		bnj1190.2	$⊢ ψ \leftrightarrow (x \in B \land y \in B \land y R x)$
3	1	simp2bi	$⊢ φ \to B \subseteq A$
4	3	adantr	$⊢ (φ \land ψ) \to B \subseteq A$
5		eqid	$⊢ trCl (x, A, R) \cap B = trCl (x, A, R) \cap B$
6	1	simp1bi	$⊢ φ \to R FrSe A$
7	6	adantr	$⊢ (φ \land ψ) \to R FrSe A$
8	2	simp1bi	$⊢ ψ \to x \in B$
9		ssel2	$⊢ (B \subseteq A \land x \in B) \to x \in A$
10	3 8 9	syl2an	$⊢ (φ \land ψ) \to x \in A$
11	2 5 7 4 10	bnj1177	$⊢ (φ \land ψ) \to (R Fr A \land trCl (x, A, R) \cap B \subseteq A \land trCl (x, A, R) \cap B \neq \emptyset \land trCl (x, A, R) \cap B \in V)$
12		bnj1154	$⊢ (R Fr A \land trCl (x, A, R) \cap B \subseteq A \land trCl (x, A, R) \cap B \neq \emptyset \land trCl (x, A, R) \cap B \in V) \to \exists u \in (trCl (x, A, R) \cap B) \forall v \in (trCl (x, A, R) \cap B) \neg v R u$
13	11 12	bnj1176	$⊢ \exists u \forall v ((φ \land ψ) \to (u \in (trCl (x, A, R) \cap B) \land (((R FrSe A \land x \in A \land u \in trCl (x, A, R)) \land (R FrSe A \land u \in A) \land v \in A) \to (v R u \to \neg v \in (trCl (x, A, R) \cap B)))))$
14		biid	$⊢ ((R FrSe A \land x \in A \land u \in trCl (x, A, R)) \land (R FrSe A \land u \in A) \land (v \in A \land v R u)) \leftrightarrow ((R FrSe A \land x \in A \land u \in trCl (x, A, R)) \land (R FrSe A \land u \in A) \land (v \in A \land v R u))$
15		biid	$⊢ ((R FrSe A \land x \in A \land u \in trCl (x, A, R)) \land (R FrSe A \land u \in A) \land v \in A) \leftrightarrow ((R FrSe A \land x \in A \land u \in trCl (x, A, R)) \land (R FrSe A \land u \in A) \land v \in A)$
16	5 14 15	bnj1175	$⊢ ((R FrSe A \land x \in A \land u \in trCl (x, A, R)) \land (R FrSe A \land u \in A) \land v \in A) \to (v R u \to v \in trCl (x, A, R))$
17	5 13 16	bnj1174	$⊢ \exists u \forall v ((φ \land ψ) \to ((φ \land ψ \land u \in (trCl (x, A, R) \cap B)) \land (((R FrSe A \land x \in A \land u \in trCl (x, A, R)) \land (R FrSe A \land u \in A) \land v \in A) \to (v R u \to \neg v \in B))))$
18	5 15 7 10	bnj1173	$⊢ (φ \land ψ \land u \in (trCl (x, A, R) \cap B)) \to (((R FrSe A \land x \in A \land u \in trCl (x, A, R)) \land (R FrSe A \land u \in A) \land v \in A) \leftrightarrow v \in A)$
19	5 17 18	bnj1172	$⊢ \exists u \forall v ((φ \land ψ) \to (u \in B \land (v \in A \to (v R u \to \neg v \in B))))$
20	4 19	bnj1171	$⊢ \exists u \forall v ((φ \land ψ) \to (u \in B \land (v \in B \to \neg v R u)))$
21	20	bnj1186	$⊢ (φ \land ψ) \to \exists u \in B \forall v \in B \neg v R u$
22	21	bnj1185	$⊢ (φ \land ψ) \to \exists x \in B \forall y \in B \neg y R x$
23	22	bnj1185	$⊢ (φ \land ψ) \to \exists w \in B \forall z \in B \neg z R w$

Metamath Proof Explorer

Theorem bnj1190

Proof