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 𝐹 ∪ { ∅ } )