bnj1137

Description: Property of _trCl . (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (Proof shortened by Mario Carneiro, 22-Dec-2016) (New usage is discouraged.)

		Ref	Expression
	Hypothesis	bnj1137.1	$⊢ B = pred (X, A, R) \cup ⋃_{y \in trCl (X, A, R)} trCl (y, A, R)$
	Assertion	bnj1137	$⊢ (R FrSe A \land X \in A) \to TrFo (B, A, R)$

Proof

Step	Hyp	Ref	Expression
1		bnj1137.1	$⊢ B = pred (X, A, R) \cup ⋃_{y \in trCl (X, A, R)} trCl (y, A, R)$
2	1	eleq2i	$⊢ v \in B \leftrightarrow v \in (pred (X, A, R) \cup ⋃_{y \in trCl (X, A, R)} trCl (y, A, R))$
3		elun	$⊢ v \in (pred (X, A, R) \cup ⋃_{y \in trCl (X, A, R)} trCl (y, A, R)) \leftrightarrow (v \in pred (X, A, R) \lor v \in ⋃_{y \in trCl (X, A, R)} trCl (y, A, R))$
4	2 3	bitri	$⊢ v \in B \leftrightarrow (v \in pred (X, A, R) \lor v \in ⋃_{y \in trCl (X, A, R)} trCl (y, A, R))$
5		bnj213	$⊢ pred (X, A, R) \subseteq A$
6	5	sseli	$⊢ v \in pred (X, A, R) \to v \in A$
7		bnj906	$⊢ (R FrSe A \land v \in A) \to pred (v, A, R) \subseteq trCl (v, A, R)$
8	7	adantlr	$⊢ ((R FrSe A \land X \in A) \land v \in A) \to pred (v, A, R) \subseteq trCl (v, A, R)$
9	6 8	sylan2	$⊢ ((R FrSe A \land X \in A) \land v \in pred (X, A, R)) \to pred (v, A, R) \subseteq trCl (v, A, R)$
10		bnj906	$⊢ (R FrSe A \land X \in A) \to pred (X, A, R) \subseteq trCl (X, A, R)$
11	10	sselda	$⊢ ((R FrSe A \land X \in A) \land v \in pred (X, A, R)) \to v \in trCl (X, A, R)$
12		bnj18eq1	$⊢ y = v \to trCl (y, A, R) = trCl (v, A, R)$
13	12	ssiun2s	$⊢ v \in trCl (X, A, R) \to trCl (v, A, R) \subseteq ⋃_{y \in trCl (X, A, R)} trCl (y, A, R)$
14	11 13	syl	$⊢ ((R FrSe A \land X \in A) \land v \in pred (X, A, R)) \to trCl (v, A, R) \subseteq ⋃_{y \in trCl (X, A, R)} trCl (y, A, R)$
15	9 14	sstrd	$⊢ ((R FrSe A \land X \in A) \land v \in pred (X, A, R)) \to pred (v, A, R) \subseteq ⋃_{y \in trCl (X, A, R)} trCl (y, A, R)$
16		bnj1147	$⊢ trCl (y, A, R) \subseteq A$
17	16	rgenw	$⊢ \forall y \in trCl (X, A, R) trCl (y, A, R) \subseteq A$
18		iunss	$⊢ ⋃_{y \in trCl (X, A, R)} trCl (y, A, R) \subseteq A \leftrightarrow \forall y \in trCl (X, A, R) trCl (y, A, R) \subseteq A$
19	17 18	mpbir	$⊢ ⋃_{y \in trCl (X, A, R)} trCl (y, A, R) \subseteq A$
20	19	sseli	$⊢ v \in ⋃_{y \in trCl (X, A, R)} trCl (y, A, R) \to v \in A$
21	20 8	sylan2	$⊢ ((R FrSe A \land X \in A) \land v \in ⋃_{y \in trCl (X, A, R)} trCl (y, A, R)) \to pred (v, A, R) \subseteq trCl (v, A, R)$
22		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)$
23	22	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))$
24	23	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)$
25		iunss	$⊢ ⋃_{y \in trCl (X, A, R)} trCl (y, A, R) \subseteq trCl (X, A, R) \leftrightarrow \forall y \in trCl (X, A, R) trCl (y, A, R) \subseteq trCl (X, A, R)$
26	24 25	sylibr	$⊢ (R FrSe A \land X \in A) \to ⋃_{y \in trCl (X, A, R)} trCl (y, A, R) \subseteq trCl (X, A, R)$
27	26	sselda	$⊢ ((R FrSe A \land X \in A) \land v \in ⋃_{y \in trCl (X, A, R)} trCl (y, A, R)) \to v \in trCl (X, A, R)$
28	27 13	syl	$⊢ ((R FrSe A \land X \in A) \land v \in ⋃_{y \in trCl (X, A, R)} trCl (y, A, R)) \to trCl (v, A, R) \subseteq ⋃_{y \in trCl (X, A, R)} trCl (y, A, R)$
29	21 28	sstrd	$⊢ ((R FrSe A \land X \in A) \land v \in ⋃_{y \in trCl (X, A, R)} trCl (y, A, R)) \to pred (v, A, R) \subseteq ⋃_{y \in trCl (X, A, R)} trCl (y, A, R)$
30	15 29	jaodan	$⊢ ((R FrSe A \land X \in A) \land (v \in pred (X, A, R) \lor v \in ⋃_{y \in trCl (X, A, R)} trCl (y, A, R))) \to pred (v, A, R) \subseteq ⋃_{y \in trCl (X, A, R)} trCl (y, A, R)$
31		ssun2	$⊢ ⋃_{y \in trCl (X, A, R)} trCl (y, A, R) \subseteq pred (X, A, R) \cup ⋃_{y \in trCl (X, A, R)} trCl (y, A, R)$
32	31 1	sseqtrri	$⊢ ⋃_{y \in trCl (X, A, R)} trCl (y, A, R) \subseteq B$
33	30 32	sstrdi	$⊢ ((R FrSe A \land X \in A) \land (v \in pred (X, A, R) \lor v \in ⋃_{y \in trCl (X, A, R)} trCl (y, A, R))) \to pred (v, A, R) \subseteq B$
34	4 33	sylan2b	$⊢ ((R FrSe A \land X \in A) \land v \in B) \to pred (v, A, R) \subseteq B$
35	34	ralrimiva	$⊢ (R FrSe A \land X \in A) \to \forall v \in B pred (v, A, R) \subseteq B$
36		df-bnj19	$⊢ TrFo (B, A, R) \leftrightarrow \forall v \in B pred (v, A, R) \subseteq B$
37	35 36	sylibr	$⊢ (R FrSe A \land X \in A) \to TrFo (B, A, R)$

Metamath Proof Explorer

Theorem bnj1137

Proof