bnj1125

Description: Property of _trCl . (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

		Ref	Expression
	Assertion	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)$

Proof

Step	Hyp	Ref	Expression
1		simp1	$⊢ (R FrSe A \land X \in A \land Y \in trCl (X, A, R)) \to R FrSe A$
2		bnj1127	$⊢ Y \in trCl (X, A, R) \to Y \in A$
3	2	3ad2ant3	$⊢ (R FrSe A \land X \in A \land Y \in trCl (X, A, R)) \to Y \in A$
4		bnj893	$⊢ (R FrSe A \land X \in A) \to trCl (X, A, R) \in V$
5	4	3adant3	$⊢ (R FrSe A \land X \in A \land Y \in trCl (X, A, R)) \to trCl (X, A, R) \in V$
6		bnj1029	$⊢ (R FrSe A \land X \in A) \to TrFo (trCl (X, A, R), A, R)$
7	6	3adant3	$⊢ (R FrSe A \land X \in A \land Y \in trCl (X, A, R)) \to TrFo (trCl (X, A, R), A, R)$
8		simp3	$⊢ (R FrSe A \land X \in A \land Y \in trCl (X, A, R)) \to Y \in trCl (X, A, R)$
9		elisset	$⊢ Y \in trCl (X, A, R) \to \exists y y = Y$
10	9	3ad2ant3	$⊢ (R FrSe A \land X \in A \land Y \in trCl (X, A, R)) \to \exists y y = Y$
11		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)$
12		rsp	$⊢ \forall y \in trCl (X, A, R) pred (y, A, R) \subseteq trCl (X, A, R) \to (y \in trCl (X, A, R) \to pred (y, A, R) \subseteq trCl (X, A, R))$
13	11 12	sylbi	$⊢ TrFo (trCl (X, A, R), A, R) \to (y \in trCl (X, A, R) \to pred (y, A, R) \subseteq trCl (X, A, R))$
14	7 13	syl	$⊢ (R FrSe A \land X \in A \land Y \in trCl (X, A, R)) \to (y \in trCl (X, A, R) \to pred (y, A, R) \subseteq trCl (X, A, R))$
15		eleq1	$⊢ y = Y \to (y \in trCl (X, A, R) \leftrightarrow Y \in trCl (X, A, R))$
16		bnj602	$⊢ y = Y \to pred (y, A, R) = pred (Y, A, R)$
17	16	sseq1d	$⊢ y = Y \to (pred (y, A, R) \subseteq trCl (X, A, R) \leftrightarrow pred (Y, A, R) \subseteq trCl (X, A, R))$
18	15 17	imbi12d	$⊢ y = Y \to ((y \in trCl (X, A, R) \to pred (y, A, R) \subseteq trCl (X, A, R)) \leftrightarrow (Y \in trCl (X, A, R) \to pred (Y, A, R) \subseteq trCl (X, A, R)))$
19	14 18	imbitrid	$⊢ y = Y \to ((R FrSe A \land X \in A \land Y \in trCl (X, A, R)) \to (Y \in trCl (X, A, R) \to pred (Y, A, R) \subseteq trCl (X, A, R)))$
20	19	exlimiv	$⊢ \exists y y = Y \to ((R FrSe A \land X \in A \land Y \in trCl (X, A, R)) \to (Y \in trCl (X, A, R) \to pred (Y, A, R) \subseteq trCl (X, A, R)))$
21	10 20	mpcom	$⊢ (R FrSe A \land X \in A \land Y \in trCl (X, A, R)) \to (Y \in trCl (X, A, R) \to pred (Y, A, R) \subseteq trCl (X, A, R))$
22	8 21	mpd	$⊢ (R FrSe A \land X \in A \land Y \in trCl (X, A, R)) \to pred (Y, A, R) \subseteq trCl (X, A, R)$
23		biid	$⊢ (R FrSe A \land Y \in A) \leftrightarrow (R FrSe A \land Y \in A)$
24		biid	$⊢ (trCl (X, A, R) \in V \land TrFo (trCl (X, A, R), A, R) \land pred (Y, A, R) \subseteq trCl (X, A, R)) \leftrightarrow (trCl (X, A, R) \in V \land TrFo (trCl (X, A, R), A, R) \land pred (Y, A, R) \subseteq trCl (X, A, R))$
25	23 24	bnj1124	$⊢ ((R FrSe A \land Y \in A) \land (trCl (X, A, R) \in V \land TrFo (trCl (X, A, R), A, R) \land pred (Y, A, R) \subseteq trCl (X, A, R))) \to trCl (Y, A, R) \subseteq trCl (X, A, R)$
26	1 3 5 7 22 25	syl23anc	$⊢ (R FrSe A \land X \in A \land Y \in trCl (X, A, R)) \to trCl (Y, A, R) \subseteq trCl (X, A, R)$

Metamath Proof Explorer

Theorem bnj1125

Proof