fvmptrabdm

Description: Value of a function mapping a set to a class abstraction restricting the value of another function. See also fvmptrabfv . (Suggested by BJ, 18-Feb-2022.) (Contributed by AV, 18-Feb-2022)

	Ref	Expression
Hypotheses	fvmptrabdm.f	$⊢ F = (x \in V ⟼ \{y \in G (Y) \| φ\})$
	fvmptrabdm.r	$⊢ x = X \to (φ \leftrightarrow ψ)$
	fvmptrabdm.v	$⊢ Y \in dom G \to X \in dom F$
Assertion	fvmptrabdm	$⊢ F (X) = \{y \in G (Y) \| ψ\}$

Proof

Step	Hyp	Ref	Expression
1		fvmptrabdm.f	$⊢ F = (x \in V ⟼ \{y \in G (Y) \| φ\})$
2		fvmptrabdm.r	$⊢ x = X \to (φ \leftrightarrow ψ)$
3		fvmptrabdm.v	$⊢ Y \in dom G \to X \in dom F$
4		pm2.1	$⊢ (\neg X \in dom F \lor X \in dom F)$
5		imor	$⊢ (Y \in dom G \to X \in dom F) \leftrightarrow (\neg Y \in dom G \lor X \in dom F)$
6		ordir	$⊢ ((\neg X \in dom F \land \neg Y \in dom G) \lor X \in dom F) \leftrightarrow ((\neg X \in dom F \lor X \in dom F) \land (\neg Y \in dom G \lor X \in dom F))$
7		ndmfv	$⊢ \neg X \in dom F \to F (X) = \emptyset$
8		ndmfv	$⊢ \neg Y \in dom G \to G (Y) = \emptyset$
9	8	rabeqdv	$⊢ \neg Y \in dom G \to \{y \in G (Y) \| ψ\} = \{y \in \emptyset \| ψ\}$
10		rab0	$⊢ \{y \in \emptyset \| ψ\} = \emptyset$
11	9 10	eqtr2di	$⊢ \neg Y \in dom G \to \emptyset = \{y \in G (Y) \| ψ\}$
12	7 11	sylan9eq	$⊢ (\neg X \in dom F \land \neg Y \in dom G) \to F (X) = \{y \in G (Y) \| ψ\}$
13	2	rabbidv	$⊢ x = X \to \{y \in G (Y) \| φ\} = \{y \in G (Y) \| ψ\}$
14	1	dmmpt	$⊢ dom F = \{x \in V \| \{y \in G (Y) \| φ\} \in V\}$
15		rabid2	$⊢ V = \{x \in V \| \{y \in G (Y) \| φ\} \in V\} \leftrightarrow \forall x \in V \{y \in G (Y) \| φ\} \in V$
16		fvex	$⊢ G (Y) \in V$
17	16	rabex	$⊢ \{y \in G (Y) \| φ\} \in V$
18	17	a1i	$⊢ x \in V \to \{y \in G (Y) \| φ\} \in V$
19	15 18	mprgbir	$⊢ V = \{x \in V \| \{y \in G (Y) \| φ\} \in V\}$
20	14 19	eqtr4i	$⊢ dom F = V$
21	20	eleq2i	$⊢ X \in dom F \leftrightarrow X \in V$
22	21	biimpi	$⊢ X \in dom F \to X \in V$
23	16	rabex	$⊢ \{y \in G (Y) \| ψ\} \in V$
24	23	a1i	$⊢ X \in dom F \to \{y \in G (Y) \| ψ\} \in V$
25	1 13 22 24	fvmptd3	$⊢ X \in dom F \to F (X) = \{y \in G (Y) \| ψ\}$
26	12 25	jaoi	$⊢ ((\neg X \in dom F \land \neg Y \in dom G) \lor X \in dom F) \to F (X) = \{y \in G (Y) \| ψ\}$
27	6 26	sylbir	$⊢ ((\neg X \in dom F \lor X \in dom F) \land (\neg Y \in dom G \lor X \in dom F)) \to F (X) = \{y \in G (Y) \| ψ\}$
28	27	expcom	$⊢ (\neg Y \in dom G \lor X \in dom F) \to ((\neg X \in dom F \lor X \in dom F) \to F (X) = \{y \in G (Y) \| ψ\})$
29	5 28	sylbi	$⊢ (Y \in dom G \to X \in dom F) \to ((\neg X \in dom F \lor X \in dom F) \to F (X) = \{y \in G (Y) \| ψ\})$
30	3 4 29	mp2	$⊢ F (X) = \{y \in G (Y) \| ψ\}$

Metamath Proof Explorer

Theorem fvmptrabdm

Proof