tpostpos

Description: Value of the double transposition for a general class F . (Contributed by Mario Carneiro, 16-Sep-2015)

		Ref	Expression
	Assertion	tpostpos	$⊢ tpos tpos F = F \cap (((V \times V) \cup \{\emptyset\}) \times V)$

Proof

Step	Hyp	Ref	Expression
1		reltpos	$⊢ Rel tpos tpos F$
2		relinxp	$⊢ Rel (F \cap (((V \times V) \cup \{\emptyset\}) \times V))$
3		relcnv	$⊢ Rel {dom tpos F}^{-1}$
4		df-rel	$⊢ Rel {dom tpos F}^{-1} \leftrightarrow {dom tpos F}^{-1} \subseteq V \times V$
5	3 4	mpbi	$⊢ {dom tpos F}^{-1} \subseteq V \times V$
6		simpl	$⊢ (w \in {dom tpos F}^{-1} \land ⋃ {\{w\}}^{-1} tpos F z) \to w \in {dom tpos F}^{-1}$
7	5 6	sselid	$⊢ (w \in {dom tpos F}^{-1} \land ⋃ {\{w\}}^{-1} tpos F z) \to w \in (V \times V)$
8		simpr	$⊢ (w F z \land w \in (V \times V)) \to w \in (V \times V)$
9		elvv	$⊢ w \in (V \times V) \leftrightarrow \exists x \exists y w = ⟨x, y⟩$
10		eleq1	$⊢ w = ⟨x, y⟩ \to (w \in {dom tpos F}^{-1} \leftrightarrow ⟨x, y⟩ \in {dom tpos F}^{-1})$
11		vex	$⊢ x \in V$
12		vex	$⊢ y \in V$
13	11 12	opelcnv	$⊢ ⟨x, y⟩ \in {dom tpos F}^{-1} \leftrightarrow ⟨y, x⟩ \in dom tpos F$
14	10 13	bitrdi	$⊢ w = ⟨x, y⟩ \to (w \in {dom tpos F}^{-1} \leftrightarrow ⟨y, x⟩ \in dom tpos F)$
15		sneq	$⊢ w = ⟨x, y⟩ \to \{w\} = \{⟨x, y⟩\}$
16	15	cnveqd	$⊢ w = ⟨x, y⟩ \to {\{w\}}^{-1} = {\{⟨x, y⟩\}}^{-1}$
17	16	unieqd	$⊢ w = ⟨x, y⟩ \to ⋃ {\{w\}}^{-1} = ⋃ {\{⟨x, y⟩\}}^{-1}$
18		opswap	$⊢ ⋃ {\{⟨x, y⟩\}}^{-1} = ⟨y, x⟩$
19	17 18	eqtrdi	$⊢ w = ⟨x, y⟩ \to ⋃ {\{w\}}^{-1} = ⟨y, x⟩$
20	19	breq1d	$⊢ w = ⟨x, y⟩ \to (⋃ {\{w\}}^{-1} tpos F z \leftrightarrow ⟨y, x⟩ tpos F z)$
21	14 20	anbi12d	$⊢ w = ⟨x, y⟩ \to ((w \in {dom tpos F}^{-1} \land ⋃ {\{w\}}^{-1} tpos F z) \leftrightarrow (⟨y, x⟩ \in dom tpos F \land ⟨y, x⟩ tpos F z))$
22		opex	$⊢ ⟨y, x⟩ \in V$
23		vex	$⊢ z \in V$
24	22 23	breldm	$⊢ ⟨y, x⟩ tpos F z \to ⟨y, x⟩ \in dom tpos F$
25	24	pm4.71ri	$⊢ ⟨y, x⟩ tpos F z \leftrightarrow (⟨y, x⟩ \in dom tpos F \land ⟨y, x⟩ tpos F z)$
26		brtpos	$⊢ z \in V \to (⟨y, x⟩ tpos F z \leftrightarrow ⟨x, y⟩ F z)$
27	26	elv	$⊢ ⟨y, x⟩ tpos F z \leftrightarrow ⟨x, y⟩ F z$
28	25 27	bitr3i	$⊢ (⟨y, x⟩ \in dom tpos F \land ⟨y, x⟩ tpos F z) \leftrightarrow ⟨x, y⟩ F z$
29	21 28	bitrdi	$⊢ w = ⟨x, y⟩ \to ((w \in {dom tpos F}^{-1} \land ⋃ {\{w\}}^{-1} tpos F z) \leftrightarrow ⟨x, y⟩ F z)$
30		breq1	$⊢ w = ⟨x, y⟩ \to (w F z \leftrightarrow ⟨x, y⟩ F z)$
31	29 30	bitr4d	$⊢ w = ⟨x, y⟩ \to ((w \in {dom tpos F}^{-1} \land ⋃ {\{w\}}^{-1} tpos F z) \leftrightarrow w F z)$
32	31	exlimivv	$⊢ \exists x \exists y w = ⟨x, y⟩ \to ((w \in {dom tpos F}^{-1} \land ⋃ {\{w\}}^{-1} tpos F z) \leftrightarrow w F z)$
33	9 32	sylbi	$⊢ w \in (V \times V) \to ((w \in {dom tpos F}^{-1} \land ⋃ {\{w\}}^{-1} tpos F z) \leftrightarrow w F z)$
34		iba	$⊢ w \in (V \times V) \to (w F z \leftrightarrow (w F z \land w \in (V \times V)))$
35	33 34	bitrd	$⊢ w \in (V \times V) \to ((w \in {dom tpos F}^{-1} \land ⋃ {\{w\}}^{-1} tpos F z) \leftrightarrow (w F z \land w \in (V \times V)))$
36	7 8 35	pm5.21nii	$⊢ (w \in {dom tpos F}^{-1} \land ⋃ {\{w\}}^{-1} tpos F z) \leftrightarrow (w F z \land w \in (V \times V))$
37		elsni	$⊢ w \in \{\emptyset\} \to w = \emptyset$
38	37	sneqd	$⊢ w \in \{\emptyset\} \to \{w\} = \{\emptyset\}$
39	38	cnveqd	$⊢ w \in \{\emptyset\} \to {\{w\}}^{-1} = {\{\emptyset\}}^{-1}$
40		cnvsn0	$⊢ {\{\emptyset\}}^{-1} = \emptyset$
41	39 40	eqtrdi	$⊢ w \in \{\emptyset\} \to {\{w\}}^{-1} = \emptyset$
42	41	unieqd	$⊢ w \in \{\emptyset\} \to ⋃ {\{w\}}^{-1} = ⋃ \emptyset$
43		uni0	$⊢ ⋃ \emptyset = \emptyset$
44	42 43	eqtrdi	$⊢ w \in \{\emptyset\} \to ⋃ {\{w\}}^{-1} = \emptyset$
45	44	breq1d	$⊢ w \in \{\emptyset\} \to (⋃ {\{w\}}^{-1} tpos F z \leftrightarrow \emptyset tpos F z)$
46		brtpos0	$⊢ z \in V \to (\emptyset tpos F z \leftrightarrow \emptyset F z)$
47	46	elv	$⊢ \emptyset tpos F z \leftrightarrow \emptyset F z$
48	45 47	bitrdi	$⊢ w \in \{\emptyset\} \to (⋃ {\{w\}}^{-1} tpos F z \leftrightarrow \emptyset F z)$
49	37	breq1d	$⊢ w \in \{\emptyset\} \to (w F z \leftrightarrow \emptyset F z)$
50	48 49	bitr4d	$⊢ w \in \{\emptyset\} \to (⋃ {\{w\}}^{-1} tpos F z \leftrightarrow w F z)$
51	50	pm5.32i	$⊢ (w \in \{\emptyset\} \land ⋃ {\{w\}}^{-1} tpos F z) \leftrightarrow (w \in \{\emptyset\} \land w F z)$
52	51	biancomi	$⊢ (w \in \{\emptyset\} \land ⋃ {\{w\}}^{-1} tpos F z) \leftrightarrow (w F z \land w \in \{\emptyset\})$
53	36 52	orbi12i	$⊢ ((w \in {dom tpos F}^{-1} \land ⋃ {\{w\}}^{-1} tpos F z) \lor (w \in \{\emptyset\} \land ⋃ {\{w\}}^{-1} tpos F z)) \leftrightarrow ((w F z \land w \in (V \times V)) \lor (w F z \land w \in \{\emptyset\}))$
54		andir	$⊢ ((w \in {dom tpos F}^{-1} \lor w \in \{\emptyset\}) \land ⋃ {\{w\}}^{-1} tpos F z) \leftrightarrow ((w \in {dom tpos F}^{-1} \land ⋃ {\{w\}}^{-1} tpos F z) \lor (w \in \{\emptyset\} \land ⋃ {\{w\}}^{-1} tpos F z))$
55		andi	$⊢ (w F z \land (w \in (V \times V) \lor w \in \{\emptyset\})) \leftrightarrow ((w F z \land w \in (V \times V)) \lor (w F z \land w \in \{\emptyset\}))$
56	53 54 55	3bitr4i	$⊢ ((w \in {dom tpos F}^{-1} \lor w \in \{\emptyset\}) \land ⋃ {\{w\}}^{-1} tpos F z) \leftrightarrow (w F z \land (w \in (V \times V) \lor w \in \{\emptyset\}))$
57		elun	$⊢ w \in ({dom tpos F}^{-1} \cup \{\emptyset\}) \leftrightarrow (w \in {dom tpos F}^{-1} \lor w \in \{\emptyset\})$
58	57	anbi1i	$⊢ (w \in ({dom tpos F}^{-1} \cup \{\emptyset\}) \land ⋃ {\{w\}}^{-1} tpos F z) \leftrightarrow ((w \in {dom tpos F}^{-1} \lor w \in \{\emptyset\}) \land ⋃ {\{w\}}^{-1} tpos F z)$
59		brxp	$⊢ w (((V \times V) \cup \{\emptyset\}) \times V) z \leftrightarrow (w \in ((V \times V) \cup \{\emptyset\}) \land z \in V)$
60	23 59	mpbiran2	$⊢ w (((V \times V) \cup \{\emptyset\}) \times V) z \leftrightarrow w \in ((V \times V) \cup \{\emptyset\})$
61		elun	$⊢ w \in ((V \times V) \cup \{\emptyset\}) \leftrightarrow (w \in (V \times V) \lor w \in \{\emptyset\})$
62	60 61	bitri	$⊢ w (((V \times V) \cup \{\emptyset\}) \times V) z \leftrightarrow (w \in (V \times V) \lor w \in \{\emptyset\})$
63	62	anbi2i	$⊢ (w F z \land w (((V \times V) \cup \{\emptyset\}) \times V) z) \leftrightarrow (w F z \land (w \in (V \times V) \lor w \in \{\emptyset\}))$
64	56 58 63	3bitr4i	$⊢ (w \in ({dom tpos F}^{-1} \cup \{\emptyset\}) \land ⋃ {\{w\}}^{-1} tpos F z) \leftrightarrow (w F z \land w (((V \times V) \cup \{\emptyset\}) \times V) z)$
65		brtpos2	$⊢ z \in V \to (w tpos tpos F z \leftrightarrow (w \in ({dom tpos F}^{-1} \cup \{\emptyset\}) \land ⋃ {\{w\}}^{-1} tpos F z))$
66	65	elv	$⊢ w tpos tpos F z \leftrightarrow (w \in ({dom tpos F}^{-1} \cup \{\emptyset\}) \land ⋃ {\{w\}}^{-1} tpos F z)$
67		brin	$⊢ w (F \cap (((V \times V) \cup \{\emptyset\}) \times V)) z \leftrightarrow (w F z \land w (((V \times V) \cup \{\emptyset\}) \times V) z)$
68	64 66 67	3bitr4i	$⊢ w tpos tpos F z \leftrightarrow w (F \cap (((V \times V) \cup \{\emptyset\}) \times V)) z$
69	1 2 68	eqbrriv	$⊢ tpos tpos F = F \cap (((V \times V) \cup \{\emptyset\}) \times V)$

Metamath Proof Explorer

Theorem tpostpos

Proof