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 I A B A × A 1 st B = 2 nd B

Proof

Step Hyp Ref Expression
1 df-res I A = I A × V
2 1 elin2 B I A B I B A × V
3 2 biancomi B I A B A × V B I
4 bj-elid4 B A × V B I 1 st B = 2 nd B
5 4 pm5.32i B A × V B I B A × V 1 st B = 2 nd B
6 1st2nd2 B A × V B = 1 st B 2 nd B
7 6 pm4.71ri B A × V B = 1 st B 2 nd B B A × V
8 eleq1 B = 1 st B 2 nd B B A × V 1 st B 2 nd B A × V
9 8 adantl 1 st B = 2 nd B B = 1 st B 2 nd B B A × V 1 st B 2 nd B A × V
10 simpl 1 st B A 2 nd B V 1 st B A
11 10 a1i 1 st B = 2 nd B 1 st B A 2 nd B V 1 st B A
12 eleq1 1 st B = 2 nd B 1 st B A 2 nd B A
13 10 12 syl5ib 1 st B = 2 nd B 1 st B A 2 nd B V 2 nd B A
14 11 13 jcad 1 st B = 2 nd B 1 st B A 2 nd B V 1 st B A 2 nd B A
15 elex 2 nd B A 2 nd B V
16 15 anim2i 1 st B A 2 nd B A 1 st B A 2 nd B V
17 14 16 impbid1 1 st B = 2 nd B 1 st B A 2 nd B V 1 st B A 2 nd B A
18 17 adantr 1 st B = 2 nd B B = 1 st B 2 nd B 1 st B A 2 nd B V 1 st B A 2 nd B A
19 opelxp 1 st B 2 nd B A × V 1 st B A 2 nd B V
20 opelxp 1 st B 2 nd B A × A 1 st B A 2 nd B A
21 18 19 20 3bitr4g 1 st B = 2 nd B B = 1 st B 2 nd B 1 st B 2 nd B A × V 1 st B 2 nd B A × A
22 eleq1 B = 1 st B 2 nd B B A × A 1 st B 2 nd B A × A
23 22 bicomd B = 1 st B 2 nd B 1 st B 2 nd B A × A B A × A
24 23 adantl 1 st B = 2 nd B B = 1 st B 2 nd B 1 st B 2 nd B A × A B A × A
25 9 21 24 3bitrd 1 st B = 2 nd B B = 1 st B 2 nd B B A × V B A × A
26 25 pm5.32da 1 st B = 2 nd B B = 1 st B 2 nd B B A × V B = 1 st B 2 nd B B A × A
27 simpr B = 1 st B 2 nd B B A × A B A × A
28 1st2nd2 B A × A B = 1 st B 2 nd B
29 28 ancri B A × A B = 1 st B 2 nd B B A × A
30 27 29 impbii B = 1 st B 2 nd B B A × A B A × A
31 26 30 bitrdi 1 st B = 2 nd B B = 1 st B 2 nd B B A × V B A × A
32 7 31 syl5bb 1 st B = 2 nd B B A × V B A × A
33 32 pm5.32ri B A × V 1 st B = 2 nd B B A × A 1 st B = 2 nd B
34 3 5 33 3bitri B I A B A × A 1 st B = 2 nd B