Metamath Proof Explorer


Theorem fvclss

Description: Upper bound for the class of values of a class. (Contributed by NM, 9-Nov-1995)

Ref Expression
Assertion fvclss { 𝑦 ∣ ∃ 𝑥 𝑦 = ( 𝐹𝑥 ) } ⊆ ( ran 𝐹 ∪ { ∅ } )

Proof

Step Hyp Ref Expression
1 eqcom ( 𝑦 = ( 𝐹𝑥 ) ↔ ( 𝐹𝑥 ) = 𝑦 )
2 tz6.12i ( 𝑦 ≠ ∅ → ( ( 𝐹𝑥 ) = 𝑦𝑥 𝐹 𝑦 ) )
3 1 2 syl5bi ( 𝑦 ≠ ∅ → ( 𝑦 = ( 𝐹𝑥 ) → 𝑥 𝐹 𝑦 ) )
4 3 eximdv ( 𝑦 ≠ ∅ → ( ∃ 𝑥 𝑦 = ( 𝐹𝑥 ) → ∃ 𝑥 𝑥 𝐹 𝑦 ) )
5 vex 𝑦 ∈ V
6 5 elrn ( 𝑦 ∈ ran 𝐹 ↔ ∃ 𝑥 𝑥 𝐹 𝑦 )
7 4 6 syl6ibr ( 𝑦 ≠ ∅ → ( ∃ 𝑥 𝑦 = ( 𝐹𝑥 ) → 𝑦 ∈ ran 𝐹 ) )
8 7 com12 ( ∃ 𝑥 𝑦 = ( 𝐹𝑥 ) → ( 𝑦 ≠ ∅ → 𝑦 ∈ ran 𝐹 ) )
9 8 necon1bd ( ∃ 𝑥 𝑦 = ( 𝐹𝑥 ) → ( ¬ 𝑦 ∈ ran 𝐹𝑦 = ∅ ) )
10 velsn ( 𝑦 ∈ { ∅ } ↔ 𝑦 = ∅ )
11 9 10 syl6ibr ( ∃ 𝑥 𝑦 = ( 𝐹𝑥 ) → ( ¬ 𝑦 ∈ ran 𝐹𝑦 ∈ { ∅ } ) )
12 11 orrd ( ∃ 𝑥 𝑦 = ( 𝐹𝑥 ) → ( 𝑦 ∈ ran 𝐹𝑦 ∈ { ∅ } ) )
13 12 ss2abi { 𝑦 ∣ ∃ 𝑥 𝑦 = ( 𝐹𝑥 ) } ⊆ { 𝑦 ∣ ( 𝑦 ∈ ran 𝐹𝑦 ∈ { ∅ } ) }
14 df-un ( ran 𝐹 ∪ { ∅ } ) = { 𝑦 ∣ ( 𝑦 ∈ ran 𝐹𝑦 ∈ { ∅ } ) }
15 13 14 sseqtrri { 𝑦 ∣ ∃ 𝑥 𝑦 = ( 𝐹𝑥 ) } ⊆ ( ran 𝐹 ∪ { ∅ } )