predtrss

Description: If R is transitive over A and Y R X , then Pred ( R , A , Y ) is a subclass of Pred ( R , A , X ) . (Contributed by Scott Fenton, 28-Oct-2024)

		Ref	Expression
	Assertion	predtrss	$⊢ ((R \cap (A \times A)) \circ (R \cap (A \times A)) \subseteq R \land Y \in Pred (R, A, X) \land X \in A) \to Pred (R, A, Y) \subseteq Pred (R, A, X)$

Proof

Step	Hyp	Ref	Expression
1		simpr	$⊢ (((R \cap (A \times A)) \circ (R \cap (A \times A)) \subseteq R \land Y \in Pred (R, A, X) \land X \in A) \land z \in A) \to z \in A$
2		predel	$⊢ Y \in Pred (R, A, X) \to Y \in A$
3	2	3ad2ant2	$⊢ ((R \cap (A \times A)) \circ (R \cap (A \times A)) \subseteq R \land Y \in Pred (R, A, X) \land X \in A) \to Y \in A$
4	3	adantr	$⊢ (((R \cap (A \times A)) \circ (R \cap (A \times A)) \subseteq R \land Y \in Pred (R, A, X) \land X \in A) \land z \in A) \to Y \in A$
5		brxp	$⊢ z (A \times A) Y \leftrightarrow (z \in A \land Y \in A)$
6	1 4 5	sylanbrc	$⊢ (((R \cap (A \times A)) \circ (R \cap (A \times A)) \subseteq R \land Y \in Pred (R, A, X) \land X \in A) \land z \in A) \to z (A \times A) Y$
7		brin	$⊢ z (R \cap (A \times A)) Y \leftrightarrow (z R Y \land z (A \times A) Y)$
8		elpredimg	$⊢ (X \in A \land Y \in Pred (R, A, X)) \to Y R X$
9	8	ancoms	$⊢ (Y \in Pred (R, A, X) \land X \in A) \to Y R X$
10	9	3adant1	$⊢ ((R \cap (A \times A)) \circ (R \cap (A \times A)) \subseteq R \land Y \in Pred (R, A, X) \land X \in A) \to Y R X$
11	10	adantr	$⊢ (((R \cap (A \times A)) \circ (R \cap (A \times A)) \subseteq R \land Y \in Pred (R, A, X) \land X \in A) \land z \in A) \to Y R X$
12		simpl3	$⊢ (((R \cap (A \times A)) \circ (R \cap (A \times A)) \subseteq R \land Y \in Pred (R, A, X) \land X \in A) \land z \in A) \to X \in A$
13		brxp	$⊢ Y (A \times A) X \leftrightarrow (Y \in A \land X \in A)$
14	4 12 13	sylanbrc	$⊢ (((R \cap (A \times A)) \circ (R \cap (A \times A)) \subseteq R \land Y \in Pred (R, A, X) \land X \in A) \land z \in A) \to Y (A \times A) X$
15		brin	$⊢ Y (R \cap (A \times A)) X \leftrightarrow (Y R X \land Y (A \times A) X)$
16	11 14 15	sylanbrc	$⊢ (((R \cap (A \times A)) \circ (R \cap (A \times A)) \subseteq R \land Y \in Pred (R, A, X) \land X \in A) \land z \in A) \to Y (R \cap (A \times A)) X$
17		breq2	$⊢ y = Y \to (z (R \cap (A \times A)) y \leftrightarrow z (R \cap (A \times A)) Y)$
18		breq1	$⊢ y = Y \to (y (R \cap (A \times A)) X \leftrightarrow Y (R \cap (A \times A)) X)$
19	17 18	anbi12d	$⊢ y = Y \to ((z (R \cap (A \times A)) y \land y (R \cap (A \times A)) X) \leftrightarrow (z (R \cap (A \times A)) Y \land Y (R \cap (A \times A)) X))$
20	19	spcegv	$⊢ Y \in Pred (R, A, X) \to ((z (R \cap (A \times A)) Y \land Y (R \cap (A \times A)) X) \to \exists y (z (R \cap (A \times A)) y \land y (R \cap (A \times A)) X))$
21	20	3ad2ant2	$⊢ ((R \cap (A \times A)) \circ (R \cap (A \times A)) \subseteq R \land Y \in Pred (R, A, X) \land X \in A) \to ((z (R \cap (A \times A)) Y \land Y (R \cap (A \times A)) X) \to \exists y (z (R \cap (A \times A)) y \land y (R \cap (A \times A)) X))$
22	21	adantr	$⊢ (((R \cap (A \times A)) \circ (R \cap (A \times A)) \subseteq R \land Y \in Pred (R, A, X) \land X \in A) \land z \in A) \to ((z (R \cap (A \times A)) Y \land Y (R \cap (A \times A)) X) \to \exists y (z (R \cap (A \times A)) y \land y (R \cap (A \times A)) X))$
23		vex	$⊢ z \in V$
24		brcog	$⊢ (z \in V \land X \in A) \to (z ((R \cap (A \times A)) \circ (R \cap (A \times A))) X \leftrightarrow \exists y (z (R \cap (A \times A)) y \land y (R \cap (A \times A)) X))$
25	23 12 24	sylancr	$⊢ (((R \cap (A \times A)) \circ (R \cap (A \times A)) \subseteq R \land Y \in Pred (R, A, X) \land X \in A) \land z \in A) \to (z ((R \cap (A \times A)) \circ (R \cap (A \times A))) X \leftrightarrow \exists y (z (R \cap (A \times A)) y \land y (R \cap (A \times A)) X))$
26	22 25	sylibrd	$⊢ (((R \cap (A \times A)) \circ (R \cap (A \times A)) \subseteq R \land Y \in Pred (R, A, X) \land X \in A) \land z \in A) \to ((z (R \cap (A \times A)) Y \land Y (R \cap (A \times A)) X) \to z ((R \cap (A \times A)) \circ (R \cap (A \times A))) X)$
27		simpl1	$⊢ (((R \cap (A \times A)) \circ (R \cap (A \times A)) \subseteq R \land Y \in Pred (R, A, X) \land X \in A) \land z \in A) \to (R \cap (A \times A)) \circ (R \cap (A \times A)) \subseteq R$
28	27	ssbrd	$⊢ (((R \cap (A \times A)) \circ (R \cap (A \times A)) \subseteq R \land Y \in Pred (R, A, X) \land X \in A) \land z \in A) \to (z ((R \cap (A \times A)) \circ (R \cap (A \times A))) X \to z R X)$
29	26 28	syld	$⊢ (((R \cap (A \times A)) \circ (R \cap (A \times A)) \subseteq R \land Y \in Pred (R, A, X) \land X \in A) \land z \in A) \to ((z (R \cap (A \times A)) Y \land Y (R \cap (A \times A)) X) \to z R X)$
30	16 29	mpan2d	$⊢ (((R \cap (A \times A)) \circ (R \cap (A \times A)) \subseteq R \land Y \in Pred (R, A, X) \land X \in A) \land z \in A) \to (z (R \cap (A \times A)) Y \to z R X)$
31	7 30	biimtrrid	$⊢ (((R \cap (A \times A)) \circ (R \cap (A \times A)) \subseteq R \land Y \in Pred (R, A, X) \land X \in A) \land z \in A) \to ((z R Y \land z (A \times A) Y) \to z R X)$
32	6 31	mpan2d	$⊢ (((R \cap (A \times A)) \circ (R \cap (A \times A)) \subseteq R \land Y \in Pred (R, A, X) \land X \in A) \land z \in A) \to (z R Y \to z R X)$
33	32	imdistanda	$⊢ ((R \cap (A \times A)) \circ (R \cap (A \times A)) \subseteq R \land Y \in Pred (R, A, X) \land X \in A) \to ((z \in A \land z R Y) \to (z \in A \land z R X))$
34	23	elpred	$⊢ Y \in Pred (R, A, X) \to (z \in Pred (R, A, Y) \leftrightarrow (z \in A \land z R Y))$
35	34	3ad2ant2	$⊢ ((R \cap (A \times A)) \circ (R \cap (A \times A)) \subseteq R \land Y \in Pred (R, A, X) \land X \in A) \to (z \in Pred (R, A, Y) \leftrightarrow (z \in A \land z R Y))$
36	23	elpred	$⊢ X \in A \to (z \in Pred (R, A, X) \leftrightarrow (z \in A \land z R X))$
37	36	3ad2ant3	$⊢ ((R \cap (A \times A)) \circ (R \cap (A \times A)) \subseteq R \land Y \in Pred (R, A, X) \land X \in A) \to (z \in Pred (R, A, X) \leftrightarrow (z \in A \land z R X))$
38	33 35 37	3imtr4d	$⊢ ((R \cap (A \times A)) \circ (R \cap (A \times A)) \subseteq R \land Y \in Pred (R, A, X) \land X \in A) \to (z \in Pred (R, A, Y) \to z \in Pred (R, A, X))$
39	38	ssrdv	$⊢ ((R \cap (A \times A)) \circ (R \cap (A \times A)) \subseteq R \land Y \in Pred (R, A, X) \land X \in A) \to Pred (R, A, Y) \subseteq Pred (R, A, X)$

Metamath Proof Explorer

Theorem predtrss

Proof