ofrfval2

Description: The function relation acting on maps. (Contributed by Mario Carneiro, 20-Jul-2014)

	Ref	Expression
Hypotheses	offval2.1	$⊢ φ \to A \in V$
	offval2.2	$⊢ (φ \land x \in A) \to B \in W$
	offval2.3	$⊢ (φ \land x \in A) \to C \in X$
	offval2.4	$⊢ φ \to F = (x \in A ⟼ B)$
	offval2.5	$⊢ φ \to G = (x \in A ⟼ C)$
Assertion	ofrfval2	$⊢ φ \to (F R_{f} G \leftrightarrow \forall x \in A B R C)$

Proof

Step	Hyp	Ref	Expression
1		offval2.1	$⊢ φ \to A \in V$
2		offval2.2	$⊢ (φ \land x \in A) \to B \in W$
3		offval2.3	$⊢ (φ \land x \in A) \to C \in X$
4		offval2.4	$⊢ φ \to F = (x \in A ⟼ B)$
5		offval2.5	$⊢ φ \to G = (x \in A ⟼ C)$
6	2	ralrimiva	$⊢ φ \to \forall x \in A B \in W$
7		eqid	$⊢ (x \in A ⟼ B) = (x \in A ⟼ B)$
8	7	fnmpt	$⊢ \forall x \in A B \in W \to (x \in A ⟼ B) Fn A$
9	6 8	syl	$⊢ φ \to (x \in A ⟼ B) Fn A$
10	4	fneq1d	$⊢ φ \to (F Fn A \leftrightarrow (x \in A ⟼ B) Fn A)$
11	9 10	mpbird	$⊢ φ \to F Fn A$
12	3	ralrimiva	$⊢ φ \to \forall x \in A C \in X$
13		eqid	$⊢ (x \in A ⟼ C) = (x \in A ⟼ C)$
14	13	fnmpt	$⊢ \forall x \in A C \in X \to (x \in A ⟼ C) Fn A$
15	12 14	syl	$⊢ φ \to (x \in A ⟼ C) Fn A$
16	5	fneq1d	$⊢ φ \to (G Fn A \leftrightarrow (x \in A ⟼ C) Fn A)$
17	15 16	mpbird	$⊢ φ \to G Fn A$
18		inidm	$⊢ A \cap A = A$
19	4	adantr	$⊢ (φ \land y \in A) \to F = (x \in A ⟼ B)$
20	19	fveq1d	$⊢ (φ \land y \in A) \to F (y) = (x \in A ⟼ B) (y)$
21	5	adantr	$⊢ (φ \land y \in A) \to G = (x \in A ⟼ C)$
22	21	fveq1d	$⊢ (φ \land y \in A) \to G (y) = (x \in A ⟼ C) (y)$
23	11 17 1 1 18 20 22	ofrfval	$⊢ φ \to (F R_{f} G \leftrightarrow \forall y \in A (x \in A ⟼ B) (y) R (x \in A ⟼ C) (y))$
24		nffvmpt1	$⊢ \underline{Ⅎ} x (x \in A ⟼ B) (y)$
25		nfcv	$⊢ \underline{Ⅎ} x R$
26		nffvmpt1	$⊢ \underline{Ⅎ} x (x \in A ⟼ C) (y)$
27	24 25 26	nfbr	$⊢ Ⅎ x (x \in A ⟼ B) (y) R (x \in A ⟼ C) (y)$
28		nfv	$⊢ Ⅎ y (x \in A ⟼ B) (x) R (x \in A ⟼ C) (x)$
29		fveq2	$⊢ y = x \to (x \in A ⟼ B) (y) = (x \in A ⟼ B) (x)$
30		fveq2	$⊢ y = x \to (x \in A ⟼ C) (y) = (x \in A ⟼ C) (x)$
31	29 30	breq12d	$⊢ y = x \to ((x \in A ⟼ B) (y) R (x \in A ⟼ C) (y) \leftrightarrow (x \in A ⟼ B) (x) R (x \in A ⟼ C) (x))$
32	27 28 31	cbvralw	$⊢ \forall y \in A (x \in A ⟼ B) (y) R (x \in A ⟼ C) (y) \leftrightarrow \forall x \in A (x \in A ⟼ B) (x) R (x \in A ⟼ C) (x)$
33		simpr	$⊢ (φ \land x \in A) \to x \in A$
34	7	fvmpt2	$⊢ (x \in A \land B \in W) \to (x \in A ⟼ B) (x) = B$
35	33 2 34	syl2anc	$⊢ (φ \land x \in A) \to (x \in A ⟼ B) (x) = B$
36	13	fvmpt2	$⊢ (x \in A \land C \in X) \to (x \in A ⟼ C) (x) = C$
37	33 3 36	syl2anc	$⊢ (φ \land x \in A) \to (x \in A ⟼ C) (x) = C$
38	35 37	breq12d	$⊢ (φ \land x \in A) \to ((x \in A ⟼ B) (x) R (x \in A ⟼ C) (x) \leftrightarrow B R C)$
39	38	ralbidva	$⊢ φ \to (\forall x \in A (x \in A ⟼ B) (x) R (x \in A ⟼ C) (x) \leftrightarrow \forall x \in A B R C)$
40	32 39	bitrid	$⊢ φ \to (\forall y \in A (x \in A ⟼ B) (y) R (x \in A ⟼ C) (y) \leftrightarrow \forall x \in A B R C)$
41	23 40	bitrd	$⊢ φ \to (F R_{f} G \leftrightarrow \forall x \in A B R C)$

Metamath Proof Explorer

Theorem ofrfval2

Proof