Theorem suppdm

Description: If the range of a function does not contain the zero, the support of the function equals its domain. (Contributed by AV, 20-May-2020)

	Ref	Expression
Assertion	suppdm	⊢ ( ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝑍 ∉ ran 𝐹 ) → ( 𝐹 supp 𝑍 ) = dom 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		suppval1	⊢ ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 𝐹 supp 𝑍 ) = { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) ≠ 𝑍 } )
2	1	adantr	⊢ ( ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝑍 ∉ ran 𝐹 ) → ( 𝐹 supp 𝑍 ) = { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) ≠ 𝑍 } )
3		df-nel	⊢ ( 𝑍 ∉ ran 𝐹 ↔ ¬ 𝑍 ∈ ran 𝐹 )
4		fvelrn	⊢ ( ( Fun 𝐹 ∧ 𝑥 ∈ dom 𝐹 ) → ( 𝐹 ‘ 𝑥 ) ∈ ran 𝐹 )
5	4	3ad2antl1	⊢ ( ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝑥 ∈ dom 𝐹 ) → ( 𝐹 ‘ 𝑥 ) ∈ ran 𝐹 )
6		eleq1	⊢ ( 𝑍 = ( 𝐹 ‘ 𝑥 ) → ( 𝑍 ∈ ran 𝐹 ↔ ( 𝐹 ‘ 𝑥 ) ∈ ran 𝐹 ) )
7	6	eqcoms	⊢ ( ( 𝐹 ‘ 𝑥 ) = 𝑍 → ( 𝑍 ∈ ran 𝐹 ↔ ( 𝐹 ‘ 𝑥 ) ∈ ran 𝐹 ) )
8	5 7	syl5ibrcom	⊢ ( ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝑥 ∈ dom 𝐹 ) → ( ( 𝐹 ‘ 𝑥 ) = 𝑍 → 𝑍 ∈ ran 𝐹 ) )
9	8	necon3bd	⊢ ( ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝑥 ∈ dom 𝐹 ) → ( ¬ 𝑍 ∈ ran 𝐹 → ( 𝐹 ‘ 𝑥 ) ≠ 𝑍 ) )
10	3 9	syl5bi	⊢ ( ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝑥 ∈ dom 𝐹 ) → ( 𝑍 ∉ ran 𝐹 → ( 𝐹 ‘ 𝑥 ) ≠ 𝑍 ) )
11	10	impancom	⊢ ( ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝑍 ∉ ran 𝐹 ) → ( 𝑥 ∈ dom 𝐹 → ( 𝐹 ‘ 𝑥 ) ≠ 𝑍 ) )
12	11	ralrimiv	⊢ ( ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝑍 ∉ ran 𝐹 ) → ∀ 𝑥 ∈ dom 𝐹 ( 𝐹 ‘ 𝑥 ) ≠ 𝑍 )
13		rabid2	⊢ ( dom 𝐹 = { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) ≠ 𝑍 } ↔ ∀ 𝑥 ∈ dom 𝐹 ( 𝐹 ‘ 𝑥 ) ≠ 𝑍 )
14	12 13	sylibr	⊢ ( ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝑍 ∉ ran 𝐹 ) → dom 𝐹 = { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) ≠ 𝑍 } )
15	2 14	eqtr4d	⊢ ( ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝑍 ∉ ran 𝐹 ) → ( 𝐹 supp 𝑍 ) = dom 𝐹 )