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 ffvelrnd ( ( ( 𝐹 : { 𝑋 , 𝑌 } ⟶ dom 𝐸𝐸 : dom 𝐸𝑅 ) ∧ ( 𝑋𝑉𝑌𝑊 ) ) → ( 𝐹𝑋 ) ∈ dom 𝐸 )
9 prid2g ( 𝑌𝑊𝑌 ∈ { 𝑋 , 𝑌 } )
10 9 ad2antll ( ( ( 𝐹 : { 𝑋 , 𝑌 } ⟶ dom 𝐸𝐸 : dom 𝐸𝑅 ) ∧ ( 𝑋𝑉𝑌𝑊 ) ) → 𝑌 ∈ { 𝑋 , 𝑌 } )
11 4 10 ffvelrnd ( ( ( 𝐹 : { 𝑋 , 𝑌 } ⟶ 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 𝐹 ) = { 𝐴 , 𝐵 } ) )