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 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 𝐴 ) )