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

Metamath Proof Explorer

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 𝐹 ∧ 𝐴 ≠ ∅ ) → ( ◡ 𝐹 “ 𝐴 ) ≠ ∅ )