bnj978

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	bnj978.1	$⊢ θ \leftrightarrow (R FrSe A \land X \in A \land y \in trCl (X, A, R) \land z \in pred (y, A, R))$
	bnj978.2	$⊢ θ \to z \in trCl (X, A, R)$
Assertion	bnj978	$⊢ (R FrSe A \land X \in A) \to TrFo (trCl (X, A, R), A, R)$

Proof

Step	Hyp	Ref	Expression
1		bnj978.1	$⊢ θ \leftrightarrow (R FrSe A \land X \in A \land y \in trCl (X, A, R) \land z \in pred (y, A, R))$
2		bnj978.2	$⊢ θ \to z \in trCl (X, A, R)$
3	1 2	sylbir	$⊢ (R FrSe A \land X \in A \land y \in trCl (X, A, R) \land z \in pred (y, A, R)) \to z \in trCl (X, A, R)$
4	3	gen2	$⊢ \forall y \forall z ((R FrSe A \land X \in A \land y \in trCl (X, A, R) \land z \in pred (y, A, R)) \to z \in trCl (X, A, R))$
5		bnj253	$⊢ (R FrSe A \land X \in A \land y \in trCl (X, A, R) \land z \in pred (y, A, R)) \leftrightarrow ((R FrSe A \land X \in A) \land y \in trCl (X, A, R) \land z \in pred (y, A, R))$
6	5	imbi1i	$⊢ ((R FrSe A \land X \in A \land y \in trCl (X, A, R) \land z \in pred (y, A, R)) \to z \in trCl (X, A, R)) \leftrightarrow (((R FrSe A \land X \in A) \land y \in trCl (X, A, R) \land z \in pred (y, A, R)) \to z \in trCl (X, A, R))$
7	6	2albii	$⊢ \forall y \forall z ((R FrSe A \land X \in A \land y \in trCl (X, A, R) \land z \in pred (y, A, R)) \to z \in trCl (X, A, R)) \leftrightarrow \forall y \forall z (((R FrSe A \land X \in A) \land y \in trCl (X, A, R) \land z \in pred (y, A, R)) \to z \in trCl (X, A, R))$
8		3impexp	$⊢ (((R FrSe A \land X \in A) \land y \in trCl (X, A, R) \land z \in pred (y, A, R)) \to z \in trCl (X, A, R)) \leftrightarrow ((R FrSe A \land X \in A) \to (y \in trCl (X, A, R) \to (z \in pred (y, A, R) \to z \in trCl (X, A, R))))$
9	8	2albii	$⊢ \forall y \forall z (((R FrSe A \land X \in A) \land y \in trCl (X, A, R) \land z \in pred (y, A, R)) \to z \in trCl (X, A, R)) \leftrightarrow \forall y \forall z ((R FrSe A \land X \in A) \to (y \in trCl (X, A, R) \to (z \in pred (y, A, R) \to z \in trCl (X, A, R))))$
10		19.21v	$⊢ \forall z ((R FrSe A \land X \in A) \to (y \in trCl (X, A, R) \to (z \in pred (y, A, R) \to z \in trCl (X, A, R)))) \leftrightarrow ((R FrSe A \land X \in A) \to \forall z (y \in trCl (X, A, R) \to (z \in pred (y, A, R) \to z \in trCl (X, A, R))))$
11		19.21v	$⊢ \forall z (y \in trCl (X, A, R) \to (z \in pred (y, A, R) \to z \in trCl (X, A, R))) \leftrightarrow (y \in trCl (X, A, R) \to \forall z (z \in pred (y, A, R) \to z \in trCl (X, A, R)))$
12	11	imbi2i	$⊢ ((R FrSe A \land X \in A) \to \forall z (y \in trCl (X, A, R) \to (z \in pred (y, A, R) \to z \in trCl (X, A, R)))) \leftrightarrow ((R FrSe A \land X \in A) \to (y \in trCl (X, A, R) \to \forall z (z \in pred (y, A, R) \to z \in trCl (X, A, R))))$
13	10 12	bitri	$⊢ \forall z ((R FrSe A \land X \in A) \to (y \in trCl (X, A, R) \to (z \in pred (y, A, R) \to z \in trCl (X, A, R)))) \leftrightarrow ((R FrSe A \land X \in A) \to (y \in trCl (X, A, R) \to \forall z (z \in pred (y, A, R) \to z \in trCl (X, A, R))))$
14	13	albii	$⊢ \forall y \forall z ((R FrSe A \land X \in A) \to (y \in trCl (X, A, R) \to (z \in pred (y, A, R) \to z \in trCl (X, A, R)))) \leftrightarrow \forall y ((R FrSe A \land X \in A) \to (y \in trCl (X, A, R) \to \forall z (z \in pred (y, A, R) \to z \in trCl (X, A, R))))$
15		19.21v	$⊢ \forall y ((R FrSe A \land X \in A) \to (y \in trCl (X, A, R) \to \forall z (z \in pred (y, A, R) \to z \in trCl (X, A, R)))) \leftrightarrow ((R FrSe A \land X \in A) \to \forall y (y \in trCl (X, A, R) \to \forall z (z \in pred (y, A, R) \to z \in trCl (X, A, R))))$
16		df-ral	$⊢ \forall y \in trCl (X, A, R) \forall z (z \in pred (y, A, R) \to z \in trCl (X, A, R)) \leftrightarrow \forall y (y \in trCl (X, A, R) \to \forall z (z \in pred (y, A, R) \to z \in trCl (X, A, R)))$
17	16	bicomi	$⊢ \forall y (y \in trCl (X, A, R) \to \forall z (z \in pred (y, A, R) \to z \in trCl (X, A, R))) \leftrightarrow \forall y \in trCl (X, A, R) \forall z (z \in pred (y, A, R) \to z \in trCl (X, A, R))$
18	17	imbi2i	$⊢ ((R FrSe A \land X \in A) \to \forall y (y \in trCl (X, A, R) \to \forall z (z \in pred (y, A, R) \to z \in trCl (X, A, R)))) \leftrightarrow ((R FrSe A \land X \in A) \to \forall y \in trCl (X, A, R) \forall z (z \in pred (y, A, R) \to z \in trCl (X, A, R)))$
19	14 15 18	3bitri	$⊢ \forall y \forall z ((R FrSe A \land X \in A) \to (y \in trCl (X, A, R) \to (z \in pred (y, A, R) \to z \in trCl (X, A, R)))) \leftrightarrow ((R FrSe A \land X \in A) \to \forall y \in trCl (X, A, R) \forall z (z \in pred (y, A, R) \to z \in trCl (X, A, R)))$
20	7 9 19	3bitri	$⊢ \forall y \forall z ((R FrSe A \land X \in A \land y \in trCl (X, A, R) \land z \in pred (y, A, R)) \to z \in trCl (X, A, R)) \leftrightarrow ((R FrSe A \land X \in A) \to \forall y \in trCl (X, A, R) \forall z (z \in pred (y, A, R) \to z \in trCl (X, A, R)))$
21	4 20	mpbi	$⊢ (R FrSe A \land X \in A) \to \forall y \in trCl (X, A, R) \forall z (z \in pred (y, A, R) \to z \in trCl (X, A, R))$
22		df-ss	$⊢ pred (y, A, R) \subseteq trCl (X, A, R) \leftrightarrow \forall z (z \in pred (y, A, R) \to z \in trCl (X, A, R))$
23	22	ralbii	$⊢ \forall y \in trCl (X, A, R) pred (y, A, R) \subseteq trCl (X, A, R) \leftrightarrow \forall y \in trCl (X, A, R) \forall z (z \in pred (y, A, R) \to z \in trCl (X, A, R))$
24	21 23	sylibr	$⊢ (R FrSe A \land X \in A) \to \forall y \in trCl (X, A, R) pred (y, A, R) \subseteq trCl (X, A, R)$
25		df-bnj19	$⊢ TrFo (trCl (X, A, R), A, R) \leftrightarrow \forall y \in trCl (X, A, R) pred (y, A, R) \subseteq trCl (X, A, R)$
26	24 25	sylibr	$⊢ (R FrSe A \land X \in A) \to TrFo (trCl (X, A, R), A, R)$

Metamath Proof Explorer

Theorem bnj978

Proof