Step |
Hyp |
Ref |
Expression |
1 |
|
df-res |
⊢ ( I ↾ 𝐴 ) = ( I ∩ ( 𝐴 × V ) ) |
2 |
1
|
elin2 |
⊢ ( 𝐵 ∈ ( I ↾ 𝐴 ) ↔ ( 𝐵 ∈ I ∧ 𝐵 ∈ ( 𝐴 × V ) ) ) |
3 |
2
|
biancomi |
⊢ ( 𝐵 ∈ ( I ↾ 𝐴 ) ↔ ( 𝐵 ∈ ( 𝐴 × V ) ∧ 𝐵 ∈ I ) ) |
4 |
|
bj-elid4 |
⊢ ( 𝐵 ∈ ( 𝐴 × V ) → ( 𝐵 ∈ I ↔ ( 1st ‘ 𝐵 ) = ( 2nd ‘ 𝐵 ) ) ) |
5 |
4
|
pm5.32i |
⊢ ( ( 𝐵 ∈ ( 𝐴 × V ) ∧ 𝐵 ∈ I ) ↔ ( 𝐵 ∈ ( 𝐴 × V ) ∧ ( 1st ‘ 𝐵 ) = ( 2nd ‘ 𝐵 ) ) ) |
6 |
|
1st2nd2 |
⊢ ( 𝐵 ∈ ( 𝐴 × V ) → 𝐵 = 〈 ( 1st ‘ 𝐵 ) , ( 2nd ‘ 𝐵 ) 〉 ) |
7 |
6
|
pm4.71ri |
⊢ ( 𝐵 ∈ ( 𝐴 × V ) ↔ ( 𝐵 = 〈 ( 1st ‘ 𝐵 ) , ( 2nd ‘ 𝐵 ) 〉 ∧ 𝐵 ∈ ( 𝐴 × V ) ) ) |
8 |
|
eleq1 |
⊢ ( 𝐵 = 〈 ( 1st ‘ 𝐵 ) , ( 2nd ‘ 𝐵 ) 〉 → ( 𝐵 ∈ ( 𝐴 × V ) ↔ 〈 ( 1st ‘ 𝐵 ) , ( 2nd ‘ 𝐵 ) 〉 ∈ ( 𝐴 × V ) ) ) |
9 |
8
|
adantl |
⊢ ( ( ( 1st ‘ 𝐵 ) = ( 2nd ‘ 𝐵 ) ∧ 𝐵 = 〈 ( 1st ‘ 𝐵 ) , ( 2nd ‘ 𝐵 ) 〉 ) → ( 𝐵 ∈ ( 𝐴 × V ) ↔ 〈 ( 1st ‘ 𝐵 ) , ( 2nd ‘ 𝐵 ) 〉 ∈ ( 𝐴 × V ) ) ) |
10 |
|
simpl |
⊢ ( ( ( 1st ‘ 𝐵 ) ∈ 𝐴 ∧ ( 2nd ‘ 𝐵 ) ∈ V ) → ( 1st ‘ 𝐵 ) ∈ 𝐴 ) |
11 |
10
|
a1i |
⊢ ( ( 1st ‘ 𝐵 ) = ( 2nd ‘ 𝐵 ) → ( ( ( 1st ‘ 𝐵 ) ∈ 𝐴 ∧ ( 2nd ‘ 𝐵 ) ∈ V ) → ( 1st ‘ 𝐵 ) ∈ 𝐴 ) ) |
12 |
|
eleq1 |
⊢ ( ( 1st ‘ 𝐵 ) = ( 2nd ‘ 𝐵 ) → ( ( 1st ‘ 𝐵 ) ∈ 𝐴 ↔ ( 2nd ‘ 𝐵 ) ∈ 𝐴 ) ) |
13 |
10 12
|
syl5ib |
⊢ ( ( 1st ‘ 𝐵 ) = ( 2nd ‘ 𝐵 ) → ( ( ( 1st ‘ 𝐵 ) ∈ 𝐴 ∧ ( 2nd ‘ 𝐵 ) ∈ V ) → ( 2nd ‘ 𝐵 ) ∈ 𝐴 ) ) |
14 |
11 13
|
jcad |
⊢ ( ( 1st ‘ 𝐵 ) = ( 2nd ‘ 𝐵 ) → ( ( ( 1st ‘ 𝐵 ) ∈ 𝐴 ∧ ( 2nd ‘ 𝐵 ) ∈ V ) → ( ( 1st ‘ 𝐵 ) ∈ 𝐴 ∧ ( 2nd ‘ 𝐵 ) ∈ 𝐴 ) ) ) |
15 |
|
elex |
⊢ ( ( 2nd ‘ 𝐵 ) ∈ 𝐴 → ( 2nd ‘ 𝐵 ) ∈ V ) |
16 |
15
|
anim2i |
⊢ ( ( ( 1st ‘ 𝐵 ) ∈ 𝐴 ∧ ( 2nd ‘ 𝐵 ) ∈ 𝐴 ) → ( ( 1st ‘ 𝐵 ) ∈ 𝐴 ∧ ( 2nd ‘ 𝐵 ) ∈ V ) ) |
17 |
14 16
|
impbid1 |
⊢ ( ( 1st ‘ 𝐵 ) = ( 2nd ‘ 𝐵 ) → ( ( ( 1st ‘ 𝐵 ) ∈ 𝐴 ∧ ( 2nd ‘ 𝐵 ) ∈ V ) ↔ ( ( 1st ‘ 𝐵 ) ∈ 𝐴 ∧ ( 2nd ‘ 𝐵 ) ∈ 𝐴 ) ) ) |
18 |
17
|
adantr |
⊢ ( ( ( 1st ‘ 𝐵 ) = ( 2nd ‘ 𝐵 ) ∧ 𝐵 = 〈 ( 1st ‘ 𝐵 ) , ( 2nd ‘ 𝐵 ) 〉 ) → ( ( ( 1st ‘ 𝐵 ) ∈ 𝐴 ∧ ( 2nd ‘ 𝐵 ) ∈ V ) ↔ ( ( 1st ‘ 𝐵 ) ∈ 𝐴 ∧ ( 2nd ‘ 𝐵 ) ∈ 𝐴 ) ) ) |
19 |
|
opelxp |
⊢ ( 〈 ( 1st ‘ 𝐵 ) , ( 2nd ‘ 𝐵 ) 〉 ∈ ( 𝐴 × V ) ↔ ( ( 1st ‘ 𝐵 ) ∈ 𝐴 ∧ ( 2nd ‘ 𝐵 ) ∈ V ) ) |
20 |
|
opelxp |
⊢ ( 〈 ( 1st ‘ 𝐵 ) , ( 2nd ‘ 𝐵 ) 〉 ∈ ( 𝐴 × 𝐴 ) ↔ ( ( 1st ‘ 𝐵 ) ∈ 𝐴 ∧ ( 2nd ‘ 𝐵 ) ∈ 𝐴 ) ) |
21 |
18 19 20
|
3bitr4g |
⊢ ( ( ( 1st ‘ 𝐵 ) = ( 2nd ‘ 𝐵 ) ∧ 𝐵 = 〈 ( 1st ‘ 𝐵 ) , ( 2nd ‘ 𝐵 ) 〉 ) → ( 〈 ( 1st ‘ 𝐵 ) , ( 2nd ‘ 𝐵 ) 〉 ∈ ( 𝐴 × V ) ↔ 〈 ( 1st ‘ 𝐵 ) , ( 2nd ‘ 𝐵 ) 〉 ∈ ( 𝐴 × 𝐴 ) ) ) |
22 |
|
eleq1 |
⊢ ( 𝐵 = 〈 ( 1st ‘ 𝐵 ) , ( 2nd ‘ 𝐵 ) 〉 → ( 𝐵 ∈ ( 𝐴 × 𝐴 ) ↔ 〈 ( 1st ‘ 𝐵 ) , ( 2nd ‘ 𝐵 ) 〉 ∈ ( 𝐴 × 𝐴 ) ) ) |
23 |
22
|
bicomd |
⊢ ( 𝐵 = 〈 ( 1st ‘ 𝐵 ) , ( 2nd ‘ 𝐵 ) 〉 → ( 〈 ( 1st ‘ 𝐵 ) , ( 2nd ‘ 𝐵 ) 〉 ∈ ( 𝐴 × 𝐴 ) ↔ 𝐵 ∈ ( 𝐴 × 𝐴 ) ) ) |
24 |
23
|
adantl |
⊢ ( ( ( 1st ‘ 𝐵 ) = ( 2nd ‘ 𝐵 ) ∧ 𝐵 = 〈 ( 1st ‘ 𝐵 ) , ( 2nd ‘ 𝐵 ) 〉 ) → ( 〈 ( 1st ‘ 𝐵 ) , ( 2nd ‘ 𝐵 ) 〉 ∈ ( 𝐴 × 𝐴 ) ↔ 𝐵 ∈ ( 𝐴 × 𝐴 ) ) ) |
25 |
9 21 24
|
3bitrd |
⊢ ( ( ( 1st ‘ 𝐵 ) = ( 2nd ‘ 𝐵 ) ∧ 𝐵 = 〈 ( 1st ‘ 𝐵 ) , ( 2nd ‘ 𝐵 ) 〉 ) → ( 𝐵 ∈ ( 𝐴 × V ) ↔ 𝐵 ∈ ( 𝐴 × 𝐴 ) ) ) |
26 |
25
|
pm5.32da |
⊢ ( ( 1st ‘ 𝐵 ) = ( 2nd ‘ 𝐵 ) → ( ( 𝐵 = 〈 ( 1st ‘ 𝐵 ) , ( 2nd ‘ 𝐵 ) 〉 ∧ 𝐵 ∈ ( 𝐴 × V ) ) ↔ ( 𝐵 = 〈 ( 1st ‘ 𝐵 ) , ( 2nd ‘ 𝐵 ) 〉 ∧ 𝐵 ∈ ( 𝐴 × 𝐴 ) ) ) ) |
27 |
|
simpr |
⊢ ( ( 𝐵 = 〈 ( 1st ‘ 𝐵 ) , ( 2nd ‘ 𝐵 ) 〉 ∧ 𝐵 ∈ ( 𝐴 × 𝐴 ) ) → 𝐵 ∈ ( 𝐴 × 𝐴 ) ) |
28 |
|
1st2nd2 |
⊢ ( 𝐵 ∈ ( 𝐴 × 𝐴 ) → 𝐵 = 〈 ( 1st ‘ 𝐵 ) , ( 2nd ‘ 𝐵 ) 〉 ) |
29 |
28
|
ancri |
⊢ ( 𝐵 ∈ ( 𝐴 × 𝐴 ) → ( 𝐵 = 〈 ( 1st ‘ 𝐵 ) , ( 2nd ‘ 𝐵 ) 〉 ∧ 𝐵 ∈ ( 𝐴 × 𝐴 ) ) ) |
30 |
27 29
|
impbii |
⊢ ( ( 𝐵 = 〈 ( 1st ‘ 𝐵 ) , ( 2nd ‘ 𝐵 ) 〉 ∧ 𝐵 ∈ ( 𝐴 × 𝐴 ) ) ↔ 𝐵 ∈ ( 𝐴 × 𝐴 ) ) |
31 |
26 30
|
syl6bb |
⊢ ( ( 1st ‘ 𝐵 ) = ( 2nd ‘ 𝐵 ) → ( ( 𝐵 = 〈 ( 1st ‘ 𝐵 ) , ( 2nd ‘ 𝐵 ) 〉 ∧ 𝐵 ∈ ( 𝐴 × V ) ) ↔ 𝐵 ∈ ( 𝐴 × 𝐴 ) ) ) |
32 |
7 31
|
syl5bb |
⊢ ( ( 1st ‘ 𝐵 ) = ( 2nd ‘ 𝐵 ) → ( 𝐵 ∈ ( 𝐴 × V ) ↔ 𝐵 ∈ ( 𝐴 × 𝐴 ) ) ) |
33 |
32
|
pm5.32ri |
⊢ ( ( 𝐵 ∈ ( 𝐴 × V ) ∧ ( 1st ‘ 𝐵 ) = ( 2nd ‘ 𝐵 ) ) ↔ ( 𝐵 ∈ ( 𝐴 × 𝐴 ) ∧ ( 1st ‘ 𝐵 ) = ( 2nd ‘ 𝐵 ) ) ) |
34 |
3 5 33
|
3bitri |
⊢ ( 𝐵 ∈ ( I ↾ 𝐴 ) ↔ ( 𝐵 ∈ ( 𝐴 × 𝐴 ) ∧ ( 1st ‘ 𝐵 ) = ( 2nd ‘ 𝐵 ) ) ) |