Step |
Hyp |
Ref |
Expression |
1 |
|
funrel |
⊢ ( Fun 𝐴 → Rel 𝐴 ) |
2 |
|
1st2nd |
⊢ ( ( Rel 𝐴 ∧ 𝑋 ∈ 𝐴 ) → 𝑋 = 〈 ( 1st ‘ 𝑋 ) , ( 2nd ‘ 𝑋 ) 〉 ) |
3 |
1 2
|
sylan |
⊢ ( ( Fun 𝐴 ∧ 𝑋 ∈ 𝐴 ) → 𝑋 = 〈 ( 1st ‘ 𝑋 ) , ( 2nd ‘ 𝑋 ) 〉 ) |
4 |
|
simpl1l |
⊢ ( ( ( ( Fun 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑋 = 〈 ( 1st ‘ 𝑋 ) , ( 2nd ‘ 𝑋 ) 〉 ∧ 𝐵 ⊆ 𝐴 ) ∧ ( 1st ‘ 𝑋 ) ∈ dom 𝐵 ) → Fun 𝐴 ) |
5 |
|
simpl3 |
⊢ ( ( ( ( Fun 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑋 = 〈 ( 1st ‘ 𝑋 ) , ( 2nd ‘ 𝑋 ) 〉 ∧ 𝐵 ⊆ 𝐴 ) ∧ ( 1st ‘ 𝑋 ) ∈ dom 𝐵 ) → 𝐵 ⊆ 𝐴 ) |
6 |
|
simpr |
⊢ ( ( ( ( Fun 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑋 = 〈 ( 1st ‘ 𝑋 ) , ( 2nd ‘ 𝑋 ) 〉 ∧ 𝐵 ⊆ 𝐴 ) ∧ ( 1st ‘ 𝑋 ) ∈ dom 𝐵 ) → ( 1st ‘ 𝑋 ) ∈ dom 𝐵 ) |
7 |
|
funssfv |
⊢ ( ( Fun 𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ ( 1st ‘ 𝑋 ) ∈ dom 𝐵 ) → ( 𝐴 ‘ ( 1st ‘ 𝑋 ) ) = ( 𝐵 ‘ ( 1st ‘ 𝑋 ) ) ) |
8 |
4 5 6 7
|
syl3anc |
⊢ ( ( ( ( Fun 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑋 = 〈 ( 1st ‘ 𝑋 ) , ( 2nd ‘ 𝑋 ) 〉 ∧ 𝐵 ⊆ 𝐴 ) ∧ ( 1st ‘ 𝑋 ) ∈ dom 𝐵 ) → ( 𝐴 ‘ ( 1st ‘ 𝑋 ) ) = ( 𝐵 ‘ ( 1st ‘ 𝑋 ) ) ) |
9 |
|
eleq1 |
⊢ ( 𝑋 = 〈 ( 1st ‘ 𝑋 ) , ( 2nd ‘ 𝑋 ) 〉 → ( 𝑋 ∈ 𝐴 ↔ 〈 ( 1st ‘ 𝑋 ) , ( 2nd ‘ 𝑋 ) 〉 ∈ 𝐴 ) ) |
10 |
9
|
adantl |
⊢ ( ( Fun 𝐴 ∧ 𝑋 = 〈 ( 1st ‘ 𝑋 ) , ( 2nd ‘ 𝑋 ) 〉 ) → ( 𝑋 ∈ 𝐴 ↔ 〈 ( 1st ‘ 𝑋 ) , ( 2nd ‘ 𝑋 ) 〉 ∈ 𝐴 ) ) |
11 |
|
funopfv |
⊢ ( Fun 𝐴 → ( 〈 ( 1st ‘ 𝑋 ) , ( 2nd ‘ 𝑋 ) 〉 ∈ 𝐴 → ( 𝐴 ‘ ( 1st ‘ 𝑋 ) ) = ( 2nd ‘ 𝑋 ) ) ) |
12 |
11
|
adantr |
⊢ ( ( Fun 𝐴 ∧ 𝑋 = 〈 ( 1st ‘ 𝑋 ) , ( 2nd ‘ 𝑋 ) 〉 ) → ( 〈 ( 1st ‘ 𝑋 ) , ( 2nd ‘ 𝑋 ) 〉 ∈ 𝐴 → ( 𝐴 ‘ ( 1st ‘ 𝑋 ) ) = ( 2nd ‘ 𝑋 ) ) ) |
13 |
10 12
|
sylbid |
⊢ ( ( Fun 𝐴 ∧ 𝑋 = 〈 ( 1st ‘ 𝑋 ) , ( 2nd ‘ 𝑋 ) 〉 ) → ( 𝑋 ∈ 𝐴 → ( 𝐴 ‘ ( 1st ‘ 𝑋 ) ) = ( 2nd ‘ 𝑋 ) ) ) |
14 |
13
|
impancom |
⊢ ( ( Fun 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( 𝑋 = 〈 ( 1st ‘ 𝑋 ) , ( 2nd ‘ 𝑋 ) 〉 → ( 𝐴 ‘ ( 1st ‘ 𝑋 ) ) = ( 2nd ‘ 𝑋 ) ) ) |
15 |
14
|
imp |
⊢ ( ( ( Fun 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑋 = 〈 ( 1st ‘ 𝑋 ) , ( 2nd ‘ 𝑋 ) 〉 ) → ( 𝐴 ‘ ( 1st ‘ 𝑋 ) ) = ( 2nd ‘ 𝑋 ) ) |
16 |
15
|
3adant3 |
⊢ ( ( ( Fun 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑋 = 〈 ( 1st ‘ 𝑋 ) , ( 2nd ‘ 𝑋 ) 〉 ∧ 𝐵 ⊆ 𝐴 ) → ( 𝐴 ‘ ( 1st ‘ 𝑋 ) ) = ( 2nd ‘ 𝑋 ) ) |
17 |
16
|
adantr |
⊢ ( ( ( ( Fun 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑋 = 〈 ( 1st ‘ 𝑋 ) , ( 2nd ‘ 𝑋 ) 〉 ∧ 𝐵 ⊆ 𝐴 ) ∧ ( 1st ‘ 𝑋 ) ∈ dom 𝐵 ) → ( 𝐴 ‘ ( 1st ‘ 𝑋 ) ) = ( 2nd ‘ 𝑋 ) ) |
18 |
8 17
|
eqtr3d |
⊢ ( ( ( ( Fun 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑋 = 〈 ( 1st ‘ 𝑋 ) , ( 2nd ‘ 𝑋 ) 〉 ∧ 𝐵 ⊆ 𝐴 ) ∧ ( 1st ‘ 𝑋 ) ∈ dom 𝐵 ) → ( 𝐵 ‘ ( 1st ‘ 𝑋 ) ) = ( 2nd ‘ 𝑋 ) ) |
19 |
|
funss |
⊢ ( 𝐵 ⊆ 𝐴 → ( Fun 𝐴 → Fun 𝐵 ) ) |
20 |
19
|
com12 |
⊢ ( Fun 𝐴 → ( 𝐵 ⊆ 𝐴 → Fun 𝐵 ) ) |
21 |
20
|
adantr |
⊢ ( ( Fun 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( 𝐵 ⊆ 𝐴 → Fun 𝐵 ) ) |
22 |
21
|
imp |
⊢ ( ( ( Fun 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝐵 ⊆ 𝐴 ) → Fun 𝐵 ) |
23 |
22
|
funfnd |
⊢ ( ( ( Fun 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝐵 ⊆ 𝐴 ) → 𝐵 Fn dom 𝐵 ) |
24 |
23
|
3adant2 |
⊢ ( ( ( Fun 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑋 = 〈 ( 1st ‘ 𝑋 ) , ( 2nd ‘ 𝑋 ) 〉 ∧ 𝐵 ⊆ 𝐴 ) → 𝐵 Fn dom 𝐵 ) |
25 |
|
fnopfvb |
⊢ ( ( 𝐵 Fn dom 𝐵 ∧ ( 1st ‘ 𝑋 ) ∈ dom 𝐵 ) → ( ( 𝐵 ‘ ( 1st ‘ 𝑋 ) ) = ( 2nd ‘ 𝑋 ) ↔ 〈 ( 1st ‘ 𝑋 ) , ( 2nd ‘ 𝑋 ) 〉 ∈ 𝐵 ) ) |
26 |
24 25
|
sylan |
⊢ ( ( ( ( Fun 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑋 = 〈 ( 1st ‘ 𝑋 ) , ( 2nd ‘ 𝑋 ) 〉 ∧ 𝐵 ⊆ 𝐴 ) ∧ ( 1st ‘ 𝑋 ) ∈ dom 𝐵 ) → ( ( 𝐵 ‘ ( 1st ‘ 𝑋 ) ) = ( 2nd ‘ 𝑋 ) ↔ 〈 ( 1st ‘ 𝑋 ) , ( 2nd ‘ 𝑋 ) 〉 ∈ 𝐵 ) ) |
27 |
18 26
|
mpbid |
⊢ ( ( ( ( Fun 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑋 = 〈 ( 1st ‘ 𝑋 ) , ( 2nd ‘ 𝑋 ) 〉 ∧ 𝐵 ⊆ 𝐴 ) ∧ ( 1st ‘ 𝑋 ) ∈ dom 𝐵 ) → 〈 ( 1st ‘ 𝑋 ) , ( 2nd ‘ 𝑋 ) 〉 ∈ 𝐵 ) |
28 |
|
eleq1 |
⊢ ( 𝑋 = 〈 ( 1st ‘ 𝑋 ) , ( 2nd ‘ 𝑋 ) 〉 → ( 𝑋 ∈ 𝐵 ↔ 〈 ( 1st ‘ 𝑋 ) , ( 2nd ‘ 𝑋 ) 〉 ∈ 𝐵 ) ) |
29 |
28
|
3ad2ant2 |
⊢ ( ( ( Fun 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑋 = 〈 ( 1st ‘ 𝑋 ) , ( 2nd ‘ 𝑋 ) 〉 ∧ 𝐵 ⊆ 𝐴 ) → ( 𝑋 ∈ 𝐵 ↔ 〈 ( 1st ‘ 𝑋 ) , ( 2nd ‘ 𝑋 ) 〉 ∈ 𝐵 ) ) |
30 |
29
|
adantr |
⊢ ( ( ( ( Fun 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑋 = 〈 ( 1st ‘ 𝑋 ) , ( 2nd ‘ 𝑋 ) 〉 ∧ 𝐵 ⊆ 𝐴 ) ∧ ( 1st ‘ 𝑋 ) ∈ dom 𝐵 ) → ( 𝑋 ∈ 𝐵 ↔ 〈 ( 1st ‘ 𝑋 ) , ( 2nd ‘ 𝑋 ) 〉 ∈ 𝐵 ) ) |
31 |
27 30
|
mpbird |
⊢ ( ( ( ( Fun 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑋 = 〈 ( 1st ‘ 𝑋 ) , ( 2nd ‘ 𝑋 ) 〉 ∧ 𝐵 ⊆ 𝐴 ) ∧ ( 1st ‘ 𝑋 ) ∈ dom 𝐵 ) → 𝑋 ∈ 𝐵 ) |
32 |
31
|
3exp1 |
⊢ ( ( Fun 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( 𝑋 = 〈 ( 1st ‘ 𝑋 ) , ( 2nd ‘ 𝑋 ) 〉 → ( 𝐵 ⊆ 𝐴 → ( ( 1st ‘ 𝑋 ) ∈ dom 𝐵 → 𝑋 ∈ 𝐵 ) ) ) ) |
33 |
3 32
|
mpd |
⊢ ( ( Fun 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( 𝐵 ⊆ 𝐴 → ( ( 1st ‘ 𝑋 ) ∈ dom 𝐵 → 𝑋 ∈ 𝐵 ) ) ) |
34 |
33
|
ex |
⊢ ( Fun 𝐴 → ( 𝑋 ∈ 𝐴 → ( 𝐵 ⊆ 𝐴 → ( ( 1st ‘ 𝑋 ) ∈ dom 𝐵 → 𝑋 ∈ 𝐵 ) ) ) ) |
35 |
34
|
com23 |
⊢ ( Fun 𝐴 → ( 𝐵 ⊆ 𝐴 → ( 𝑋 ∈ 𝐴 → ( ( 1st ‘ 𝑋 ) ∈ dom 𝐵 → 𝑋 ∈ 𝐵 ) ) ) ) |
36 |
35
|
3imp |
⊢ ( ( Fun 𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( ( 1st ‘ 𝑋 ) ∈ dom 𝐵 → 𝑋 ∈ 𝐵 ) ) |