xpdifid

Description: The set of distinct couples in a Cartesian product. (Contributed by Thierry Arnoux, 25-May-2019)

		Ref	Expression
	Assertion	xpdifid	$⊢ ⋃_{x \in A} (\{x\} \times (B ∖ \{x\})) = (A \times B) ∖ I$

Proof

Step	Hyp	Ref	Expression
1		elxp	$⊢ p \in (\{x\} \times (B ∖ \{x\})) \leftrightarrow \exists i \exists j (p = ⟨i, j⟩ \land (i \in \{x\} \land j \in (B ∖ \{x\})))$
2	1	rexbii	$⊢ \exists x \in A p \in (\{x\} \times (B ∖ \{x\})) \leftrightarrow \exists x \in A \exists i \exists j (p = ⟨i, j⟩ \land (i \in \{x\} \land j \in (B ∖ \{x\})))$
3		rexcom4	$⊢ \exists x \in A \exists i \exists j (p = ⟨i, j⟩ \land (i \in \{x\} \land j \in (B ∖ \{x\}))) \leftrightarrow \exists i \exists x \in A \exists j (p = ⟨i, j⟩ \land (i \in \{x\} \land j \in (B ∖ \{x\})))$
4		rexcom4	$⊢ \exists x \in A \exists j (p = ⟨i, j⟩ \land (i \in \{x\} \land j \in (B ∖ \{x\}))) \leftrightarrow \exists j \exists x \in A (p = ⟨i, j⟩ \land (i \in \{x\} \land j \in (B ∖ \{x\})))$
5	4	exbii	$⊢ \exists i \exists x \in A \exists j (p = ⟨i, j⟩ \land (i \in \{x\} \land j \in (B ∖ \{x\}))) \leftrightarrow \exists i \exists j \exists x \in A (p = ⟨i, j⟩ \land (i \in \{x\} \land j \in (B ∖ \{x\})))$
6	2 3 5	3bitri	$⊢ \exists x \in A p \in (\{x\} \times (B ∖ \{x\})) \leftrightarrow \exists i \exists j \exists x \in A (p = ⟨i, j⟩ \land (i \in \{x\} \land j \in (B ∖ \{x\})))$
7		eliun	$⊢ p \in ⋃_{x \in A} (\{x\} \times (B ∖ \{x\})) \leftrightarrow \exists x \in A p \in (\{x\} \times (B ∖ \{x\}))$
8		eldif	$⊢ ⟨i, j⟩ \in ((A \times B) ∖ I) \leftrightarrow (⟨i, j⟩ \in (A \times B) \land \neg ⟨i, j⟩ \in I)$
9		opelxp	$⊢ ⟨i, j⟩ \in (A \times B) \leftrightarrow (i \in A \land j \in B)$
10		df-br	$⊢ i I j \leftrightarrow ⟨i, j⟩ \in I$
11		vex	$⊢ j \in V$
12	11	ideq	$⊢ i I j \leftrightarrow i = j$
13	10 12	bitr3i	$⊢ ⟨i, j⟩ \in I \leftrightarrow i = j$
14	13	necon3bbii	$⊢ \neg ⟨i, j⟩ \in I \leftrightarrow i \neq j$
15	9 14	anbi12i	$⊢ (⟨i, j⟩ \in (A \times B) \land \neg ⟨i, j⟩ \in I) \leftrightarrow ((i \in A \land j \in B) \land i \neq j)$
16	8 15	bitri	$⊢ ⟨i, j⟩ \in ((A \times B) ∖ I) \leftrightarrow ((i \in A \land j \in B) \land i \neq j)$
17	16	anbi2i	$⊢ (p = ⟨i, j⟩ \land ⟨i, j⟩ \in ((A \times B) ∖ I)) \leftrightarrow (p = ⟨i, j⟩ \land ((i \in A \land j \in B) \land i \neq j))$
18	17	2exbii	$⊢ \exists i \exists j (p = ⟨i, j⟩ \land ⟨i, j⟩ \in ((A \times B) ∖ I)) \leftrightarrow \exists i \exists j (p = ⟨i, j⟩ \land ((i \in A \land j \in B) \land i \neq j))$
19		eldifi	$⊢ p \in ((A \times B) ∖ I) \to p \in (A \times B)$
20		elxpi	$⊢ p \in (A \times B) \to \exists i \exists j (p = ⟨i, j⟩ \land (i \in A \land j \in B))$
21		simpl	$⊢ (p = ⟨i, j⟩ \land (i \in A \land j \in B)) \to p = ⟨i, j⟩$
22	21	2eximi	$⊢ \exists i \exists j (p = ⟨i, j⟩ \land (i \in A \land j \in B)) \to \exists i \exists j p = ⟨i, j⟩$
23	19 20 22	3syl	$⊢ p \in ((A \times B) ∖ I) \to \exists i \exists j p = ⟨i, j⟩$
24	23	ancli	$⊢ p \in ((A \times B) ∖ I) \to (p \in ((A \times B) ∖ I) \land \exists i \exists j p = ⟨i, j⟩)$
25		19.42vv	$⊢ \exists i \exists j (p \in ((A \times B) ∖ I) \land p = ⟨i, j⟩) \leftrightarrow (p \in ((A \times B) ∖ I) \land \exists i \exists j p = ⟨i, j⟩)$
26	24 25	sylibr	$⊢ p \in ((A \times B) ∖ I) \to \exists i \exists j (p \in ((A \times B) ∖ I) \land p = ⟨i, j⟩)$
27		ancom	$⊢ (p \in ((A \times B) ∖ I) \land p = ⟨i, j⟩) \leftrightarrow (p = ⟨i, j⟩ \land p \in ((A \times B) ∖ I))$
28		eleq1	$⊢ p = ⟨i, j⟩ \to (p \in ((A \times B) ∖ I) \leftrightarrow ⟨i, j⟩ \in ((A \times B) ∖ I))$
29	28	adantl	$⊢ (p \in ((A \times B) ∖ I) \land p = ⟨i, j⟩) \to (p \in ((A \times B) ∖ I) \leftrightarrow ⟨i, j⟩ \in ((A \times B) ∖ I))$
30	29	pm5.32da	$⊢ p \in ((A \times B) ∖ I) \to ((p = ⟨i, j⟩ \land p \in ((A \times B) ∖ I)) \leftrightarrow (p = ⟨i, j⟩ \land ⟨i, j⟩ \in ((A \times B) ∖ I)))$
31	27 30	syl5bb	$⊢ p \in ((A \times B) ∖ I) \to ((p \in ((A \times B) ∖ I) \land p = ⟨i, j⟩) \leftrightarrow (p = ⟨i, j⟩ \land ⟨i, j⟩ \in ((A \times B) ∖ I)))$
32	31	2exbidv	$⊢ p \in ((A \times B) ∖ I) \to (\exists i \exists j (p \in ((A \times B) ∖ I) \land p = ⟨i, j⟩) \leftrightarrow \exists i \exists j (p = ⟨i, j⟩ \land ⟨i, j⟩ \in ((A \times B) ∖ I)))$
33	26 32	mpbid	$⊢ p \in ((A \times B) ∖ I) \to \exists i \exists j (p = ⟨i, j⟩ \land ⟨i, j⟩ \in ((A \times B) ∖ I))$
34	28	biimpar	$⊢ (p = ⟨i, j⟩ \land ⟨i, j⟩ \in ((A \times B) ∖ I)) \to p \in ((A \times B) ∖ I)$
35	34	exlimivv	$⊢ \exists i \exists j (p = ⟨i, j⟩ \land ⟨i, j⟩ \in ((A \times B) ∖ I)) \to p \in ((A \times B) ∖ I)$
36	33 35	impbii	$⊢ p \in ((A \times B) ∖ I) \leftrightarrow \exists i \exists j (p = ⟨i, j⟩ \land ⟨i, j⟩ \in ((A \times B) ∖ I))$
37		r19.42v	$⊢ \exists x \in A (p = ⟨i, j⟩ \land (i \in \{x\} \land j \in (B ∖ \{x\}))) \leftrightarrow (p = ⟨i, j⟩ \land \exists x \in A (i \in \{x\} \land j \in (B ∖ \{x\})))$
38		simprl	$⊢ (y \in A \land (i \in \{y\} \land j \in (B ∖ \{y\}))) \to i \in \{y\}$
39		velsn	$⊢ i \in \{y\} \leftrightarrow i = y$
40	38 39	sylib	$⊢ (y \in A \land (i \in \{y\} \land j \in (B ∖ \{y\}))) \to i = y$
41		simpl	$⊢ (y \in A \land (i \in \{y\} \land j \in (B ∖ \{y\}))) \to y \in A$
42	40 41	eqeltrd	$⊢ (y \in A \land (i \in \{y\} \land j \in (B ∖ \{y\}))) \to i \in A$
43		simprr	$⊢ (y \in A \land (i \in \{y\} \land j \in (B ∖ \{y\}))) \to j \in (B ∖ \{y\})$
44	43	eldifad	$⊢ (y \in A \land (i \in \{y\} \land j \in (B ∖ \{y\}))) \to j \in B$
45	43	eldifbd	$⊢ (y \in A \land (i \in \{y\} \land j \in (B ∖ \{y\}))) \to \neg j \in \{y\}$
46		velsn	$⊢ j \in \{y\} \leftrightarrow j = y$
47	46	necon3bbii	$⊢ \neg j \in \{y\} \leftrightarrow j \neq y$
48	45 47	sylib	$⊢ (y \in A \land (i \in \{y\} \land j \in (B ∖ \{y\}))) \to j \neq y$
49	48	necomd	$⊢ (y \in A \land (i \in \{y\} \land j \in (B ∖ \{y\}))) \to y \neq j$
50	40 49	eqnetrd	$⊢ (y \in A \land (i \in \{y\} \land j \in (B ∖ \{y\}))) \to i \neq j$
51	42 44 50	jca31	$⊢ (y \in A \land (i \in \{y\} \land j \in (B ∖ \{y\}))) \to ((i \in A \land j \in B) \land i \neq j)$
52	51	adantll	$⊢ ((\exists x \in A (i \in \{x\} \land j \in (B ∖ \{x\})) \land y \in A) \land (i \in \{y\} \land j \in (B ∖ \{y\}))) \to ((i \in A \land j \in B) \land i \neq j)$
53		sneq	$⊢ x = y \to \{x\} = \{y\}$
54	53	eleq2d	$⊢ x = y \to (i \in \{x\} \leftrightarrow i \in \{y\})$
55	53	difeq2d	$⊢ x = y \to B ∖ \{x\} = B ∖ \{y\}$
56	55	eleq2d	$⊢ x = y \to (j \in (B ∖ \{x\}) \leftrightarrow j \in (B ∖ \{y\}))$
57	54 56	anbi12d	$⊢ x = y \to ((i \in \{x\} \land j \in (B ∖ \{x\})) \leftrightarrow (i \in \{y\} \land j \in (B ∖ \{y\})))$
58	57	cbvrexvw	$⊢ \exists x \in A (i \in \{x\} \land j \in (B ∖ \{x\})) \leftrightarrow \exists y \in A (i \in \{y\} \land j \in (B ∖ \{y\}))$
59	58	biimpi	$⊢ \exists x \in A (i \in \{x\} \land j \in (B ∖ \{x\})) \to \exists y \in A (i \in \{y\} \land j \in (B ∖ \{y\}))$
60	52 59	r19.29a	$⊢ \exists x \in A (i \in \{x\} \land j \in (B ∖ \{x\})) \to ((i \in A \land j \in B) \land i \neq j)$
61		simpll	$⊢ ((i \in A \land j \in B) \land i \neq j) \to i \in A$
62		vsnid	$⊢ i \in \{i\}$
63	62	a1i	$⊢ ((i \in A \land j \in B) \land i \neq j) \to i \in \{i\}$
64		simplr	$⊢ ((i \in A \land j \in B) \land i \neq j) \to j \in B$
65		simpr	$⊢ ((i \in A \land j \in B) \land i \neq j) \to i \neq j$
66	65	necomd	$⊢ ((i \in A \land j \in B) \land i \neq j) \to j \neq i$
67		velsn	$⊢ j \in \{i\} \leftrightarrow j = i$
68	67	necon3bbii	$⊢ \neg j \in \{i\} \leftrightarrow j \neq i$
69	66 68	sylibr	$⊢ ((i \in A \land j \in B) \land i \neq j) \to \neg j \in \{i\}$
70	64 69	eldifd	$⊢ ((i \in A \land j \in B) \land i \neq j) \to j \in (B ∖ \{i\})$
71		sneq	$⊢ x = i \to \{x\} = \{i\}$
72	71	eleq2d	$⊢ x = i \to (i \in \{x\} \leftrightarrow i \in \{i\})$
73	71	difeq2d	$⊢ x = i \to B ∖ \{x\} = B ∖ \{i\}$
74	73	eleq2d	$⊢ x = i \to (j \in (B ∖ \{x\}) \leftrightarrow j \in (B ∖ \{i\}))$
75	72 74	anbi12d	$⊢ x = i \to ((i \in \{x\} \land j \in (B ∖ \{x\})) \leftrightarrow (i \in \{i\} \land j \in (B ∖ \{i\})))$
76	75	rspcev	$⊢ (i \in A \land (i \in \{i\} \land j \in (B ∖ \{i\}))) \to \exists x \in A (i \in \{x\} \land j \in (B ∖ \{x\}))$
77	61 63 70 76	syl12anc	$⊢ ((i \in A \land j \in B) \land i \neq j) \to \exists x \in A (i \in \{x\} \land j \in (B ∖ \{x\}))$
78	60 77	impbii	$⊢ \exists x \in A (i \in \{x\} \land j \in (B ∖ \{x\})) \leftrightarrow ((i \in A \land j \in B) \land i \neq j)$
79	78	anbi2i	$⊢ (p = ⟨i, j⟩ \land \exists x \in A (i \in \{x\} \land j \in (B ∖ \{x\}))) \leftrightarrow (p = ⟨i, j⟩ \land ((i \in A \land j \in B) \land i \neq j))$
80	37 79	bitri	$⊢ \exists x \in A (p = ⟨i, j⟩ \land (i \in \{x\} \land j \in (B ∖ \{x\}))) \leftrightarrow (p = ⟨i, j⟩ \land ((i \in A \land j \in B) \land i \neq j))$
81	80	2exbii	$⊢ \exists i \exists j \exists x \in A (p = ⟨i, j⟩ \land (i \in \{x\} \land j \in (B ∖ \{x\}))) \leftrightarrow \exists i \exists j (p = ⟨i, j⟩ \land ((i \in A \land j \in B) \land i \neq j))$
82	18 36 81	3bitr4i	$⊢ p \in ((A \times B) ∖ I) \leftrightarrow \exists i \exists j \exists x \in A (p = ⟨i, j⟩ \land (i \in \{x\} \land j \in (B ∖ \{x\})))$
83	6 7 82	3bitr4i	$⊢ p \in ⋃_{x \in A} (\{x\} \times (B ∖ \{x\})) \leftrightarrow p \in ((A \times B) ∖ I)$
84	83	eqriv	$⊢ ⋃_{x \in A} (\{x\} \times (B ∖ \{x\})) = (A \times B) ∖ I$

Metamath Proof Explorer

Theorem xpdifid

Proof