unirnmap

Description: Given a subset of a set exponentiation, the base set can be restricted. (Contributed by Glauco Siliprandi, 3-Mar-2021)

	Ref	Expression
Hypotheses	unirnmap.a	$⊢ φ \to A \in V$
	unirnmap.x	$⊢ φ \to X \subseteq B^{A}$
Assertion	unirnmap	$⊢ φ \to X \subseteq {ran ⋃ X}^{A}$

Proof

Step	Hyp	Ref	Expression
1		unirnmap.a	$⊢ φ \to A \in V$
2		unirnmap.x	$⊢ φ \to X \subseteq B^{A}$
3	2	sselda	$⊢ (φ \land g \in X) \to g \in (B^{A})$
4		elmapfn	$⊢ g \in (B^{A}) \to g Fn A$
5	3 4	syl	$⊢ (φ \land g \in X) \to g Fn A$
6		simplr	$⊢ ((φ \land g \in X) \land x \in A) \to g \in X$
7		dffn3	$⊢ g Fn A \leftrightarrow g : A ⟶ ran g$
8	5 7	sylib	$⊢ (φ \land g \in X) \to g : A ⟶ ran g$
9	8	ffvelcdmda	$⊢ ((φ \land g \in X) \land x \in A) \to g (x) \in ran g$
10		rneq	$⊢ f = g \to ran f = ran g$
11	10	eleq2d	$⊢ f = g \to (g (x) \in ran f \leftrightarrow g (x) \in ran g)$
12	11	rspcev	$⊢ (g \in X \land g (x) \in ran g) \to \exists f \in X g (x) \in ran f$
13	6 9 12	syl2anc	$⊢ ((φ \land g \in X) \land x \in A) \to \exists f \in X g (x) \in ran f$
14		eliun	$⊢ g (x) \in ⋃_{f \in X} ran f \leftrightarrow \exists f \in X g (x) \in ran f$
15	13 14	sylibr	$⊢ ((φ \land g \in X) \land x \in A) \to g (x) \in ⋃_{f \in X} ran f$
16		rnuni	$⊢ ran ⋃ X = ⋃_{f \in X} ran f$
17	15 16	eleqtrrdi	$⊢ ((φ \land g \in X) \land x \in A) \to g (x) \in ran ⋃ X$
18	17	ralrimiva	$⊢ (φ \land g \in X) \to \forall x \in A g (x) \in ran ⋃ X$
19	5 18	jca	$⊢ (φ \land g \in X) \to (g Fn A \land \forall x \in A g (x) \in ran ⋃ X)$
20		ffnfv	$⊢ g : A ⟶ ran ⋃ X \leftrightarrow (g Fn A \land \forall x \in A g (x) \in ran ⋃ X)$
21	19 20	sylibr	$⊢ (φ \land g \in X) \to g : A ⟶ ran ⋃ X$
22		ovexd	$⊢ φ \to B^{A} \in V$
23	22 2	ssexd	$⊢ φ \to X \in V$
24	23	uniexd	$⊢ φ \to ⋃ X \in V$
25		rnexg	$⊢ ⋃ X \in V \to ran ⋃ X \in V$
26	24 25	syl	$⊢ φ \to ran ⋃ X \in V$
27	26 1	elmapd	$⊢ φ \to (g \in ({ran ⋃ X}^{A}) \leftrightarrow g : A ⟶ ran ⋃ X)$
28	27	adantr	$⊢ (φ \land g \in X) \to (g \in ({ran ⋃ X}^{A}) \leftrightarrow g : A ⟶ ran ⋃ X)$
29	21 28	mpbird	$⊢ (φ \land g \in X) \to g \in ({ran ⋃ X}^{A})$
30	29	ralrimiva	$⊢ φ \to \forall g \in X g \in ({ran ⋃ X}^{A})$
31		dfss3	$⊢ X \subseteq {ran ⋃ X}^{A} \leftrightarrow \forall g \in X g \in ({ran ⋃ X}^{A})$
32	30 31	sylibr	$⊢ φ \to X \subseteq {ran ⋃ X}^{A}$

Metamath Proof Explorer

Theorem unirnmap

Proof