xpdifcnvepel

Description: The set of couples in a Cartesian product, where the second is not an element of the first. (Contributed by Thierry Arnoux, 17-Jun-2026)

		Ref	Expression
	Assertion	xpdifcnvepel	$⊢ ⋃_{x \in A} (\{x\} \times (B ∖ x)) = (A \times B) ∖ E^{-1}$

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) ∖ E^{-1}) \leftrightarrow (⟨i, j⟩ \in (A \times B) \land \neg ⟨i, j⟩ \in E^{-1})$
9		opelxp	$⊢ ⟨i, j⟩ \in (A \times B) \leftrightarrow (i \in A \land j \in B)$
10		vex	$⊢ i \in V$
11		vex	$⊢ j \in V$
12	10 11	brcnv	$⊢ i E^{-1} j \leftrightarrow j E i$
13		df-br	$⊢ i E^{-1} j \leftrightarrow ⟨i, j⟩ \in E^{-1}$
14		epel	$⊢ j E i \leftrightarrow j \in i$
15	12 13 14	3bitr3i	$⊢ ⟨i, j⟩ \in E^{-1} \leftrightarrow j \in i$
16	15	notbii	$⊢ \neg ⟨i, j⟩ \in E^{-1} \leftrightarrow \neg j \in i$
17	9 16	anbi12i	$⊢ (⟨i, j⟩ \in (A \times B) \land \neg ⟨i, j⟩ \in E^{-1}) \leftrightarrow ((i \in A \land j \in B) \land \neg j \in i)$
18	8 17	bitri	$⊢ ⟨i, j⟩ \in ((A \times B) ∖ E^{-1}) \leftrightarrow ((i \in A \land j \in B) \land \neg j \in i)$
19	18	anbi2i	$⊢ (p = ⟨i, j⟩ \land ⟨i, j⟩ \in ((A \times B) ∖ E^{-1})) \leftrightarrow (p = ⟨i, j⟩ \land ((i \in A \land j \in B) \land \neg j \in i))$
20	19	2exbii	$⊢ \exists i \exists j (p = ⟨i, j⟩ \land ⟨i, j⟩ \in ((A \times B) ∖ E^{-1})) \leftrightarrow \exists i \exists j (p = ⟨i, j⟩ \land ((i \in A \land j \in B) \land \neg j \in i))$
21		eldifi	$⊢ p \in ((A \times B) ∖ E^{-1}) \to p \in (A \times B)$
22		elxpi	$⊢ p \in (A \times B) \to \exists i \exists j (p = ⟨i, j⟩ \land (i \in A \land j \in B))$
23		simpl	$⊢ (p = ⟨i, j⟩ \land (i \in A \land j \in B)) \to p = ⟨i, j⟩$
24	23	2eximi	$⊢ \exists i \exists j (p = ⟨i, j⟩ \land (i \in A \land j \in B)) \to \exists i \exists j p = ⟨i, j⟩$
25	21 22 24	3syl	$⊢ p \in ((A \times B) ∖ E^{-1}) \to \exists i \exists j p = ⟨i, j⟩$
26	25	ancli	$⊢ p \in ((A \times B) ∖ E^{-1}) \to (p \in ((A \times B) ∖ E^{-1}) \land \exists i \exists j p = ⟨i, j⟩)$
27		19.42vv	$⊢ \exists i \exists j (p \in ((A \times B) ∖ E^{-1}) \land p = ⟨i, j⟩) \leftrightarrow (p \in ((A \times B) ∖ E^{-1}) \land \exists i \exists j p = ⟨i, j⟩)$
28	26 27	sylibr	$⊢ p \in ((A \times B) ∖ E^{-1}) \to \exists i \exists j (p \in ((A \times B) ∖ E^{-1}) \land p = ⟨i, j⟩)$
29		ancom	$⊢ (p \in ((A \times B) ∖ E^{-1}) \land p = ⟨i, j⟩) \leftrightarrow (p = ⟨i, j⟩ \land p \in ((A \times B) ∖ E^{-1}))$
30		eleq1	$⊢ p = ⟨i, j⟩ \to (p \in ((A \times B) ∖ E^{-1}) \leftrightarrow ⟨i, j⟩ \in ((A \times B) ∖ E^{-1}))$
31	30	adantl	$⊢ (p \in ((A \times B) ∖ E^{-1}) \land p = ⟨i, j⟩) \to (p \in ((A \times B) ∖ E^{-1}) \leftrightarrow ⟨i, j⟩ \in ((A \times B) ∖ E^{-1}))$
32	31	pm5.32da	$⊢ p \in ((A \times B) ∖ E^{-1}) \to ((p = ⟨i, j⟩ \land p \in ((A \times B) ∖ E^{-1})) \leftrightarrow (p = ⟨i, j⟩ \land ⟨i, j⟩ \in ((A \times B) ∖ E^{-1})))$
33	29 32	bitrid	$⊢ p \in ((A \times B) ∖ E^{-1}) \to ((p \in ((A \times B) ∖ E^{-1}) \land p = ⟨i, j⟩) \leftrightarrow (p = ⟨i, j⟩ \land ⟨i, j⟩ \in ((A \times B) ∖ E^{-1})))$
34	33	2exbidv	$⊢ p \in ((A \times B) ∖ E^{-1}) \to (\exists i \exists j (p \in ((A \times B) ∖ E^{-1}) \land p = ⟨i, j⟩) \leftrightarrow \exists i \exists j (p = ⟨i, j⟩ \land ⟨i, j⟩ \in ((A \times B) ∖ E^{-1})))$
35	28 34	mpbid	$⊢ p \in ((A \times B) ∖ E^{-1}) \to \exists i \exists j (p = ⟨i, j⟩ \land ⟨i, j⟩ \in ((A \times B) ∖ E^{-1}))$
36	30	biimpar	$⊢ (p = ⟨i, j⟩ \land ⟨i, j⟩ \in ((A \times B) ∖ E^{-1})) \to p \in ((A \times B) ∖ E^{-1})$
37	36	exlimivv	$⊢ \exists i \exists j (p = ⟨i, j⟩ \land ⟨i, j⟩ \in ((A \times B) ∖ E^{-1})) \to p \in ((A \times B) ∖ E^{-1})$
38	35 37	impbii	$⊢ p \in ((A \times B) ∖ E^{-1}) \leftrightarrow \exists i \exists j (p = ⟨i, j⟩ \land ⟨i, j⟩ \in ((A \times B) ∖ E^{-1}))$
39		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)))$
40		simprl	$⊢ (y \in A \land (i \in \{y\} \land j \in (B ∖ y))) \to i \in \{y\}$
41	40	elsnd	$⊢ (y \in A \land (i \in \{y\} \land j \in (B ∖ y))) \to i = y$
42		simpl	$⊢ (y \in A \land (i \in \{y\} \land j \in (B ∖ y))) \to y \in A$
43	41 42	eqeltrd	$⊢ (y \in A \land (i \in \{y\} \land j \in (B ∖ y))) \to i \in A$
44		simprr	$⊢ (y \in A \land (i \in \{y\} \land j \in (B ∖ y))) \to j \in (B ∖ y)$
45	44	eldifad	$⊢ (y \in A \land (i \in \{y\} \land j \in (B ∖ y))) \to j \in B$
46	44	eldifbd	$⊢ (y \in A \land (i \in \{y\} \land j \in (B ∖ y))) \to \neg j \in y$
47	46 41	neleqtrrd	$⊢ (y \in A \land (i \in \{y\} \land j \in (B ∖ y))) \to \neg j \in i$
48	43 45 47	jca31	$⊢ (y \in A \land (i \in \{y\} \land j \in (B ∖ y))) \to ((i \in A \land j \in B) \land \neg j \in i)$
49	48	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 \neg j \in i)$
50		sneq	$⊢ x = y \to \{x\} = \{y\}$
51	50	eleq2d	$⊢ x = y \to (i \in \{x\} \leftrightarrow i \in \{y\})$
52		difeq2	$⊢ x = y \to B ∖ x = B ∖ y$
53	52	eleq2d	$⊢ x = y \to (j \in (B ∖ x) \leftrightarrow j \in (B ∖ y))$
54	51 53	anbi12d	$⊢ x = y \to ((i \in \{x\} \land j \in (B ∖ x)) \leftrightarrow (i \in \{y\} \land j \in (B ∖ y)))$
55	54	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))$
56	55	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))$
57	49 56	r19.29a	$⊢ \exists x \in A (i \in \{x\} \land j \in (B ∖ x)) \to ((i \in A \land j \in B) \land \neg j \in i)$
58		simpll	$⊢ ((i \in A \land j \in B) \land \neg j \in i) \to i \in A$
59		vsnid	$⊢ i \in \{i\}$
60	59	a1i	$⊢ ((i \in A \land j \in B) \land \neg j \in i) \to i \in \{i\}$
61		simplr	$⊢ ((i \in A \land j \in B) \land \neg j \in i) \to j \in B$
62		simpr	$⊢ ((i \in A \land j \in B) \land \neg j \in i) \to \neg j \in i$
63	61 62	eldifd	$⊢ ((i \in A \land j \in B) \land \neg j \in i) \to j \in (B ∖ i)$
64		sneq	$⊢ x = i \to \{x\} = \{i\}$
65	64	eleq2d	$⊢ x = i \to (i \in \{x\} \leftrightarrow i \in \{i\})$
66		difeq2	$⊢ x = i \to B ∖ x = B ∖ i$
67	66	eleq2d	$⊢ x = i \to (j \in (B ∖ x) \leftrightarrow j \in (B ∖ i))$
68	65 67	anbi12d	$⊢ x = i \to ((i \in \{x\} \land j \in (B ∖ x)) \leftrightarrow (i \in \{i\} \land j \in (B ∖ i)))$
69	68	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))$
70	58 60 63 69	syl12anc	$⊢ ((i \in A \land j \in B) \land \neg j \in i) \to \exists x \in A (i \in \{x\} \land j \in (B ∖ x))$
71	57 70	impbii	$⊢ \exists x \in A (i \in \{x\} \land j \in (B ∖ x)) \leftrightarrow ((i \in A \land j \in B) \land \neg j \in i)$
72	71	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 \neg j \in i))$
73	39 72	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 \neg j \in i))$
74	73	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 \neg j \in i))$
75	20 38 74	3bitr4i	$⊢ p \in ((A \times B) ∖ E^{-1}) \leftrightarrow \exists i \exists j \exists x \in A (p = ⟨i, j⟩ \land (i \in \{x\} \land j \in (B ∖ x)))$
76	6 7 75	3bitr4i	$⊢ p \in ⋃_{x \in A} (\{x\} \times (B ∖ x)) \leftrightarrow p \in ((A \times B) ∖ E^{-1})$
77	76	eqriv	$⊢ ⋃_{x \in A} (\{x\} \times (B ∖ x)) = (A \times B) ∖ E^{-1}$

Metamath Proof Explorer

Theorem xpdifcnvepel

Proof