preddowncl

Description: A property of classes that are downward closed under predecessor. (Contributed by Scott Fenton, 13-Apr-2011)

		Ref	Expression
	Assertion	preddowncl	$⊢ (B \subseteq A \land \forall x \in B Pred (R, A, x) \subseteq B) \to (X \in B \to Pred (R, B, X) = Pred (R, A, X))$

Proof

Step	Hyp	Ref	Expression
1		eleq1	$⊢ y = X \to (y \in B \leftrightarrow X \in B)$
2		predeq3	$⊢ y = X \to Pred (R, B, y) = Pred (R, B, X)$
3		predeq3	$⊢ y = X \to Pred (R, A, y) = Pred (R, A, X)$
4	2 3	eqeq12d	$⊢ y = X \to (Pred (R, B, y) = Pred (R, A, y) \leftrightarrow Pred (R, B, X) = Pred (R, A, X))$
5	1 4	imbi12d	$⊢ y = X \to ((y \in B \to Pred (R, B, y) = Pred (R, A, y)) \leftrightarrow (X \in B \to Pred (R, B, X) = Pred (R, A, X)))$
6	5	imbi2d	$⊢ y = X \to (((B \subseteq A \land \forall x \in B Pred (R, A, x) \subseteq B) \to (y \in B \to Pred (R, B, y) = Pred (R, A, y))) \leftrightarrow ((B \subseteq A \land \forall x \in B Pred (R, A, x) \subseteq B) \to (X \in B \to Pred (R, B, X) = Pred (R, A, X))))$
7		predpredss	$⊢ B \subseteq A \to Pred (R, B, y) \subseteq Pred (R, A, y)$
8	7	ad2antrr	$⊢ ((B \subseteq A \land \forall x \in B Pred (R, A, x) \subseteq B) \land y \in B) \to Pred (R, B, y) \subseteq Pred (R, A, y)$
9		predeq3	$⊢ x = y \to Pred (R, A, x) = Pred (R, A, y)$
10	9	sseq1d	$⊢ x = y \to (Pred (R, A, x) \subseteq B \leftrightarrow Pred (R, A, y) \subseteq B)$
11	10	rspccva	$⊢ (\forall x \in B Pred (R, A, x) \subseteq B \land y \in B) \to Pred (R, A, y) \subseteq B$
12	11	sseld	$⊢ (\forall x \in B Pred (R, A, x) \subseteq B \land y \in B) \to (z \in Pred (R, A, y) \to z \in B)$
13		vex	$⊢ y \in V$
14	13	elpredim	$⊢ z \in Pred (R, A, y) \to z R y$
15	12 14	jca2	$⊢ (\forall x \in B Pred (R, A, x) \subseteq B \land y \in B) \to (z \in Pred (R, A, y) \to (z \in B \land z R y))$
16		vex	$⊢ z \in V$
17	16	elpred	$⊢ y \in B \to (z \in Pred (R, B, y) \leftrightarrow (z \in B \land z R y))$
18	17	imbi2d	$⊢ y \in B \to ((z \in Pred (R, A, y) \to z \in Pred (R, B, y)) \leftrightarrow (z \in Pred (R, A, y) \to (z \in B \land z R y)))$
19	18	adantl	$⊢ (\forall x \in B Pred (R, A, x) \subseteq B \land y \in B) \to ((z \in Pred (R, A, y) \to z \in Pred (R, B, y)) \leftrightarrow (z \in Pred (R, A, y) \to (z \in B \land z R y)))$
20	15 19	mpbird	$⊢ (\forall x \in B Pred (R, A, x) \subseteq B \land y \in B) \to (z \in Pred (R, A, y) \to z \in Pred (R, B, y))$
21	20	ssrdv	$⊢ (\forall x \in B Pred (R, A, x) \subseteq B \land y \in B) \to Pred (R, A, y) \subseteq Pred (R, B, y)$
22	21	adantll	$⊢ ((B \subseteq A \land \forall x \in B Pred (R, A, x) \subseteq B) \land y \in B) \to Pred (R, A, y) \subseteq Pred (R, B, y)$
23	8 22	eqssd	$⊢ ((B \subseteq A \land \forall x \in B Pred (R, A, x) \subseteq B) \land y \in B) \to Pred (R, B, y) = Pred (R, A, y)$
24	23	ex	$⊢ (B \subseteq A \land \forall x \in B Pred (R, A, x) \subseteq B) \to (y \in B \to Pred (R, B, y) = Pred (R, A, y))$
25	6 24	vtoclg	$⊢ X \in B \to ((B \subseteq A \land \forall x \in B Pred (R, A, x) \subseteq B) \to (X \in B \to Pred (R, B, X) = Pred (R, A, X)))$
26	25	pm2.43b	$⊢ (B \subseteq A \land \forall x \in B Pred (R, A, x) \subseteq B) \to (X \in B \to Pred (R, B, X) = Pred (R, A, X))$

Metamath Proof Explorer

Theorem preddowncl

Proof