Proof of Theorem bj-elid6
Step | Hyp | Ref
| Expression |
1 | | df-res 5531 |
. . . 4
⊢ ( I
↾ 𝐴) = ( I ∩
(𝐴 ×
V)) |
2 | 1 | elin2 4124 |
. . 3
⊢ (𝐵 ∈ ( I ↾ 𝐴) ↔ (𝐵 ∈ I ∧ 𝐵 ∈ (𝐴 × V))) |
3 | 2 | biancomi 466 |
. 2
⊢ (𝐵 ∈ ( I ↾ 𝐴) ↔ (𝐵 ∈ (𝐴 × V) ∧ 𝐵 ∈ I )) |
4 | | bj-elid4 34583 |
. . 3
⊢ (𝐵 ∈ (𝐴 × V) → (𝐵 ∈ I ↔ (1st
‘𝐵) = (2nd
‘𝐵))) |
5 | 4 | pm5.32i 578 |
. 2
⊢ ((𝐵 ∈ (𝐴 × V) ∧ 𝐵 ∈ I ) ↔ (𝐵 ∈ (𝐴 × V) ∧ (1st
‘𝐵) = (2nd
‘𝐵))) |
6 | | 1st2nd2 7710 |
. . . . 5
⊢ (𝐵 ∈ (𝐴 × V) → 𝐵 = 〈(1st ‘𝐵), (2nd ‘𝐵)〉) |
7 | 6 | pm4.71ri 564 |
. . . 4
⊢ (𝐵 ∈ (𝐴 × V) ↔ (𝐵 = 〈(1st ‘𝐵), (2nd ‘𝐵)〉 ∧ 𝐵 ∈ (𝐴 × V))) |
8 | | eleq1 2877 |
. . . . . . . 8
⊢ (𝐵 = 〈(1st
‘𝐵), (2nd
‘𝐵)〉 →
(𝐵 ∈ (𝐴 × V) ↔
〈(1st ‘𝐵), (2nd ‘𝐵)〉 ∈ (𝐴 × V))) |
9 | 8 | adantl 485 |
. . . . . . 7
⊢
(((1st ‘𝐵) = (2nd ‘𝐵) ∧ 𝐵 = 〈(1st ‘𝐵), (2nd ‘𝐵)〉) → (𝐵 ∈ (𝐴 × V) ↔ 〈(1st
‘𝐵), (2nd
‘𝐵)〉 ∈
(𝐴 ×
V))) |
10 | | simpl 486 |
. . . . . . . . . . . 12
⊢
(((1st ‘𝐵) ∈ 𝐴 ∧ (2nd ‘𝐵) ∈ V) →
(1st ‘𝐵)
∈ 𝐴) |
11 | 10 | a1i 11 |
. . . . . . . . . . 11
⊢
((1st ‘𝐵) = (2nd ‘𝐵) → (((1st ‘𝐵) ∈ 𝐴 ∧ (2nd ‘𝐵) ∈ V) →
(1st ‘𝐵)
∈ 𝐴)) |
12 | | eleq1 2877 |
. . . . . . . . . . . 12
⊢
((1st ‘𝐵) = (2nd ‘𝐵) → ((1st ‘𝐵) ∈ 𝐴 ↔ (2nd ‘𝐵) ∈ 𝐴)) |
13 | 10, 12 | syl5ib 247 |
. . . . . . . . . . 11
⊢
((1st ‘𝐵) = (2nd ‘𝐵) → (((1st ‘𝐵) ∈ 𝐴 ∧ (2nd ‘𝐵) ∈ V) →
(2nd ‘𝐵)
∈ 𝐴)) |
14 | 11, 13 | jcad 516 |
. . . . . . . . . 10
⊢
((1st ‘𝐵) = (2nd ‘𝐵) → (((1st ‘𝐵) ∈ 𝐴 ∧ (2nd ‘𝐵) ∈ V) →
((1st ‘𝐵)
∈ 𝐴 ∧
(2nd ‘𝐵)
∈ 𝐴))) |
15 | | elex 3459 |
. . . . . . . . . . 11
⊢
((2nd ‘𝐵) ∈ 𝐴 → (2nd ‘𝐵) ∈ V) |
16 | 15 | anim2i 619 |
. . . . . . . . . 10
⊢
(((1st ‘𝐵) ∈ 𝐴 ∧ (2nd ‘𝐵) ∈ 𝐴) → ((1st ‘𝐵) ∈ 𝐴 ∧ (2nd ‘𝐵) ∈ V)) |
17 | 14, 16 | impbid1 228 |
. . . . . . . . 9
⊢
((1st ‘𝐵) = (2nd ‘𝐵) → (((1st ‘𝐵) ∈ 𝐴 ∧ (2nd ‘𝐵) ∈ V) ↔
((1st ‘𝐵)
∈ 𝐴 ∧
(2nd ‘𝐵)
∈ 𝐴))) |
18 | 17 | adantr 484 |
. . . . . . . 8
⊢
(((1st ‘𝐵) = (2nd ‘𝐵) ∧ 𝐵 = 〈(1st ‘𝐵), (2nd ‘𝐵)〉) →
(((1st ‘𝐵)
∈ 𝐴 ∧
(2nd ‘𝐵)
∈ V) ↔ ((1st ‘𝐵) ∈ 𝐴 ∧ (2nd ‘𝐵) ∈ 𝐴))) |
19 | | opelxp 5555 |
. . . . . . . 8
⊢
(〈(1st ‘𝐵), (2nd ‘𝐵)〉 ∈ (𝐴 × V) ↔ ((1st
‘𝐵) ∈ 𝐴 ∧ (2nd
‘𝐵) ∈
V)) |
20 | | opelxp 5555 |
. . . . . . . 8
⊢
(〈(1st ‘𝐵), (2nd ‘𝐵)〉 ∈ (𝐴 × 𝐴) ↔ ((1st ‘𝐵) ∈ 𝐴 ∧ (2nd ‘𝐵) ∈ 𝐴)) |
21 | 18, 19, 20 | 3bitr4g 317 |
. . . . . . 7
⊢
(((1st ‘𝐵) = (2nd ‘𝐵) ∧ 𝐵 = 〈(1st ‘𝐵), (2nd ‘𝐵)〉) →
(〈(1st ‘𝐵), (2nd ‘𝐵)〉 ∈ (𝐴 × V) ↔ 〈(1st
‘𝐵), (2nd
‘𝐵)〉 ∈
(𝐴 × 𝐴))) |
22 | | eleq1 2877 |
. . . . . . . . 9
⊢ (𝐵 = 〈(1st
‘𝐵), (2nd
‘𝐵)〉 →
(𝐵 ∈ (𝐴 × 𝐴) ↔ 〈(1st ‘𝐵), (2nd ‘𝐵)〉 ∈ (𝐴 × 𝐴))) |
23 | 22 | bicomd 226 |
. . . . . . . 8
⊢ (𝐵 = 〈(1st
‘𝐵), (2nd
‘𝐵)〉 →
(〈(1st ‘𝐵), (2nd ‘𝐵)〉 ∈ (𝐴 × 𝐴) ↔ 𝐵 ∈ (𝐴 × 𝐴))) |
24 | 23 | adantl 485 |
. . . . . . 7
⊢
(((1st ‘𝐵) = (2nd ‘𝐵) ∧ 𝐵 = 〈(1st ‘𝐵), (2nd ‘𝐵)〉) →
(〈(1st ‘𝐵), (2nd ‘𝐵)〉 ∈ (𝐴 × 𝐴) ↔ 𝐵 ∈ (𝐴 × 𝐴))) |
25 | 9, 21, 24 | 3bitrd 308 |
. . . . . 6
⊢
(((1st ‘𝐵) = (2nd ‘𝐵) ∧ 𝐵 = 〈(1st ‘𝐵), (2nd ‘𝐵)〉) → (𝐵 ∈ (𝐴 × V) ↔ 𝐵 ∈ (𝐴 × 𝐴))) |
26 | 25 | pm5.32da 582 |
. . . . 5
⊢
((1st ‘𝐵) = (2nd ‘𝐵) → ((𝐵 = 〈(1st ‘𝐵), (2nd ‘𝐵)〉 ∧ 𝐵 ∈ (𝐴 × V)) ↔ (𝐵 = 〈(1st ‘𝐵), (2nd ‘𝐵)〉 ∧ 𝐵 ∈ (𝐴 × 𝐴)))) |
27 | | simpr 488 |
. . . . . 6
⊢ ((𝐵 = 〈(1st
‘𝐵), (2nd
‘𝐵)〉 ∧ 𝐵 ∈ (𝐴 × 𝐴)) → 𝐵 ∈ (𝐴 × 𝐴)) |
28 | | 1st2nd2 7710 |
. . . . . . 7
⊢ (𝐵 ∈ (𝐴 × 𝐴) → 𝐵 = 〈(1st ‘𝐵), (2nd ‘𝐵)〉) |
29 | 28 | ancri 553 |
. . . . . 6
⊢ (𝐵 ∈ (𝐴 × 𝐴) → (𝐵 = 〈(1st ‘𝐵), (2nd ‘𝐵)〉 ∧ 𝐵 ∈ (𝐴 × 𝐴))) |
30 | 27, 29 | impbii 212 |
. . . . 5
⊢ ((𝐵 = 〈(1st
‘𝐵), (2nd
‘𝐵)〉 ∧ 𝐵 ∈ (𝐴 × 𝐴)) ↔ 𝐵 ∈ (𝐴 × 𝐴)) |
31 | 26, 30 | syl6bb 290 |
. . . 4
⊢
((1st ‘𝐵) = (2nd ‘𝐵) → ((𝐵 = 〈(1st ‘𝐵), (2nd ‘𝐵)〉 ∧ 𝐵 ∈ (𝐴 × V)) ↔ 𝐵 ∈ (𝐴 × 𝐴))) |
32 | 7, 31 | syl5bb 286 |
. . 3
⊢
((1st ‘𝐵) = (2nd ‘𝐵) → (𝐵 ∈ (𝐴 × V) ↔ 𝐵 ∈ (𝐴 × 𝐴))) |
33 | 32 | pm5.32ri 579 |
. 2
⊢ ((𝐵 ∈ (𝐴 × V) ∧ (1st
‘𝐵) = (2nd
‘𝐵)) ↔ (𝐵 ∈ (𝐴 × 𝐴) ∧ (1st ‘𝐵) = (2nd ‘𝐵))) |
34 | 3, 5, 33 | 3bitri 300 |
1
⊢ (𝐵 ∈ ( I ↾ 𝐴) ↔ (𝐵 ∈ (𝐴 × 𝐴) ∧ (1st ‘𝐵) = (2nd ‘𝐵))) |