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 𝐹 ) = { 𝐴 , 𝐵 } ) ) |