bnj1136

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	bnj1136.1	$⊢ B = pred (X, A, R) \cup ⋃_{y \in trCl (X, A, R)} trCl (y, A, R)$
	bnj1136.2	$⊢ θ \leftrightarrow (R FrSe A \land X \in A)$
	bnj1136.3	$⊢ τ \leftrightarrow (B \in V \land TrFo (B, A, R) \land pred (X, A, R) \subseteq B)$
Assertion	bnj1136	$⊢ (R FrSe A \land X \in A) \to trCl (X, A, R) = B$

Proof

Step	Hyp	Ref	Expression
1		bnj1136.1	$⊢ B = pred (X, A, R) \cup ⋃_{y \in trCl (X, A, R)} trCl (y, A, R)$
2		bnj1136.2	$⊢ θ \leftrightarrow (R FrSe A \land X \in A)$
3		bnj1136.3	$⊢ τ \leftrightarrow (B \in V \land TrFo (B, A, R) \land pred (X, A, R) \subseteq B)$
4	2	biimpri	$⊢ (R FrSe A \land X \in A) \to θ$
5		bnj1148	$⊢ (R FrSe A \land X \in A) \to pred (X, A, R) \in V$
6		bnj893	$⊢ (R FrSe A \land X \in A) \to trCl (X, A, R) \in V$
7		simp1	$⊢ (R FrSe A \land X \in A \land y \in trCl (X, A, R)) \to R FrSe A$
8		bnj1127	$⊢ y \in trCl (X, A, R) \to y \in A$
9	8	3ad2ant3	$⊢ (R FrSe A \land X \in A \land y \in trCl (X, A, R)) \to y \in A$
10		bnj893	$⊢ (R FrSe A \land y \in A) \to trCl (y, A, R) \in V$
11	7 9 10	syl2anc	$⊢ (R FrSe A \land X \in A \land y \in trCl (X, A, R)) \to trCl (y, A, R) \in V$
12	11	3expia	$⊢ (R FrSe A \land X \in A) \to (y \in trCl (X, A, R) \to trCl (y, A, R) \in V)$
13	12	ralrimiv	$⊢ (R FrSe A \land X \in A) \to \forall y \in trCl (X, A, R) trCl (y, A, R) \in V$
14		iunexg	$⊢ (trCl (X, A, R) \in V \land \forall y \in trCl (X, A, R) trCl (y, A, R) \in V) \to ⋃_{y \in trCl (X, A, R)} trCl (y, A, R) \in V$
15	6 13 14	syl2anc	$⊢ (R FrSe A \land X \in A) \to ⋃_{y \in trCl (X, A, R)} trCl (y, A, R) \in V$
16	5 15	bnj1149	$⊢ (R FrSe A \land X \in A) \to pred (X, A, R) \cup ⋃_{y \in trCl (X, A, R)} trCl (y, A, R) \in V$
17	1 16	eqeltrid	$⊢ (R FrSe A \land X \in A) \to B \in V$
18	1	bnj1137	$⊢ (R FrSe A \land X \in A) \to TrFo (B, A, R)$
19	1	bnj931	$⊢ pred (X, A, R) \subseteq B$
20	19	a1i	$⊢ (R FrSe A \land X \in A) \to pred (X, A, R) \subseteq B$
21	17 18 20 3	syl3anbrc	$⊢ (R FrSe A \land X \in A) \to τ$
22	2 3	bnj1124	$⊢ (θ \land τ) \to trCl (X, A, R) \subseteq B$
23	4 21 22	syl2anc	$⊢ (R FrSe A \land X \in A) \to trCl (X, A, R) \subseteq B$
24		bnj906	$⊢ (R FrSe A \land X \in A) \to pred (X, A, R) \subseteq trCl (X, A, R)$
25		bnj1125	$⊢ (R FrSe A \land X \in A \land y \in trCl (X, A, R)) \to trCl (y, A, R) \subseteq trCl (X, A, R)$
26	25	3expia	$⊢ (R FrSe A \land X \in A) \to (y \in trCl (X, A, R) \to trCl (y, A, R) \subseteq trCl (X, A, R))$
27	26	ralrimiv	$⊢ (R FrSe A \land X \in A) \to \forall y \in trCl (X, A, R) trCl (y, A, R) \subseteq trCl (X, A, R)$
28		ss2iun	$⊢ \forall y \in trCl (X, A, R) trCl (y, A, R) \subseteq trCl (X, A, R) \to ⋃_{y \in trCl (X, A, R)} trCl (y, A, R) \subseteq ⋃_{y \in trCl (X, A, R)} trCl (X, A, R)$
29		bnj1143	$⊢ ⋃_{y \in trCl (X, A, R)} trCl (X, A, R) \subseteq trCl (X, A, R)$
30	28 29	sstrdi	$⊢ \forall y \in trCl (X, A, R) trCl (y, A, R) \subseteq trCl (X, A, R) \to ⋃_{y \in trCl (X, A, R)} trCl (y, A, R) \subseteq trCl (X, A, R)$
31	27 30	syl	$⊢ (R FrSe A \land X \in A) \to ⋃_{y \in trCl (X, A, R)} trCl (y, A, R) \subseteq trCl (X, A, R)$
32	24 31	unssd	$⊢ (R FrSe A \land X \in A) \to pred (X, A, R) \cup ⋃_{y \in trCl (X, A, R)} trCl (y, A, R) \subseteq trCl (X, A, R)$
33	1 32	eqsstrid	$⊢ (R FrSe A \land X \in A) \to B \subseteq trCl (X, A, R)$
34	23 33	eqssd	$⊢ (R FrSe A \land X \in A) \to trCl (X, A, R) = B$

Metamath Proof Explorer

Theorem bnj1136

Proof