This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 biimtrid ⊢ ( 𝑦 ≠ ∅ → ( 𝑦 = ( 𝐹 ‘ 𝑥 ) → 𝑥 𝐹 𝑦 ) )
4 3 eximdv ⊢ ( 𝑦 ≠ ∅ → ( ∃ 𝑥 𝑦 = ( 𝐹 ‘ 𝑥 ) → ∃ 𝑥 𝑥 𝐹 𝑦 ) )
5 vex ⊢ 𝑦 ∈ V
6 5 elrn ⊢ ( 𝑦 ∈ ran 𝐹 ↔ ∃ 𝑥 𝑥 𝐹 𝑦 )
7 4 6 imbitrrdi ⊢ ( 𝑦 ≠ ∅ → ( ∃ 𝑥 𝑦 = ( 𝐹 ‘ 𝑥 ) → 𝑦 ∈ ran 𝐹 ) )
8 7 com12 ⊢ ( ∃ 𝑥 𝑦 = ( 𝐹 ‘ 𝑥 ) → ( 𝑦 ≠ ∅ → 𝑦 ∈ ran 𝐹 ) )
9 8 necon1bd ⊢ ( ∃ 𝑥 𝑦 = ( 𝐹 ‘ 𝑥 ) → ( ¬ 𝑦 ∈ ran 𝐹 → 𝑦 = ∅ ) )
10 velsn ⊢ ( 𝑦 ∈ { ∅ } ↔ 𝑦 = ∅ )
11 9 10 imbitrrdi ⊢ ( ∃ 𝑥 𝑦 = ( 𝐹 ‘ 𝑥 ) → ( ¬ 𝑦 ∈ ran 𝐹 → 𝑦 ∈ { ∅ } ) )
12 11 orrd ⊢ ( ∃ 𝑥 𝑦 = ( 𝐹 ‘ 𝑥 ) → ( 𝑦 ∈ ran 𝐹 ∨ 𝑦 ∈ { ∅ } ) )
13 12 ss2abi ⊢ { 𝑦 ∣ ∃ 𝑥 𝑦 = ( 𝐹 ‘ 𝑥 ) } ⊆ { 𝑦 ∣ ( 𝑦 ∈ ran 𝐹 ∨ 𝑦 ∈ { ∅ } ) }
14 df-un ⊢ ( ran 𝐹 ∪ { ∅ } ) = { 𝑦 ∣ ( 𝑦 ∈ ran 𝐹 ∨ 𝑦 ∈ { ∅ } ) }
15 13 14 sseqtrri ⊢ { 𝑦 ∣ ∃ 𝑥 𝑦 = ( 𝐹 ‘ 𝑥 ) } ⊆ ( ran 𝐹 ∪ { ∅ } )