opswap

Description: Swap the members of an ordered pair. (Contributed by NM, 14-Dec-2008) (Revised by Mario Carneiro, 30-Aug-2015)

		Ref	Expression
	Assertion	opswap	$⊢ ⋃ {\{⟨A, B⟩\}}^{-1} = ⟨B, A⟩$

Step	Hyp	Ref	Expression
1		cnvsng	$⊢ (A \in V \land B \in V) \to {\{⟨A, B⟩\}}^{-1} = \{⟨B, A⟩\}$
2	1	unieqd	$⊢ (A \in V \land B \in V) \to ⋃ {\{⟨A, B⟩\}}^{-1} = ⋃ \{⟨B, A⟩\}$
3		opex	$⊢ ⟨B, A⟩ \in V$
4	3	unisn	$⊢ ⋃ \{⟨B, A⟩\} = ⟨B, A⟩$
5	2 4	eqtrdi	$⊢ (A \in V \land B \in V) \to ⋃ {\{⟨A, B⟩\}}^{-1} = ⟨B, A⟩$
6		uni0	$⊢ ⋃ \emptyset = \emptyset$
7		opprc	$⊢ \neg (A \in V \land B \in V) \to ⟨A, B⟩ = \emptyset$
8	7	sneqd	$⊢ \neg (A \in V \land B \in V) \to \{⟨A, B⟩\} = \{\emptyset\}$
9	8	cnveqd	$⊢ \neg (A \in V \land B \in V) \to {\{⟨A, B⟩\}}^{-1} = {\{\emptyset\}}^{-1}$
10		cnvsn0	$⊢ {\{\emptyset\}}^{-1} = \emptyset$
11	9 10	eqtrdi	$⊢ \neg (A \in V \land B \in V) \to {\{⟨A, B⟩\}}^{-1} = \emptyset$
12	11	unieqd	$⊢ \neg (A \in V \land B \in V) \to ⋃ {\{⟨A, B⟩\}}^{-1} = ⋃ \emptyset$
13		ancom	$⊢ (A \in V \land B \in V) \leftrightarrow (B \in V \land A \in V)$
14		opprc	$⊢ \neg (B \in V \land A \in V) \to ⟨B, A⟩ = \emptyset$
15	13 14	sylnbi	$⊢ \neg (A \in V \land B \in V) \to ⟨B, A⟩ = \emptyset$
16	6 12 15	3eqtr4a	$⊢ \neg (A \in V \land B \in V) \to ⋃ {\{⟨A, B⟩\}}^{-1} = ⟨B, A⟩$
17	5 16	pm2.61i	$⊢ ⋃ {\{⟨A, B⟩\}}^{-1} = ⟨B, A⟩$

Metamath Proof Explorer