dmrelrnrel

Description: A relation preserving function. (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	dmrelrnrel.x	$⊢ Ⅎ x φ$
	dmrelrnrel.y	$⊢ Ⅎ y φ$
	dmrelrnrel.i	$⊢ φ \to \forall x \in A \forall y \in A (x R y \to F (x) S F (y))$
	dmrelrnrel.b	$⊢ φ \to B \in A$
	dmrelrnrel.c	$⊢ φ \to C \in A$
	dmrelrnrel.r	$⊢ φ \to B R C$
Assertion	dmrelrnrel	$⊢ φ \to F (B) S F (C)$

Proof

Step	Hyp	Ref	Expression
1		dmrelrnrel.x	$⊢ Ⅎ x φ$
2		dmrelrnrel.y	$⊢ Ⅎ y φ$
3		dmrelrnrel.i	$⊢ φ \to \forall x \in A \forall y \in A (x R y \to F (x) S F (y))$
4		dmrelrnrel.b	$⊢ φ \to B \in A$
5		dmrelrnrel.c	$⊢ φ \to C \in A$
6		dmrelrnrel.r	$⊢ φ \to B R C$
7		id	$⊢ φ \to φ$
8	7 4 5	jca31	$⊢ φ \to ((φ \land B \in A) \land C \in A)$
9		nfv	$⊢ Ⅎ y B \in A$
10	2 9	nfan	$⊢ Ⅎ y (φ \land B \in A)$
11		nfv	$⊢ Ⅎ y C \in A$
12	10 11	nfan	$⊢ Ⅎ y ((φ \land B \in A) \land C \in A)$
13		nfv	$⊢ Ⅎ y (B R C \to F (B) S F (C))$
14	12 13	nfim	$⊢ Ⅎ y (((φ \land B \in A) \land C \in A) \to (B R C \to F (B) S F (C)))$
15	9 14	nfim	$⊢ Ⅎ y (B \in A \to (((φ \land B \in A) \land C \in A) \to (B R C \to F (B) S F (C))))$
16		eleq1	$⊢ y = C \to (y \in A \leftrightarrow C \in A)$
17	16	anbi2d	$⊢ y = C \to (((φ \land B \in A) \land y \in A) \leftrightarrow ((φ \land B \in A) \land C \in A))$
18		breq2	$⊢ y = C \to (B R y \leftrightarrow B R C)$
19		fveq2	$⊢ y = C \to F (y) = F (C)$
20	19	breq2d	$⊢ y = C \to (F (B) S F (y) \leftrightarrow F (B) S F (C))$
21	18 20	imbi12d	$⊢ y = C \to ((B R y \to F (B) S F (y)) \leftrightarrow (B R C \to F (B) S F (C)))$
22	17 21	imbi12d	$⊢ y = C \to ((((φ \land B \in A) \land y \in A) \to (B R y \to F (B) S F (y))) \leftrightarrow (((φ \land B \in A) \land C \in A) \to (B R C \to F (B) S F (C))))$
23	22	imbi2d	$⊢ y = C \to ((B \in A \to (((φ \land B \in A) \land y \in A) \to (B R y \to F (B) S F (y)))) \leftrightarrow (B \in A \to (((φ \land B \in A) \land C \in A) \to (B R C \to F (B) S F (C)))))$
24		nfv	$⊢ Ⅎ x B \in A$
25	1 24	nfan	$⊢ Ⅎ x (φ \land B \in A)$
26		nfv	$⊢ Ⅎ x y \in A$
27	25 26	nfan	$⊢ Ⅎ x ((φ \land B \in A) \land y \in A)$
28		nfv	$⊢ Ⅎ x (B R y \to F (B) S F (y))$
29	27 28	nfim	$⊢ Ⅎ x (((φ \land B \in A) \land y \in A) \to (B R y \to F (B) S F (y)))$
30		eleq1	$⊢ x = B \to (x \in A \leftrightarrow B \in A)$
31	30	anbi2d	$⊢ x = B \to ((φ \land x \in A) \leftrightarrow (φ \land B \in A))$
32	31	anbi1d	$⊢ x = B \to (((φ \land x \in A) \land y \in A) \leftrightarrow ((φ \land B \in A) \land y \in A))$
33		breq1	$⊢ x = B \to (x R y \leftrightarrow B R y)$
34		fveq2	$⊢ x = B \to F (x) = F (B)$
35	34	breq1d	$⊢ x = B \to (F (x) S F (y) \leftrightarrow F (B) S F (y))$
36	33 35	imbi12d	$⊢ x = B \to ((x R y \to F (x) S F (y)) \leftrightarrow (B R y \to F (B) S F (y)))$
37	32 36	imbi12d	$⊢ x = B \to ((((φ \land x \in A) \land y \in A) \to (x R y \to F (x) S F (y))) \leftrightarrow (((φ \land B \in A) \land y \in A) \to (B R y \to F (B) S F (y))))$
38	3	r19.21bi	$⊢ (φ \land x \in A) \to \forall y \in A (x R y \to F (x) S F (y))$
39	38	r19.21bi	$⊢ ((φ \land x \in A) \land y \in A) \to (x R y \to F (x) S F (y))$
40	29 37 39	vtoclg1f	$⊢ B \in A \to (((φ \land B \in A) \land y \in A) \to (B R y \to F (B) S F (y)))$
41	15 23 40	vtoclg1f	$⊢ C \in A \to (B \in A \to (((φ \land B \in A) \land C \in A) \to (B R C \to F (B) S F (C))))$
42	5 4 41	sylc	$⊢ φ \to (((φ \land B \in A) \land C \in A) \to (B R C \to F (B) S F (C)))$
43	8 6 42	mp2d	$⊢ φ \to F (B) S F (C)$

Metamath Proof Explorer

Theorem dmrelrnrel

Proof