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 ({I ↾}_{A}) \leftrightarrow (B \in (A \times A) \land 1^{st} (B) = 2^{nd} (B))$

Proof

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

Metamath Proof Explorer

Theorem bj-elid6

Proof