Metamath Proof Explorer

Theorem imarnf1pr

Description: The image of the range of a function F under a function E if F is a function from a pair into the domain of E . (Contributed by Alexander van der Vekens, 2-Feb-2018)

Ref Expression
Assertion imarnf1pr ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) → ( ( ( 𝐹 : { 𝑋 , 𝑌 } ⟶ dom 𝐸 ∧ 𝐸 : dom 𝐸 ⟶ 𝑅 ) ∧ ( ( 𝐸 ‘ ( 𝐹 ‘ 𝑋 ) ) = 𝐴 ∧ ( 𝐸 ‘ ( 𝐹 ‘ 𝑌 ) ) = 𝐵 ) ) → ( 𝐸 “ ran 𝐹 ) = { 𝐴 , 𝐵 } ) )

Proof

Step Hyp Ref Expression
1 ffn ⊢ ( 𝐸 : dom 𝐸 ⟶ 𝑅 → 𝐸 Fn dom 𝐸 )
2 1 adantl ⊢ ( ( 𝐹 : { 𝑋 , 𝑌 } ⟶ dom 𝐸 ∧ 𝐸 : dom 𝐸 ⟶ 𝑅 ) → 𝐸 Fn dom 𝐸 )
3 2 adantr ⊢ ( ( ( 𝐹 : { 𝑋 , 𝑌 } ⟶ dom 𝐸 ∧ 𝐸 : dom 𝐸 ⟶ 𝑅 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ) → 𝐸 Fn dom 𝐸 )
4 simpll ⊢ ( ( ( 𝐹 : { 𝑋 , 𝑌 } ⟶ dom 𝐸 ∧ 𝐸 : dom 𝐸 ⟶ 𝑅 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ) → 𝐹 : { 𝑋 , 𝑌 } ⟶ dom 𝐸 )
5 prid1g ⊢ ( 𝑋 ∈ 𝑉 → 𝑋 ∈ { 𝑋 , 𝑌 } )
6 5 adantr ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) → 𝑋 ∈ { 𝑋 , 𝑌 } )
7 6 adantl ⊢ ( ( ( 𝐹 : { 𝑋 , 𝑌 } ⟶ dom 𝐸 ∧ 𝐸 : dom 𝐸 ⟶ 𝑅 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ) → 𝑋 ∈ { 𝑋 , 𝑌 } )
8 4 7 ffvelcdmd ⊢ ( ( ( 𝐹 : { 𝑋 , 𝑌 } ⟶ dom 𝐸 ∧ 𝐸 : dom 𝐸 ⟶ 𝑅 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ) → ( 𝐹 ‘ 𝑋 ) ∈ dom 𝐸 )
9 prid2g ⊢ ( 𝑌 ∈ 𝑊 → 𝑌 ∈ { 𝑋 , 𝑌 } )
10 9 ad2antll ⊢ ( ( ( 𝐹 : { 𝑋 , 𝑌 } ⟶ dom 𝐸 ∧ 𝐸 : dom 𝐸 ⟶ 𝑅 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ) → 𝑌 ∈ { 𝑋 , 𝑌 } )
11 4 10 ffvelcdmd ⊢ ( ( ( 𝐹 : { 𝑋 , 𝑌 } ⟶ dom 𝐸 ∧ 𝐸 : dom 𝐸 ⟶ 𝑅 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ) → ( 𝐹 ‘ 𝑌 ) ∈ dom 𝐸 )
12 fnimapr ⊢ ( ( 𝐸 Fn dom 𝐸 ∧ ( 𝐹 ‘ 𝑋 ) ∈ dom 𝐸 ∧ ( 𝐹 ‘ 𝑌 ) ∈ dom 𝐸 ) → ( 𝐸 “ { ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑌 ) } ) = { ( 𝐸 ‘ ( 𝐹 ‘ 𝑋 ) ) , ( 𝐸 ‘ ( 𝐹 ‘ 𝑌 ) ) } )
13 3 8 11 12 syl3anc ⊢ ( ( ( 𝐹 : { 𝑋 , 𝑌 } ⟶ dom 𝐸 ∧ 𝐸 : dom 𝐸 ⟶ 𝑅 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ) → ( 𝐸 “ { ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑌 ) } ) = { ( 𝐸 ‘ ( 𝐹 ‘ 𝑋 ) ) , ( 𝐸 ‘ ( 𝐹 ‘ 𝑌 ) ) } )
14 13 ex ⊢ ( ( 𝐹 : { 𝑋 , 𝑌 } ⟶ dom 𝐸 ∧ 𝐸 : dom 𝐸 ⟶ 𝑅 ) → ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) → ( 𝐸 “ { ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑌 ) } ) = { ( 𝐸 ‘ ( 𝐹 ‘ 𝑋 ) ) , ( 𝐸 ‘ ( 𝐹 ‘ 𝑌 ) ) } ) )
15 14 adantr ⊢ ( ( ( 𝐹 : { 𝑋 , 𝑌 } ⟶ dom 𝐸 ∧ 𝐸 : dom 𝐸 ⟶ 𝑅 ) ∧ ( ( 𝐸 ‘ ( 𝐹 ‘ 𝑋 ) ) = 𝐴 ∧ ( 𝐸 ‘ ( 𝐹 ‘ 𝑌 ) ) = 𝐵 ) ) → ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) → ( 𝐸 “ { ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑌 ) } ) = { ( 𝐸 ‘ ( 𝐹 ‘ 𝑋 ) ) , ( 𝐸 ‘ ( 𝐹 ‘ 𝑌 ) ) } ) )
16 15 impcom ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ∧ ( ( 𝐹 : { 𝑋 , 𝑌 } ⟶ dom 𝐸 ∧ 𝐸 : dom 𝐸 ⟶ 𝑅 ) ∧ ( ( 𝐸 ‘ ( 𝐹 ‘ 𝑋 ) ) = 𝐴 ∧ ( 𝐸 ‘ ( 𝐹 ‘ 𝑌 ) ) = 𝐵 ) ) ) → ( 𝐸 “ { ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑌 ) } ) = { ( 𝐸 ‘ ( 𝐹 ‘ 𝑋 ) ) , ( 𝐸 ‘ ( 𝐹 ‘ 𝑌 ) ) } )
17 ffn ⊢ ( 𝐹 : { 𝑋 , 𝑌 } ⟶ dom 𝐸 → 𝐹 Fn { 𝑋 , 𝑌 } )
18 rnfdmpr ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) → ( 𝐹 Fn { 𝑋 , 𝑌 } → ran 𝐹 = { ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑌 ) } ) )
19 17 18 syl5com ⊢ ( 𝐹 : { 𝑋 , 𝑌 } ⟶ dom 𝐸 → ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) → ran 𝐹 = { ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑌 ) } ) )
20 19 adantr ⊢ ( ( 𝐹 : { 𝑋 , 𝑌 } ⟶ dom 𝐸 ∧ 𝐸 : dom 𝐸 ⟶ 𝑅 ) → ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) → ran 𝐹 = { ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑌 ) } ) )
21 20 adantr ⊢ ( ( ( 𝐹 : { 𝑋 , 𝑌 } ⟶ dom 𝐸 ∧ 𝐸 : dom 𝐸 ⟶ 𝑅 ) ∧ ( ( 𝐸 ‘ ( 𝐹 ‘ 𝑋 ) ) = 𝐴 ∧ ( 𝐸 ‘ ( 𝐹 ‘ 𝑌 ) ) = 𝐵 ) ) → ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) → ran 𝐹 = { ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑌 ) } ) )
22 21 impcom ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ∧ ( ( 𝐹 : { 𝑋 , 𝑌 } ⟶ dom 𝐸 ∧ 𝐸 : dom 𝐸 ⟶ 𝑅 ) ∧ ( ( 𝐸 ‘ ( 𝐹 ‘ 𝑋 ) ) = 𝐴 ∧ ( 𝐸 ‘ ( 𝐹 ‘ 𝑌 ) ) = 𝐵 ) ) ) → ran 𝐹 = { ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑌 ) } )
23 22 eqcomd ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ∧ ( ( 𝐹 : { 𝑋 , 𝑌 } ⟶ dom 𝐸 ∧ 𝐸 : dom 𝐸 ⟶ 𝑅 ) ∧ ( ( 𝐸 ‘ ( 𝐹 ‘ 𝑋 ) ) = 𝐴 ∧ ( 𝐸 ‘ ( 𝐹 ‘ 𝑌 ) ) = 𝐵 ) ) ) → { ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑌 ) } = ran 𝐹 )
24 23 imaeq2d ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ∧ ( ( 𝐹 : { 𝑋 , 𝑌 } ⟶ dom 𝐸 ∧ 𝐸 : dom 𝐸 ⟶ 𝑅 ) ∧ ( ( 𝐸 ‘ ( 𝐹 ‘ 𝑋 ) ) = 𝐴 ∧ ( 𝐸 ‘ ( 𝐹 ‘ 𝑌 ) ) = 𝐵 ) ) ) → ( 𝐸 “ { ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑌 ) } ) = ( 𝐸 “ ran 𝐹 ) )
25 preq12 ⊢ ( ( ( 𝐸 ‘ ( 𝐹 ‘ 𝑋 ) ) = 𝐴 ∧ ( 𝐸 ‘ ( 𝐹 ‘ 𝑌 ) ) = 𝐵 ) → { ( 𝐸 ‘ ( 𝐹 ‘ 𝑋 ) ) , ( 𝐸 ‘ ( 𝐹 ‘ 𝑌 ) ) } = { 𝐴 , 𝐵 } )
26 25 ad2antll ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ∧ ( ( 𝐹 : { 𝑋 , 𝑌 } ⟶ dom 𝐸 ∧ 𝐸 : dom 𝐸 ⟶ 𝑅 ) ∧ ( ( 𝐸 ‘ ( 𝐹 ‘ 𝑋 ) ) = 𝐴 ∧ ( 𝐸 ‘ ( 𝐹 ‘ 𝑌 ) ) = 𝐵 ) ) ) → { ( 𝐸 ‘ ( 𝐹 ‘ 𝑋 ) ) , ( 𝐸 ‘ ( 𝐹 ‘ 𝑌 ) ) } = { 𝐴 , 𝐵 } )
27 16 24 26 3eqtr3d ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ∧ ( ( 𝐹 : { 𝑋 , 𝑌 } ⟶ dom 𝐸 ∧ 𝐸 : dom 𝐸 ⟶ 𝑅 ) ∧ ( ( 𝐸 ‘ ( 𝐹 ‘ 𝑋 ) ) = 𝐴 ∧ ( 𝐸 ‘ ( 𝐹 ‘ 𝑌 ) ) = 𝐵 ) ) ) → ( 𝐸 “ ran 𝐹 ) = { 𝐴 , 𝐵 } )
28 27 ex ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) → ( ( ( 𝐹 : { 𝑋 , 𝑌 } ⟶ dom 𝐸 ∧ 𝐸 : dom 𝐸 ⟶ 𝑅 ) ∧ ( ( 𝐸 ‘ ( 𝐹 ‘ 𝑋 ) ) = 𝐴 ∧ ( 𝐸 ‘ ( 𝐹 ‘ 𝑌 ) ) = 𝐵 ) ) → ( 𝐸 “ ran 𝐹 ) = { 𝐴 , 𝐵 } ) )