bnj1408

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

Proof

Step	Hyp	Ref	Expression
1		bnj1408.1	$⊢ B = pred (X, A, R) \cup ⋃_{y \in pred (X, A, R)} trCl (y, A, R)$
2		bnj1408.2	$⊢ C = pred (X, A, R) \cup ⋃_{y \in trCl (X, A, R)} trCl (y, A, R)$
3		bnj1408.3	$⊢ θ \leftrightarrow (R FrSe A \land X \in A)$
4		bnj1408.4	$⊢ τ \leftrightarrow (B \in V \land TrFo (B, A, R) \land pred (X, A, R) \subseteq B)$
5	3	biimpri	$⊢ (R FrSe A \land X \in A) \to θ$
6	1	bnj1413	$⊢ (R FrSe A \land X \in A) \to B \in V$
7		simplll	$⊢ (((R FrSe A \land X \in A) \land z \in B) \land z \in pred (X, A, R)) \to R FrSe A$
8		bnj213	$⊢ pred (X, A, R) \subseteq A$
9	8	sseli	$⊢ z \in pred (X, A, R) \to z \in A$
10	9	adantl	$⊢ (((R FrSe A \land X \in A) \land z \in B) \land z \in pred (X, A, R)) \to z \in A$
11		bnj906	$⊢ (R FrSe A \land z \in A) \to pred (z, A, R) \subseteq trCl (z, A, R)$
12	7 10 11	syl2anc	$⊢ (((R FrSe A \land X \in A) \land z \in B) \land z \in pred (X, A, R)) \to pred (z, A, R) \subseteq trCl (z, A, R)$
13		bnj1318	$⊢ y = z \to trCl (y, A, R) = trCl (z, A, R)$
14	13	ssiun2s	$⊢ z \in pred (X, A, R) \to trCl (z, A, R) \subseteq ⋃_{y \in pred (X, A, R)} trCl (y, A, R)$
15		ssun4	$⊢ trCl (z, A, R) \subseteq ⋃_{y \in pred (X, A, R)} trCl (y, A, R) \to trCl (z, A, R) \subseteq pred (X, A, R) \cup ⋃_{y \in pred (X, A, R)} trCl (y, A, R)$
16	15 1	sseqtrrdi	$⊢ trCl (z, A, R) \subseteq ⋃_{y \in pred (X, A, R)} trCl (y, A, R) \to trCl (z, A, R) \subseteq B$
17	14 16	syl	$⊢ z \in pred (X, A, R) \to trCl (z, A, R) \subseteq B$
18	17	adantl	$⊢ (((R FrSe A \land X \in A) \land z \in B) \land z \in pred (X, A, R)) \to trCl (z, A, R) \subseteq B$
19	12 18	sstrd	$⊢ (((R FrSe A \land X \in A) \land z \in B) \land z \in pred (X, A, R)) \to pred (z, A, R) \subseteq B$
20		simpr	$⊢ (((R FrSe A \land X \in A) \land z \in B) \land z \in ⋃_{y \in pred (X, A, R)} trCl (y, A, R)) \to z \in ⋃_{y \in pred (X, A, R)} trCl (y, A, R)$
21	20	bnj1405	$⊢ (((R FrSe A \land X \in A) \land z \in B) \land z \in ⋃_{y \in pred (X, A, R)} trCl (y, A, R)) \to \exists y \in pred (X, A, R) z \in trCl (y, A, R)$
22		biid	$⊢ ((((R FrSe A \land X \in A) \land z \in B) \land z \in ⋃_{y \in pred (X, A, R)} trCl (y, A, R)) \land y \in pred (X, A, R) \land z \in trCl (y, A, R)) \leftrightarrow ((((R FrSe A \land X \in A) \land z \in B) \land z \in ⋃_{y \in pred (X, A, R)} trCl (y, A, R)) \land y \in pred (X, A, R) \land z \in trCl (y, A, R))$
23		nfv	$⊢ Ⅎ y (R FrSe A \land X \in A)$
24		nfcv	$⊢ \underline{Ⅎ} y pred (X, A, R)$
25		nfiu1	$⊢ \underline{Ⅎ} y ⋃_{y \in pred (X, A, R)} trCl (y, A, R)$
26	24 25	nfun	$⊢ \underline{Ⅎ} y (pred (X, A, R) \cup ⋃_{y \in pred (X, A, R)} trCl (y, A, R))$
27	1 26	nfcxfr	$⊢ \underline{Ⅎ} y B$
28	27	nfcri	$⊢ Ⅎ y z \in B$
29	23 28	nfan	$⊢ Ⅎ y ((R FrSe A \land X \in A) \land z \in B)$
30	25	nfcri	$⊢ Ⅎ y z \in ⋃_{y \in pred (X, A, R)} trCl (y, A, R)$
31	29 30	nfan	$⊢ Ⅎ y (((R FrSe A \land X \in A) \land z \in B) \land z \in ⋃_{y \in pred (X, A, R)} trCl (y, A, R))$
32	31	nf5ri	$⊢ (((R FrSe A \land X \in A) \land z \in B) \land z \in ⋃_{y \in pred (X, A, R)} trCl (y, A, R)) \to \forall y (((R FrSe A \land X \in A) \land z \in B) \land z \in ⋃_{y \in pred (X, A, R)} trCl (y, A, R))$
33	21 22 32	bnj1521	$⊢ (((R FrSe A \land X \in A) \land z \in B) \land z \in ⋃_{y \in pred (X, A, R)} trCl (y, A, R)) \to \exists y ((((R FrSe A \land X \in A) \land z \in B) \land z \in ⋃_{y \in pred (X, A, R)} trCl (y, A, R)) \land y \in pred (X, A, R) \land z \in trCl (y, A, R))$
34		simplll	$⊢ (((R FrSe A \land X \in A) \land z \in B) \land z \in ⋃_{y \in pred (X, A, R)} trCl (y, A, R)) \to R FrSe A$
35	34	3ad2ant1	$⊢ ((((R FrSe A \land X \in A) \land z \in B) \land z \in ⋃_{y \in pred (X, A, R)} trCl (y, A, R)) \land y \in pred (X, A, R) \land z \in trCl (y, A, R)) \to R FrSe A$
36		bnj1147	$⊢ trCl (y, A, R) \subseteq A$
37		simp3	$⊢ ((((R FrSe A \land X \in A) \land z \in B) \land z \in ⋃_{y \in pred (X, A, R)} trCl (y, A, R)) \land y \in pred (X, A, R) \land z \in trCl (y, A, R)) \to z \in trCl (y, A, R)$
38	36 37	bnj1213	$⊢ ((((R FrSe A \land X \in A) \land z \in B) \land z \in ⋃_{y \in pred (X, A, R)} trCl (y, A, R)) \land y \in pred (X, A, R) \land z \in trCl (y, A, R)) \to z \in A$
39	35 38 11	syl2anc	$⊢ ((((R FrSe A \land X \in A) \land z \in B) \land z \in ⋃_{y \in pred (X, A, R)} trCl (y, A, R)) \land y \in pred (X, A, R) \land z \in trCl (y, A, R)) \to pred (z, A, R) \subseteq trCl (z, A, R)$
40		simp2	$⊢ ((((R FrSe A \land X \in A) \land z \in B) \land z \in ⋃_{y \in pred (X, A, R)} trCl (y, A, R)) \land y \in pred (X, A, R) \land z \in trCl (y, A, R)) \to y \in pred (X, A, R)$
41	8 40	bnj1213	$⊢ ((((R FrSe A \land X \in A) \land z \in B) \land z \in ⋃_{y \in pred (X, A, R)} trCl (y, A, R)) \land y \in pred (X, A, R) \land z \in trCl (y, A, R)) \to y \in A$
42		bnj1125	$⊢ (R FrSe A \land y \in A \land z \in trCl (y, A, R)) \to trCl (z, A, R) \subseteq trCl (y, A, R)$
43	35 41 37 42	syl3anc	$⊢ ((((R FrSe A \land X \in A) \land z \in B) \land z \in ⋃_{y \in pred (X, A, R)} trCl (y, A, R)) \land y \in pred (X, A, R) \land z \in trCl (y, A, R)) \to trCl (z, A, R) \subseteq trCl (y, A, R)$
44	39 43	sstrd	$⊢ ((((R FrSe A \land X \in A) \land z \in B) \land z \in ⋃_{y \in pred (X, A, R)} trCl (y, A, R)) \land y \in pred (X, A, R) \land z \in trCl (y, A, R)) \to pred (z, A, R) \subseteq trCl (y, A, R)$
45		ssiun2	$⊢ y \in pred (X, A, R) \to trCl (y, A, R) \subseteq ⋃_{y \in pred (X, A, R)} trCl (y, A, R)$
46	45	3ad2ant2	$⊢ ((((R FrSe A \land X \in A) \land z \in B) \land z \in ⋃_{y \in pred (X, A, R)} trCl (y, A, R)) \land y \in pred (X, A, R) \land z \in trCl (y, A, R)) \to trCl (y, A, R) \subseteq ⋃_{y \in pred (X, A, R)} trCl (y, A, R)$
47		ssun4	$⊢ trCl (y, A, R) \subseteq ⋃_{y \in pred (X, A, R)} trCl (y, A, R) \to trCl (y, A, R) \subseteq pred (X, A, R) \cup ⋃_{y \in pred (X, A, R)} trCl (y, A, R)$
48	47 1	sseqtrrdi	$⊢ trCl (y, A, R) \subseteq ⋃_{y \in pred (X, A, R)} trCl (y, A, R) \to trCl (y, A, R) \subseteq B$
49	46 48	syl	$⊢ ((((R FrSe A \land X \in A) \land z \in B) \land z \in ⋃_{y \in pred (X, A, R)} trCl (y, A, R)) \land y \in pred (X, A, R) \land z \in trCl (y, A, R)) \to trCl (y, A, R) \subseteq B$
50	44 49	sstrd	$⊢ ((((R FrSe A \land X \in A) \land z \in B) \land z \in ⋃_{y \in pred (X, A, R)} trCl (y, A, R)) \land y \in pred (X, A, R) \land z \in trCl (y, A, R)) \to pred (z, A, R) \subseteq B$
51	33 50	bnj593	$⊢ (((R FrSe A \land X \in A) \land z \in B) \land z \in ⋃_{y \in pred (X, A, R)} trCl (y, A, R)) \to \exists y pred (z, A, R) \subseteq B$
52		nfcv	$⊢ \underline{Ⅎ} y pred (z, A, R)$
53	52 27	nfss	$⊢ Ⅎ y pred (z, A, R) \subseteq B$
54	53	nf5ri	$⊢ pred (z, A, R) \subseteq B \to \forall y pred (z, A, R) \subseteq B$
55	51 54	bnj1397	$⊢ (((R FrSe A \land X \in A) \land z \in B) \land z \in ⋃_{y \in pred (X, A, R)} trCl (y, A, R)) \to pred (z, A, R) \subseteq B$
56		simpr	$⊢ ((R FrSe A \land X \in A) \land z \in B) \to z \in B$
57	1	bnj1138	$⊢ z \in B \leftrightarrow (z \in pred (X, A, R) \lor z \in ⋃_{y \in pred (X, A, R)} trCl (y, A, R))$
58	56 57	sylib	$⊢ ((R FrSe A \land X \in A) \land z \in B) \to (z \in pred (X, A, R) \lor z \in ⋃_{y \in pred (X, A, R)} trCl (y, A, R))$
59	19 55 58	mpjaodan	$⊢ ((R FrSe A \land X \in A) \land z \in B) \to pred (z, A, R) \subseteq B$
60	59	ralrimiva	$⊢ (R FrSe A \land X \in A) \to \forall z \in B pred (z, A, R) \subseteq B$
61		df-bnj19	$⊢ TrFo (B, A, R) \leftrightarrow \forall z \in B pred (z, A, R) \subseteq B$
62	60 61	sylibr	$⊢ (R FrSe A \land X \in A) \to TrFo (B, A, R)$
63	1	bnj931	$⊢ pred (X, A, R) \subseteq B$
64	63	a1i	$⊢ (R FrSe A \land X \in A) \to pred (X, A, R) \subseteq B$
65	6 62 64 4	syl3anbrc	$⊢ (R FrSe A \land X \in A) \to τ$
66	3 4	bnj1124	$⊢ (θ \land τ) \to trCl (X, A, R) \subseteq B$
67	5 65 66	syl2anc	$⊢ (R FrSe A \land X \in A) \to trCl (X, A, R) \subseteq B$
68		bnj906	$⊢ (R FrSe A \land X \in A) \to pred (X, A, R) \subseteq trCl (X, A, R)$
69		iunss1	$⊢ pred (X, A, R) \subseteq trCl (X, A, R) \to ⋃_{y \in pred (X, A, R)} trCl (y, A, R) \subseteq ⋃_{y \in trCl (X, A, R)} trCl (y, A, R)$
70		unss2	$⊢ ⋃_{y \in pred (X, A, R)} trCl (y, A, R) \subseteq ⋃_{y \in trCl (X, A, R)} trCl (y, A, R) \to pred (X, A, R) \cup ⋃_{y \in pred (X, A, R)} trCl (y, A, R) \subseteq pred (X, A, R) \cup ⋃_{y \in trCl (X, A, R)} trCl (y, A, R)$
71	68 69 70	3syl	$⊢ (R FrSe A \land X \in A) \to pred (X, A, R) \cup ⋃_{y \in pred (X, A, R)} trCl (y, A, R) \subseteq pred (X, A, R) \cup ⋃_{y \in trCl (X, A, R)} trCl (y, A, R)$
72	71 1 2	3sstr4g	$⊢ (R FrSe A \land X \in A) \to B \subseteq C$
73		biid	$⊢ (R FrSe A \land X \in A) \leftrightarrow (R FrSe A \land X \in A)$
74		biid	$⊢ (C \in V \land TrFo (C, A, R) \land pred (X, A, R) \subseteq C) \leftrightarrow (C \in V \land TrFo (C, A, R) \land pred (X, A, R) \subseteq C)$
75	2 73 74	bnj1136	$⊢ (R FrSe A \land X \in A) \to trCl (X, A, R) = C$
76	72 75	sseqtrrd	$⊢ (R FrSe A \land X \in A) \to B \subseteq trCl (X, A, R)$
77	67 76	eqssd	$⊢ (R FrSe A \land X \in A) \to trCl (X, A, R) = B$

Metamath Proof Explorer

Theorem bnj1408

Proof