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 ⊢ φ → A ∈ V
unirnmap.x ⊢ φ → X ⊆ B A
Assertion unirnmap ⊢ φ → X ⊆ ran ⁡ ⋃ X A

Proof

Step Hyp Ref Expression
1 unirnmap.a ⊢ φ → A ∈ V
2 unirnmap.x ⊢ φ → X ⊆ B A
3 2 sselda ⊢ φ ∧ g ∈ X → g ∈ B A
4 elmapfn ⊢ g ∈ B A → g Fn A
5 3 4 syl ⊢ φ ∧ g ∈ X → g Fn A
6 simplr ⊢ φ ∧ g ∈ X ∧ x ∈ A → g ∈ X
7 dffn3 ⊢ g Fn A ↔ g : A ⟶ ran ⁡ g
8 5 7 sylib ⊢ φ ∧ g ∈ X → g : A ⟶ ran ⁡ g
9 8 ffvelrnda ⊢ φ ∧ g ∈ X ∧ x ∈ A → g ⁡ x ∈ ran ⁡ g
10 rneq ⊢ f = g → ran ⁡ f = ran ⁡ g
11 10 eleq2d ⊢ f = g → g ⁡ x ∈ ran ⁡ f ↔ g ⁡ x ∈ ran ⁡ g
12 11 rspcev ⊢ g ∈ X ∧ g ⁡ x ∈ ran ⁡ g → ∃ f ∈ X g ⁡ x ∈ ran ⁡ f
13 6 9 12 syl2anc ⊢ φ ∧ g ∈ X ∧ x ∈ A → ∃ f ∈ X g ⁡ x ∈ ran ⁡ f
14 eliun ⊢ g ⁡ x ∈ ⋃ f ∈ X ran ⁡ f ↔ ∃ f ∈ X g ⁡ x ∈ ran ⁡ f
15 13 14 sylibr ⊢ φ ∧ g ∈ X ∧ x ∈ A → g ⁡ x ∈ ⋃ f ∈ X ran ⁡ f
16 rnuni ⊢ ran ⁡ ⋃ X = ⋃ f ∈ X ran ⁡ f
17 15 16 eleqtrrdi ⊢ φ ∧ g ∈ X ∧ x ∈ A → g ⁡ x ∈ ran ⁡ ⋃ X
18 17 ralrimiva ⊢ φ ∧ g ∈ X → ∀ x ∈ A g ⁡ x ∈ ran ⁡ ⋃ X
19 5 18 jca ⊢ φ ∧ g ∈ X → g Fn A ∧ ∀ x ∈ A g ⁡ x ∈ ran ⁡ ⋃ X
20 ffnfv ⊢ g : A ⟶ ran ⁡ ⋃ X ↔ g Fn A ∧ ∀ x ∈ A g ⁡ x ∈ ran ⁡ ⋃ X
21 19 20 sylibr ⊢ φ ∧ g ∈ X → g : A ⟶ ran ⁡ ⋃ X
22 ovexd ⊢ φ → B A ∈ V
23 22 2 ssexd ⊢ φ → X ∈ V
24 23 uniexd ⊢ φ → ⋃ X ∈ V
25 rnexg ⊢ ⋃ X ∈ V → ran ⁡ ⋃ X ∈ V
26 24 25 syl ⊢ φ → ran ⁡ ⋃ X ∈ V
27 26 1 elmapd ⊢ φ → g ∈ ran ⁡ ⋃ X A ↔ g : A ⟶ ran ⁡ ⋃ X
28 27 adantr ⊢ φ ∧ g ∈ X → g ∈ ran ⁡ ⋃ X A ↔ g : A ⟶ ran ⁡ ⋃ X
29 21 28 mpbird ⊢ φ ∧ g ∈ X → g ∈ ran ⁡ ⋃ X A
30 29 ralrimiva ⊢ φ → ∀ g ∈ X g ∈ ran ⁡ ⋃ X A
31 dfss3 ⊢ X ⊆ ran ⁡ ⋃ X A ↔ ∀ g ∈ X g ∈ ran ⁡ ⋃ X A
32 30 31 sylibr ⊢ φ → X ⊆ ran ⁡ ⋃ X A