Metamath Proof Explorer

Theorem mptpreima

Description: The preimage of a function in maps-to notation. (Contributed by Stefan O'Rear, 25-Jan-2015)

Ref Expression
Hypothesis dmmpt.1 ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
Assertion mptpreima ( ◡ 𝐹 “ 𝐶 ) = { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ 𝐶 }

Proof

Step Hyp Ref Expression
1 dmmpt.1 ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
2 df-mpt ⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) }
3 1 2 eqtri ⊢ 𝐹 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) }
4 3 cnveqi ⊢ ◡ 𝐹 = ◡ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) }
5 cnvopab ⊢ ◡ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) } = { ⟨ 𝑦 , 𝑥 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) }
6 4 5 eqtri ⊢ ◡ 𝐹 = { ⟨ 𝑦 , 𝑥 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) }
7 6 imaeq1i ⊢ ( ◡ 𝐹 “ 𝐶 ) = ( { ⟨ 𝑦 , 𝑥 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) } “ 𝐶 )
8 df-ima ⊢ ( { ⟨ 𝑦 , 𝑥 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) } “ 𝐶 ) = ran ( { ⟨ 𝑦 , 𝑥 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) } ↾ 𝐶 )
9 resopab ⊢ ( { ⟨ 𝑦 , 𝑥 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) } ↾ 𝐶 ) = { ⟨ 𝑦 , 𝑥 ⟩ ∣ ( 𝑦 ∈ 𝐶 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) ) }
10 9 rneqi ⊢ ran ( { ⟨ 𝑦 , 𝑥 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) } ↾ 𝐶 ) = ran { ⟨ 𝑦 , 𝑥 ⟩ ∣ ( 𝑦 ∈ 𝐶 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) ) }
11 ancom ⊢ ( ( 𝑦 ∈ 𝐶 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) ∧ 𝑦 ∈ 𝐶 ) )
12 anass ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) ∧ 𝑦 ∈ 𝐶 ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝑦 = 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) )
13 11 12 bitri ⊢ ( ( 𝑦 ∈ 𝐶 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝑦 = 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) )
14 13 exbii ⊢ ( ∃ 𝑦 ( 𝑦 ∈ 𝐶 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) ) ↔ ∃ 𝑦 ( 𝑥 ∈ 𝐴 ∧ ( 𝑦 = 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) )
15 19.42v ⊢ ( ∃ 𝑦 ( 𝑥 ∈ 𝐴 ∧ ( 𝑦 = 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ∃ 𝑦 ( 𝑦 = 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) )
16 dfclel ⊢ ( 𝐵 ∈ 𝐶 ↔ ∃ 𝑦 ( 𝑦 = 𝐵 ∧ 𝑦 ∈ 𝐶 ) )
17 16 bicomi ⊢ ( ∃ 𝑦 ( 𝑦 = 𝐵 ∧ 𝑦 ∈ 𝐶 ) ↔ 𝐵 ∈ 𝐶 )
18 17 anbi2i ⊢ ( ( 𝑥 ∈ 𝐴 ∧ ∃ 𝑦 ( 𝑦 = 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝐶 ) )
19 15 18 bitri ⊢ ( ∃ 𝑦 ( 𝑥 ∈ 𝐴 ∧ ( 𝑦 = 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝐶 ) )
20 14 19 bitri ⊢ ( ∃ 𝑦 ( 𝑦 ∈ 𝐶 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝐶 ) )
21 20 abbii ⊢ { 𝑥 ∣ ∃ 𝑦 ( 𝑦 ∈ 𝐶 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) ) } = { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝐶 ) }
22 rnopab ⊢ ran { ⟨ 𝑦 , 𝑥 ⟩ ∣ ( 𝑦 ∈ 𝐶 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) ) } = { 𝑥 ∣ ∃ 𝑦 ( 𝑦 ∈ 𝐶 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) ) }
23 df-rab ⊢ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ 𝐶 } = { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝐶 ) }
24 21 22 23 3eqtr4i ⊢ ran { ⟨ 𝑦 , 𝑥 ⟩ ∣ ( 𝑦 ∈ 𝐶 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) ) } = { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ 𝐶 }
25 10 24 eqtri ⊢ ran ( { ⟨ 𝑦 , 𝑥 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) } ↾ 𝐶 ) = { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ 𝐶 }
26 8 25 eqtri ⊢ ( { ⟨ 𝑦 , 𝑥 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) } “ 𝐶 ) = { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ 𝐶 }
27 7 26 eqtri ⊢ ( ◡ 𝐹 “ 𝐶 ) = { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ 𝐶 }