Theorem preiman0

Description: The preimage of a nonempty set is nonempty. (Contributed by Thierry Arnoux, 9-Jun-2024)

	Ref	Expression
Assertion	preiman0	⊢ ( ( Fun 𝐹 ∧ 𝐴 ⊆ ran 𝐹 ∧ 𝐴 ≠ ∅ ) → ( ◡ 𝐹 “ 𝐴 ) ≠ ∅ )

Proof

Step	Hyp	Ref	Expression
1		df-rn	⊢ ran 𝐹 = dom ◡ 𝐹
2	1	ineq1i	⊢ ( ran 𝐹 ∩ ( 𝐴 ∩ ran 𝐹 ) ) = ( dom ◡ 𝐹 ∩ ( 𝐴 ∩ ran 𝐹 ) )
3		dfss2	⊢ ( 𝐴 ⊆ ran 𝐹 ↔ ( 𝐴 ∩ ran 𝐹 ) = 𝐴 )
4	3	biimpi	⊢ ( 𝐴 ⊆ ran 𝐹 → ( 𝐴 ∩ ran 𝐹 ) = 𝐴 )
5	4	ineq2d	⊢ ( 𝐴 ⊆ ran 𝐹 → ( ran 𝐹 ∩ ( 𝐴 ∩ ran 𝐹 ) ) = ( ran 𝐹 ∩ 𝐴 ) )
6		sseqin2	⊢ ( 𝐴 ⊆ ran 𝐹 ↔ ( ran 𝐹 ∩ 𝐴 ) = 𝐴 )
7	6	biimpi	⊢ ( 𝐴 ⊆ ran 𝐹 → ( ran 𝐹 ∩ 𝐴 ) = 𝐴 )
8	5 7	eqtrd	⊢ ( 𝐴 ⊆ ran 𝐹 → ( ran 𝐹 ∩ ( 𝐴 ∩ ran 𝐹 ) ) = 𝐴 )
9	8	3ad2ant2	⊢ ( ( Fun 𝐹 ∧ 𝐴 ⊆ ran 𝐹 ∧ ( ◡ 𝐹 “ 𝐴 ) = ∅ ) → ( ran 𝐹 ∩ ( 𝐴 ∩ ran 𝐹 ) ) = 𝐴 )
10		fimacnvinrn	⊢ ( Fun 𝐹 → ( ◡ 𝐹 “ 𝐴 ) = ( ◡ 𝐹 “ ( 𝐴 ∩ ran 𝐹 ) ) )
11	10	eqeq1d	⊢ ( Fun 𝐹 → ( ( ◡ 𝐹 “ 𝐴 ) = ∅ ↔ ( ◡ 𝐹 “ ( 𝐴 ∩ ran 𝐹 ) ) = ∅ ) )
12	11	biimpa	⊢ ( ( Fun 𝐹 ∧ ( ◡ 𝐹 “ 𝐴 ) = ∅ ) → ( ◡ 𝐹 “ ( 𝐴 ∩ ran 𝐹 ) ) = ∅ )
13	12	3adant2	⊢ ( ( Fun 𝐹 ∧ 𝐴 ⊆ ran 𝐹 ∧ ( ◡ 𝐹 “ 𝐴 ) = ∅ ) → ( ◡ 𝐹 “ ( 𝐴 ∩ ran 𝐹 ) ) = ∅ )
14		imadisj	⊢ ( ( ◡ 𝐹 “ ( 𝐴 ∩ ran 𝐹 ) ) = ∅ ↔ ( dom ◡ 𝐹 ∩ ( 𝐴 ∩ ran 𝐹 ) ) = ∅ )
15	13 14	sylib	⊢ ( ( Fun 𝐹 ∧ 𝐴 ⊆ ran 𝐹 ∧ ( ◡ 𝐹 “ 𝐴 ) = ∅ ) → ( dom ◡ 𝐹 ∩ ( 𝐴 ∩ ran 𝐹 ) ) = ∅ )
16	2 9 15	3eqtr3a	⊢ ( ( Fun 𝐹 ∧ 𝐴 ⊆ ran 𝐹 ∧ ( ◡ 𝐹 “ 𝐴 ) = ∅ ) → 𝐴 = ∅ )
17	16	3expia	⊢ ( ( Fun 𝐹 ∧ 𝐴 ⊆ ran 𝐹 ) → ( ( ◡ 𝐹 “ 𝐴 ) = ∅ → 𝐴 = ∅ ) )
18	17	necon3d	⊢ ( ( Fun 𝐹 ∧ 𝐴 ⊆ ran 𝐹 ) → ( 𝐴 ≠ ∅ → ( ◡ 𝐹 “ 𝐴 ) ≠ ∅ ) )
19	18	3impia	⊢ ( ( Fun 𝐹 ∧ 𝐴 ⊆ ran 𝐹 ∧ 𝐴 ≠ ∅ ) → ( ◡ 𝐹 “ 𝐴 ) ≠ ∅ )