Metamath Proof Explorer


Theorem fvssunirnOLD

Description: Obsolete version of fvssunirn as of 13-Jan-2025. (Contributed by Stefan O'Rear, 2-Nov-2014) (Revised by Mario Carneiro, 31-Aug-2015) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion fvssunirnOLD ( 𝐹𝑋 ) ⊆ ran 𝐹

Proof

Step Hyp Ref Expression
1 fvrn0 ( 𝐹𝑋 ) ∈ ( ran 𝐹 ∪ { ∅ } )
2 elssuni ( ( 𝐹𝑋 ) ∈ ( ran 𝐹 ∪ { ∅ } ) → ( 𝐹𝑋 ) ⊆ ( ran 𝐹 ∪ { ∅ } ) )
3 1 2 ax-mp ( 𝐹𝑋 ) ⊆ ( ran 𝐹 ∪ { ∅ } )
4 uniun ( ran 𝐹 ∪ { ∅ } ) = ( ran 𝐹 { ∅ } )
5 0ex ∅ ∈ V
6 5 unisn { ∅ } = ∅
7 6 uneq2i ( ran 𝐹 { ∅ } ) = ( ran 𝐹 ∪ ∅ )
8 un0 ( ran 𝐹 ∪ ∅ ) = ran 𝐹
9 4 7 8 3eqtri ( ran 𝐹 ∪ { ∅ } ) = ran 𝐹
10 3 9 sseqtri ( 𝐹𝑋 ) ⊆ ran 𝐹