Theorem preiman0

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

	Ref	Expression
Assertion	preiman0	|- ( ( Fun F /\ A C_ ran F /\ A =/= (/) ) -> ( `' F " A ) =/= (/) )

Proof

Step	Hyp	Ref	Expression
1		df-rn	|- ran F = dom `' F
2	1	ineq1i	|- ( ran F i^i ( A i^i ran F ) ) = ( dom `' F i^i ( A i^i ran F ) )
3		dfss2	|- ( A C_ ran F <-> ( A i^i ran F ) = A )
4	3	biimpi	|- ( A C_ ran F -> ( A i^i ran F ) = A )
5	4	ineq2d	|- ( A C_ ran F -> ( ran F i^i ( A i^i ran F ) ) = ( ran F i^i A ) )
6		sseqin2	|- ( A C_ ran F <-> ( ran F i^i A ) = A )
7	6	biimpi	|- ( A C_ ran F -> ( ran F i^i A ) = A )
8	5 7	eqtrd	|- ( A C_ ran F -> ( ran F i^i ( A i^i ran F ) ) = A )
9	8	3ad2ant2	|- ( ( Fun F /\ A C_ ran F /\ ( `' F " A ) = (/) ) -> ( ran F i^i ( A i^i ran F ) ) = A )
10		fimacnvinrn	|- ( Fun F -> ( `' F " A ) = ( `' F " ( A i^i ran F ) ) )
11	10	eqeq1d	|- ( Fun F -> ( ( `' F " A ) = (/) <-> ( `' F " ( A i^i ran F ) ) = (/) ) )
12	11	biimpa	|- ( ( Fun F /\ ( `' F " A ) = (/) ) -> ( `' F " ( A i^i ran F ) ) = (/) )
13	12	3adant2	|- ( ( Fun F /\ A C_ ran F /\ ( `' F " A ) = (/) ) -> ( `' F " ( A i^i ran F ) ) = (/) )
14		imadisj	|- ( ( `' F " ( A i^i ran F ) ) = (/) <-> ( dom `' F i^i ( A i^i ran F ) ) = (/) )
15	13 14	sylib	|- ( ( Fun F /\ A C_ ran F /\ ( `' F " A ) = (/) ) -> ( dom `' F i^i ( A i^i ran F ) ) = (/) )
16	2 9 15	3eqtr3a	|- ( ( Fun F /\ A C_ ran F /\ ( `' F " A ) = (/) ) -> A = (/) )
17	16	3expia	|- ( ( Fun F /\ A C_ ran F ) -> ( ( `' F " A ) = (/) -> A = (/) ) )
18	17	necon3d	|- ( ( Fun F /\ A C_ ran F ) -> ( A =/= (/) -> ( `' F " A ) =/= (/) ) )
19	18	3impia	|- ( ( Fun F /\ A C_ ran F /\ A =/= (/) ) -> ( `' F " A ) =/= (/) )