brtpos2

Description: Value of the transposition at an ordered pair <. A , B >. . (Contributed by Mario Carneiro, 10-Sep-2015)

		Ref	Expression
	Assertion	brtpos2	$⊢ B \in V \to (A tpos F B \leftrightarrow (A \in ({dom F}^{-1} \cup \{\emptyset\}) \land ⋃ {\{A\}}^{-1} F B))$

Proof

Step	Hyp	Ref	Expression
1		reltpos	$⊢ Rel tpos F$
2	1	brrelex1i	$⊢ A tpos F B \to A \in V$
3	2	a1i	$⊢ B \in V \to (A tpos F B \to A \in V)$
4		elex	$⊢ A \in ({dom F}^{-1} \cup \{\emptyset\}) \to A \in V$
5	4	adantr	$⊢ (A \in ({dom F}^{-1} \cup \{\emptyset\}) \land ⋃ {\{A\}}^{-1} F B) \to A \in V$
6	5	a1i	$⊢ B \in V \to ((A \in ({dom F}^{-1} \cup \{\emptyset\}) \land ⋃ {\{A\}}^{-1} F B) \to A \in V)$
7		df-tpos	$⊢ tpos F = F \circ (x \in ({dom F}^{-1} \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1})$
8	7	breqi	$⊢ A tpos F B \leftrightarrow A (F \circ (x \in ({dom F}^{-1} \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1})) B$
9		brcog	$⊢ (A \in V \land B \in V) \to (A (F \circ (x \in ({dom F}^{-1} \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1})) B \leftrightarrow \exists y (A (x \in ({dom F}^{-1} \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1}) y \land y F B))$
10	8 9	bitrid	$⊢ (A \in V \land B \in V) \to (A tpos F B \leftrightarrow \exists y (A (x \in ({dom F}^{-1} \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1}) y \land y F B))$
11		funmpt	$⊢ Fun (x \in ({dom F}^{-1} \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1})$
12		funbrfv2b	$⊢ Fun (x \in ({dom F}^{-1} \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1}) \to (A (x \in ({dom F}^{-1} \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1}) y \leftrightarrow (A \in dom (x \in ({dom F}^{-1} \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1}) \land (x \in ({dom F}^{-1} \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1}) (A) = y))$
13	11 12	ax-mp	$⊢ A (x \in ({dom F}^{-1} \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1}) y \leftrightarrow (A \in dom (x \in ({dom F}^{-1} \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1}) \land (x \in ({dom F}^{-1} \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1}) (A) = y)$
14		snex	$⊢ \{x\} \in V$
15	14	cnvex	$⊢ {\{x\}}^{-1} \in V$
16	15	uniex	$⊢ ⋃ {\{x\}}^{-1} \in V$
17		eqid	$⊢ (x \in ({dom F}^{-1} \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1}) = (x \in ({dom F}^{-1} \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1})$
18	16 17	dmmpti	$⊢ dom (x \in ({dom F}^{-1} \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1}) = {dom F}^{-1} \cup \{\emptyset\}$
19	18	eleq2i	$⊢ A \in dom (x \in ({dom F}^{-1} \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1}) \leftrightarrow A \in ({dom F}^{-1} \cup \{\emptyset\})$
20		eqcom	$⊢ (x \in ({dom F}^{-1} \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1}) (A) = y \leftrightarrow y = (x \in ({dom F}^{-1} \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1}) (A)$
21	19 20	anbi12i	$⊢ (A \in dom (x \in ({dom F}^{-1} \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1}) \land (x \in ({dom F}^{-1} \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1}) (A) = y) \leftrightarrow (A \in ({dom F}^{-1} \cup \{\emptyset\}) \land y = (x \in ({dom F}^{-1} \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1}) (A))$
22		sneq	$⊢ x = A \to \{x\} = \{A\}$
23	22	cnveqd	$⊢ x = A \to {\{x\}}^{-1} = {\{A\}}^{-1}$
24	23	unieqd	$⊢ x = A \to ⋃ {\{x\}}^{-1} = ⋃ {\{A\}}^{-1}$
25		snex	$⊢ \{A\} \in V$
26	25	cnvex	$⊢ {\{A\}}^{-1} \in V$
27	26	uniex	$⊢ ⋃ {\{A\}}^{-1} \in V$
28	24 17 27	fvmpt	$⊢ A \in ({dom F}^{-1} \cup \{\emptyset\}) \to (x \in ({dom F}^{-1} \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1}) (A) = ⋃ {\{A\}}^{-1}$
29	28	eqeq2d	$⊢ A \in ({dom F}^{-1} \cup \{\emptyset\}) \to (y = (x \in ({dom F}^{-1} \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1}) (A) \leftrightarrow y = ⋃ {\{A\}}^{-1})$
30	29	pm5.32i	$⊢ (A \in ({dom F}^{-1} \cup \{\emptyset\}) \land y = (x \in ({dom F}^{-1} \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1}) (A)) \leftrightarrow (A \in ({dom F}^{-1} \cup \{\emptyset\}) \land y = ⋃ {\{A\}}^{-1})$
31	21 30	bitri	$⊢ (A \in dom (x \in ({dom F}^{-1} \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1}) \land (x \in ({dom F}^{-1} \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1}) (A) = y) \leftrightarrow (A \in ({dom F}^{-1} \cup \{\emptyset\}) \land y = ⋃ {\{A\}}^{-1})$
32	13 31	bitri	$⊢ A (x \in ({dom F}^{-1} \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1}) y \leftrightarrow (A \in ({dom F}^{-1} \cup \{\emptyset\}) \land y = ⋃ {\{A\}}^{-1})$
33	32	biancomi	$⊢ A (x \in ({dom F}^{-1} \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1}) y \leftrightarrow (y = ⋃ {\{A\}}^{-1} \land A \in ({dom F}^{-1} \cup \{\emptyset\}))$
34	33	anbi1i	$⊢ (A (x \in ({dom F}^{-1} \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1}) y \land y F B) \leftrightarrow ((y = ⋃ {\{A\}}^{-1} \land A \in ({dom F}^{-1} \cup \{\emptyset\})) \land y F B)$
35		anass	$⊢ ((y = ⋃ {\{A\}}^{-1} \land A \in ({dom F}^{-1} \cup \{\emptyset\})) \land y F B) \leftrightarrow (y = ⋃ {\{A\}}^{-1} \land (A \in ({dom F}^{-1} \cup \{\emptyset\}) \land y F B))$
36	34 35	bitri	$⊢ (A (x \in ({dom F}^{-1} \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1}) y \land y F B) \leftrightarrow (y = ⋃ {\{A\}}^{-1} \land (A \in ({dom F}^{-1} \cup \{\emptyset\}) \land y F B))$
37	36	exbii	$⊢ \exists y (A (x \in ({dom F}^{-1} \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1}) y \land y F B) \leftrightarrow \exists y (y = ⋃ {\{A\}}^{-1} \land (A \in ({dom F}^{-1} \cup \{\emptyset\}) \land y F B))$
38		breq1	$⊢ y = ⋃ {\{A\}}^{-1} \to (y F B \leftrightarrow ⋃ {\{A\}}^{-1} F B)$
39	38	anbi2d	$⊢ y = ⋃ {\{A\}}^{-1} \to ((A \in ({dom F}^{-1} \cup \{\emptyset\}) \land y F B) \leftrightarrow (A \in ({dom F}^{-1} \cup \{\emptyset\}) \land ⋃ {\{A\}}^{-1} F B))$
40	27 39	ceqsexv	$⊢ \exists y (y = ⋃ {\{A\}}^{-1} \land (A \in ({dom F}^{-1} \cup \{\emptyset\}) \land y F B)) \leftrightarrow (A \in ({dom F}^{-1} \cup \{\emptyset\}) \land ⋃ {\{A\}}^{-1} F B)$
41	37 40	bitri	$⊢ \exists y (A (x \in ({dom F}^{-1} \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1}) y \land y F B) \leftrightarrow (A \in ({dom F}^{-1} \cup \{\emptyset\}) \land ⋃ {\{A\}}^{-1} F B)$
42	10 41	bitrdi	$⊢ (A \in V \land B \in V) \to (A tpos F B \leftrightarrow (A \in ({dom F}^{-1} \cup \{\emptyset\}) \land ⋃ {\{A\}}^{-1} F B))$
43	42	expcom	$⊢ B \in V \to (A \in V \to (A tpos F B \leftrightarrow (A \in ({dom F}^{-1} \cup \{\emptyset\}) \land ⋃ {\{A\}}^{-1} F B)))$
44	3 6 43	pm5.21ndd	$⊢ B \in V \to (A tpos F B \leftrightarrow (A \in ({dom F}^{-1} \cup \{\emptyset\}) \land ⋃ {\{A\}}^{-1} F B))$

Metamath Proof Explorer

Theorem brtpos2

Proof