Metamath Proof Explorer

Theorem elrnust

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

Ref Expression
Assertion elrnust ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → 𝑈 ∈ ∪ ran UnifOn )

Proof

Step Hyp Ref Expression
1 elfvdm ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → 𝑋 ∈ dom UnifOn )
2 fveq2 ⊢ ( 𝑥 = 𝑋 → ( UnifOn ‘ 𝑥 ) = ( UnifOn ‘ 𝑋 ) )
3 2 eleq2d ⊢ ( 𝑥 = 𝑋 → ( 𝑈 ∈ ( UnifOn ‘ 𝑥 ) ↔ 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ) )
4 3 rspcev ⊢ ( ( 𝑋 ∈ dom UnifOn ∧ 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ) → ∃ 𝑥 ∈ dom UnifOn 𝑈 ∈ ( UnifOn ‘ 𝑥 ) )
5 1 4 mpancom ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ∃ 𝑥 ∈ dom UnifOn 𝑈 ∈ ( UnifOn ‘ 𝑥 ) )
6 ustfn ⊢ UnifOn Fn V
7 fnfun ⊢ ( UnifOn Fn V → Fun UnifOn )
8 elunirn ⊢ ( Fun UnifOn → ( 𝑈 ∈ ∪ ran UnifOn ↔ ∃ 𝑥 ∈ dom UnifOn 𝑈 ∈ ( UnifOn ‘ 𝑥 ) ) )
9 6 7 8 mp2b ⊢ ( 𝑈 ∈ ∪ ran UnifOn ↔ ∃ 𝑥 ∈ dom UnifOn 𝑈 ∈ ( UnifOn ‘ 𝑥 ) )
10 5 9 sylibr ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → 𝑈 ∈ ∪ ran UnifOn )