# Metamath Proof Explorer

## Theorem bj-elid6

Description: Characterization of the elements of the diagonal of a Cartesian square. (Contributed by BJ, 22-Jun-2019)

Ref Expression
Assertion bj-elid6 ${⊢}{B}\in \left({\mathrm{I}↾}_{{A}}\right)↔\left({B}\in \left({A}×{A}\right)\wedge {1}^{st}\left({B}\right)={2}^{nd}\left({B}\right)\right)$

### Proof

Step Hyp Ref Expression
1 df-res ${⊢}{\mathrm{I}↾}_{{A}}=\mathrm{I}\cap \left({A}×\mathrm{V}\right)$
2 1 elin2 ${⊢}{B}\in \left({\mathrm{I}↾}_{{A}}\right)↔\left({B}\in \mathrm{I}\wedge {B}\in \left({A}×\mathrm{V}\right)\right)$
3 2 biancomi ${⊢}{B}\in \left({\mathrm{I}↾}_{{A}}\right)↔\left({B}\in \left({A}×\mathrm{V}\right)\wedge {B}\in \mathrm{I}\right)$
4 bj-elid4 ${⊢}{B}\in \left({A}×\mathrm{V}\right)\to \left({B}\in \mathrm{I}↔{1}^{st}\left({B}\right)={2}^{nd}\left({B}\right)\right)$
5 4 pm5.32i ${⊢}\left({B}\in \left({A}×\mathrm{V}\right)\wedge {B}\in \mathrm{I}\right)↔\left({B}\in \left({A}×\mathrm{V}\right)\wedge {1}^{st}\left({B}\right)={2}^{nd}\left({B}\right)\right)$
6 1st2nd2 ${⊢}{B}\in \left({A}×\mathrm{V}\right)\to {B}=⟨{1}^{st}\left({B}\right),{2}^{nd}\left({B}\right)⟩$
7 6 pm4.71ri ${⊢}{B}\in \left({A}×\mathrm{V}\right)↔\left({B}=⟨{1}^{st}\left({B}\right),{2}^{nd}\left({B}\right)⟩\wedge {B}\in \left({A}×\mathrm{V}\right)\right)$
8 eleq1 ${⊢}{B}=⟨{1}^{st}\left({B}\right),{2}^{nd}\left({B}\right)⟩\to \left({B}\in \left({A}×\mathrm{V}\right)↔⟨{1}^{st}\left({B}\right),{2}^{nd}\left({B}\right)⟩\in \left({A}×\mathrm{V}\right)\right)$
9 8 adantl ${⊢}\left({1}^{st}\left({B}\right)={2}^{nd}\left({B}\right)\wedge {B}=⟨{1}^{st}\left({B}\right),{2}^{nd}\left({B}\right)⟩\right)\to \left({B}\in \left({A}×\mathrm{V}\right)↔⟨{1}^{st}\left({B}\right),{2}^{nd}\left({B}\right)⟩\in \left({A}×\mathrm{V}\right)\right)$
10 simpl ${⊢}\left({1}^{st}\left({B}\right)\in {A}\wedge {2}^{nd}\left({B}\right)\in \mathrm{V}\right)\to {1}^{st}\left({B}\right)\in {A}$
11 10 a1i ${⊢}{1}^{st}\left({B}\right)={2}^{nd}\left({B}\right)\to \left(\left({1}^{st}\left({B}\right)\in {A}\wedge {2}^{nd}\left({B}\right)\in \mathrm{V}\right)\to {1}^{st}\left({B}\right)\in {A}\right)$
12 eleq1 ${⊢}{1}^{st}\left({B}\right)={2}^{nd}\left({B}\right)\to \left({1}^{st}\left({B}\right)\in {A}↔{2}^{nd}\left({B}\right)\in {A}\right)$
13 10 12 syl5ib ${⊢}{1}^{st}\left({B}\right)={2}^{nd}\left({B}\right)\to \left(\left({1}^{st}\left({B}\right)\in {A}\wedge {2}^{nd}\left({B}\right)\in \mathrm{V}\right)\to {2}^{nd}\left({B}\right)\in {A}\right)$
14 11 13 jcad ${⊢}{1}^{st}\left({B}\right)={2}^{nd}\left({B}\right)\to \left(\left({1}^{st}\left({B}\right)\in {A}\wedge {2}^{nd}\left({B}\right)\in \mathrm{V}\right)\to \left({1}^{st}\left({B}\right)\in {A}\wedge {2}^{nd}\left({B}\right)\in {A}\right)\right)$
15 elex ${⊢}{2}^{nd}\left({B}\right)\in {A}\to {2}^{nd}\left({B}\right)\in \mathrm{V}$
16 15 anim2i ${⊢}\left({1}^{st}\left({B}\right)\in {A}\wedge {2}^{nd}\left({B}\right)\in {A}\right)\to \left({1}^{st}\left({B}\right)\in {A}\wedge {2}^{nd}\left({B}\right)\in \mathrm{V}\right)$
17 14 16 impbid1 ${⊢}{1}^{st}\left({B}\right)={2}^{nd}\left({B}\right)\to \left(\left({1}^{st}\left({B}\right)\in {A}\wedge {2}^{nd}\left({B}\right)\in \mathrm{V}\right)↔\left({1}^{st}\left({B}\right)\in {A}\wedge {2}^{nd}\left({B}\right)\in {A}\right)\right)$
18 17 adantr ${⊢}\left({1}^{st}\left({B}\right)={2}^{nd}\left({B}\right)\wedge {B}=⟨{1}^{st}\left({B}\right),{2}^{nd}\left({B}\right)⟩\right)\to \left(\left({1}^{st}\left({B}\right)\in {A}\wedge {2}^{nd}\left({B}\right)\in \mathrm{V}\right)↔\left({1}^{st}\left({B}\right)\in {A}\wedge {2}^{nd}\left({B}\right)\in {A}\right)\right)$
19 opelxp ${⊢}⟨{1}^{st}\left({B}\right),{2}^{nd}\left({B}\right)⟩\in \left({A}×\mathrm{V}\right)↔\left({1}^{st}\left({B}\right)\in {A}\wedge {2}^{nd}\left({B}\right)\in \mathrm{V}\right)$
20 opelxp ${⊢}⟨{1}^{st}\left({B}\right),{2}^{nd}\left({B}\right)⟩\in \left({A}×{A}\right)↔\left({1}^{st}\left({B}\right)\in {A}\wedge {2}^{nd}\left({B}\right)\in {A}\right)$
21 18 19 20 3bitr4g ${⊢}\left({1}^{st}\left({B}\right)={2}^{nd}\left({B}\right)\wedge {B}=⟨{1}^{st}\left({B}\right),{2}^{nd}\left({B}\right)⟩\right)\to \left(⟨{1}^{st}\left({B}\right),{2}^{nd}\left({B}\right)⟩\in \left({A}×\mathrm{V}\right)↔⟨{1}^{st}\left({B}\right),{2}^{nd}\left({B}\right)⟩\in \left({A}×{A}\right)\right)$
22 eleq1 ${⊢}{B}=⟨{1}^{st}\left({B}\right),{2}^{nd}\left({B}\right)⟩\to \left({B}\in \left({A}×{A}\right)↔⟨{1}^{st}\left({B}\right),{2}^{nd}\left({B}\right)⟩\in \left({A}×{A}\right)\right)$
23 22 bicomd ${⊢}{B}=⟨{1}^{st}\left({B}\right),{2}^{nd}\left({B}\right)⟩\to \left(⟨{1}^{st}\left({B}\right),{2}^{nd}\left({B}\right)⟩\in \left({A}×{A}\right)↔{B}\in \left({A}×{A}\right)\right)$
24 23 adantl ${⊢}\left({1}^{st}\left({B}\right)={2}^{nd}\left({B}\right)\wedge {B}=⟨{1}^{st}\left({B}\right),{2}^{nd}\left({B}\right)⟩\right)\to \left(⟨{1}^{st}\left({B}\right),{2}^{nd}\left({B}\right)⟩\in \left({A}×{A}\right)↔{B}\in \left({A}×{A}\right)\right)$
25 9 21 24 3bitrd ${⊢}\left({1}^{st}\left({B}\right)={2}^{nd}\left({B}\right)\wedge {B}=⟨{1}^{st}\left({B}\right),{2}^{nd}\left({B}\right)⟩\right)\to \left({B}\in \left({A}×\mathrm{V}\right)↔{B}\in \left({A}×{A}\right)\right)$
26 25 pm5.32da ${⊢}{1}^{st}\left({B}\right)={2}^{nd}\left({B}\right)\to \left(\left({B}=⟨{1}^{st}\left({B}\right),{2}^{nd}\left({B}\right)⟩\wedge {B}\in \left({A}×\mathrm{V}\right)\right)↔\left({B}=⟨{1}^{st}\left({B}\right),{2}^{nd}\left({B}\right)⟩\wedge {B}\in \left({A}×{A}\right)\right)\right)$
27 simpr ${⊢}\left({B}=⟨{1}^{st}\left({B}\right),{2}^{nd}\left({B}\right)⟩\wedge {B}\in \left({A}×{A}\right)\right)\to {B}\in \left({A}×{A}\right)$
28 1st2nd2 ${⊢}{B}\in \left({A}×{A}\right)\to {B}=⟨{1}^{st}\left({B}\right),{2}^{nd}\left({B}\right)⟩$
29 28 ancri ${⊢}{B}\in \left({A}×{A}\right)\to \left({B}=⟨{1}^{st}\left({B}\right),{2}^{nd}\left({B}\right)⟩\wedge {B}\in \left({A}×{A}\right)\right)$
30 27 29 impbii ${⊢}\left({B}=⟨{1}^{st}\left({B}\right),{2}^{nd}\left({B}\right)⟩\wedge {B}\in \left({A}×{A}\right)\right)↔{B}\in \left({A}×{A}\right)$
31 26 30 syl6bb ${⊢}{1}^{st}\left({B}\right)={2}^{nd}\left({B}\right)\to \left(\left({B}=⟨{1}^{st}\left({B}\right),{2}^{nd}\left({B}\right)⟩\wedge {B}\in \left({A}×\mathrm{V}\right)\right)↔{B}\in \left({A}×{A}\right)\right)$
32 7 31 syl5bb ${⊢}{1}^{st}\left({B}\right)={2}^{nd}\left({B}\right)\to \left({B}\in \left({A}×\mathrm{V}\right)↔{B}\in \left({A}×{A}\right)\right)$
33 32 pm5.32ri ${⊢}\left({B}\in \left({A}×\mathrm{V}\right)\wedge {1}^{st}\left({B}\right)={2}^{nd}\left({B}\right)\right)↔\left({B}\in \left({A}×{A}\right)\wedge {1}^{st}\left({B}\right)={2}^{nd}\left({B}\right)\right)$
34 3 5 33 3bitri ${⊢}{B}\in \left({\mathrm{I}↾}_{{A}}\right)↔\left({B}\in \left({A}×{A}\right)\wedge {1}^{st}\left({B}\right)={2}^{nd}\left({B}\right)\right)$