Metamath Proof Explorer

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 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑋 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑔 ‘ 𝑥 ) ∈ 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 𝐴 ) )