Metamath Proof Explorer

Theorem elrnust

Description: First direction for ustbas . (Contributed by Thierry Arnoux, 16-Nov-2017)

Ref Expression
Assertion elrnust ⊢ U ∈ UnifOn ⁡ X → U ∈ ⋃ ran ⁡ UnifOn

Proof

Step Hyp Ref Expression
1 elfvdm ⊢ U ∈ UnifOn ⁡ X → X ∈ dom ⁡ UnifOn
2 fveq2 ⊢ x = X → UnifOn ⁡ x = UnifOn ⁡ X
3 2 eleq2d ⊢ x = X → U ∈ UnifOn ⁡ x ↔ U ∈ UnifOn ⁡ X
4 3 rspcev ⊢ X ∈ dom ⁡ UnifOn ∧ U ∈ UnifOn ⁡ X → ∃ x ∈ dom ⁡ UnifOn U ∈ UnifOn ⁡ x
5 1 4 mpancom ⊢ U ∈ UnifOn ⁡ X → ∃ x ∈ dom ⁡ UnifOn U ∈ UnifOn ⁡ x
6 ustfn ⊢ UnifOn Fn V
7 fnfun ⊢ UnifOn Fn V → Fun ⁡ UnifOn
8 elunirn ⊢ Fun ⁡ UnifOn → U ∈ ⋃ ran ⁡ UnifOn ↔ ∃ x ∈ dom ⁡ UnifOn U ∈ UnifOn ⁡ x
9 6 7 8 mp2b ⊢ U ∈ ⋃ ran ⁡ UnifOn ↔ ∃ x ∈ dom ⁡ UnifOn U ∈ UnifOn ⁡ x
10 5 9 sylibr ⊢ U ∈ UnifOn ⁡ X → U ∈ ⋃ ran ⁡ UnifOn