Theorem 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	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	unirnmap.x	⊢ ( 𝜑 → 𝑋 ⊆ ( 𝐵 ↑m 𝐴 ) )
Assertion	unirnmap	⊢ ( 𝜑 → 𝑋 ⊆ ( ran ∪ 𝑋 ↑m 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		unirnmap.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2		unirnmap.x	⊢ ( 𝜑 → 𝑋 ⊆ ( 𝐵 ↑m 𝐴 ) )
3	2	sselda	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑋 ) → 𝑔 ∈ ( 𝐵 ↑m 𝐴 ) )
4		elmapfn	⊢ ( 𝑔 ∈ ( 𝐵 ↑m 𝐴 ) → 𝑔 Fn 𝐴 )
5	3 4	syl	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑋 ) → 𝑔 Fn 𝐴 )
6		simplr	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑋 ) ∧ 𝑥 ∈ 𝐴 ) → 𝑔 ∈ 𝑋 )
7		dffn3	⊢ ( 𝑔 Fn 𝐴 ↔ 𝑔 : 𝐴 ⟶ ran 𝑔 )
8	5 7	sylib	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑋 ) → 𝑔 : 𝐴 ⟶ ran 𝑔 )
9	8	ffvelrnda	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑋 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑔 ‘ 𝑥 ) ∈ ran 𝑔 )
10		rneq	⊢ ( 𝑓 = 𝑔 → ran 𝑓 = ran 𝑔 )
11	10	eleq2d	⊢ ( 𝑓 = 𝑔 → ( ( 𝑔 ‘ 𝑥 ) ∈ ran 𝑓 ↔ ( 𝑔 ‘ 𝑥 ) ∈ ran 𝑔 ) )
12	11	rspcev	⊢ ( ( 𝑔 ∈ 𝑋 ∧ ( 𝑔 ‘ 𝑥 ) ∈ ran 𝑔 ) → ∃ 𝑓 ∈ 𝑋 ( 𝑔 ‘ 𝑥 ) ∈ ran 𝑓 )
13	6 9 12	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑋 ) ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑓 ∈ 𝑋 ( 𝑔 ‘ 𝑥 ) ∈ ran 𝑓 )
14		eliun	⊢ ( ( 𝑔 ‘ 𝑥 ) ∈ ∪ 𝑓 ∈ 𝑋 ran 𝑓 ↔ ∃ 𝑓 ∈ 𝑋 ( 𝑔 ‘ 𝑥 ) ∈ ran 𝑓 )
15	13 14	sylibr	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑋 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑔 ‘ 𝑥 ) ∈ ∪ 𝑓 ∈ 𝑋 ran 𝑓 )
16		rnuni	⊢ ran ∪ 𝑋 = ∪ 𝑓 ∈ 𝑋 ran 𝑓
17	15 16	eleqtrrdi	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑋 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑔 ‘ 𝑥 ) ∈ ran ∪ 𝑋 )
18	17	ralrimiva	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑋 ) → ∀ 𝑥 ∈ 𝐴 ( 𝑔 ‘ 𝑥 ) ∈ ran ∪ 𝑋 )
19	5 18	jca	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑋 ) → ( 𝑔 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑔 ‘ 𝑥 ) ∈ ran ∪ 𝑋 ) )
20		ffnfv	⊢ ( 𝑔 : 𝐴 ⟶ ran ∪ 𝑋 ↔ ( 𝑔 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑔 ‘ 𝑥 ) ∈ ran ∪ 𝑋 ) )
21	19 20	sylibr	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑋 ) → 𝑔 : 𝐴 ⟶ ran ∪ 𝑋 )
22		ovexd	⊢ ( 𝜑 → ( 𝐵 ↑m 𝐴 ) ∈ V )
23	22 2	ssexd	⊢ ( 𝜑 → 𝑋 ∈ V )
24	23	uniexd	⊢ ( 𝜑 → ∪ 𝑋 ∈ V )
25		rnexg	⊢ ( ∪ 𝑋 ∈ V → ran ∪ 𝑋 ∈ V )
26	24 25	syl	⊢ ( 𝜑 → ran ∪ 𝑋 ∈ V )
27	26 1	elmapd	⊢ ( 𝜑 → ( 𝑔 ∈ ( ran ∪ 𝑋 ↑m 𝐴 ) ↔ 𝑔 : 𝐴 ⟶ ran ∪ 𝑋 ) )
28	27	adantr	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑋 ) → ( 𝑔 ∈ ( ran ∪ 𝑋 ↑m 𝐴 ) ↔ 𝑔 : 𝐴 ⟶ ran ∪ 𝑋 ) )
29	21 28	mpbird	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑋 ) → 𝑔 ∈ ( ran ∪ 𝑋 ↑m 𝐴 ) )
30	29	ralrimiva	⊢ ( 𝜑 → ∀ 𝑔 ∈ 𝑋 𝑔 ∈ ( ran ∪ 𝑋 ↑m 𝐴 ) )
31		dfss3	⊢ ( 𝑋 ⊆ ( ran ∪ 𝑋 ↑m 𝐴 ) ↔ ∀ 𝑔 ∈ 𝑋 𝑔 ∈ ( ran ∪ 𝑋 ↑m 𝐴 ) )
32	30 31	sylibr	⊢ ( 𝜑 → 𝑋 ⊆ ( ran ∪ 𝑋 ↑m 𝐴 ) )