dftpos4

Description: Alternate definition of tpos . (Contributed by Mario Carneiro, 4-Oct-2015)

		Ref	Expression
	Assertion	dftpos4	$⊢ tpos F = F \circ (x \in ((V \times V) \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1})$

Proof

Step	Hyp	Ref	Expression
1		df-tpos	$⊢ tpos F = F \circ (x \in ({dom F}^{-1} \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1})$
2		relcnv	$⊢ Rel {dom F}^{-1}$
3		df-rel	$⊢ Rel {dom F}^{-1} \leftrightarrow {dom F}^{-1} \subseteq V \times V$
4	2 3	mpbi	$⊢ {dom F}^{-1} \subseteq V \times V$
5		unss1	$⊢ {dom F}^{-1} \subseteq V \times V \to {dom F}^{-1} \cup \{\emptyset\} \subseteq (V \times V) \cup \{\emptyset\}$
6		resmpt	$⊢ {dom F}^{-1} \cup \{\emptyset\} \subseteq (V \times V) \cup \{\emptyset\} \to {(x \in ((V \times V) \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1}) ↾}_{({dom F}^{-1} \cup \{\emptyset\})} = (x \in ({dom F}^{-1} \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1})$
7	4 5 6	mp2b	$⊢ {(x \in ((V \times V) \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1}) ↾}_{({dom F}^{-1} \cup \{\emptyset\})} = (x \in ({dom F}^{-1} \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1})$
8		resss	$⊢ {(x \in ((V \times V) \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1}) ↾}_{({dom F}^{-1} \cup \{\emptyset\})} \subseteq (x \in ((V \times V) \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1})$
9	7 8	eqsstrri	$⊢ (x \in ({dom F}^{-1} \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1}) \subseteq (x \in ((V \times V) \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1})$
10		coss2	$⊢ (x \in ({dom F}^{-1} \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1}) \subseteq (x \in ((V \times V) \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1}) \to F \circ (x \in ({dom F}^{-1} \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1}) \subseteq F \circ (x \in ((V \times V) \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1})$
11	9 10	ax-mp	$⊢ F \circ (x \in ({dom F}^{-1} \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1}) \subseteq F \circ (x \in ((V \times V) \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1})$
12	1 11	eqsstri	$⊢ tpos F \subseteq F \circ (x \in ((V \times V) \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1})$
13		relco	$⊢ Rel (F \circ (x \in ((V \times V) \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1}))$
14		vex	$⊢ y \in V$
15		vex	$⊢ z \in V$
16	14 15	opelco	$⊢ ⟨y, z⟩ \in (F \circ (x \in ((V \times V) \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1})) \leftrightarrow \exists w (y (x \in ((V \times V) \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1}) w \land w F z)$
17		vex	$⊢ w \in V$
18		eleq1	$⊢ x = y \to (x \in ((V \times V) \cup \{\emptyset\}) \leftrightarrow y \in ((V \times V) \cup \{\emptyset\}))$
19		sneq	$⊢ x = y \to \{x\} = \{y\}$
20	19	cnveqd	$⊢ x = y \to {\{x\}}^{-1} = {\{y\}}^{-1}$
21	20	unieqd	$⊢ x = y \to ⋃ {\{x\}}^{-1} = ⋃ {\{y\}}^{-1}$
22	21	eqeq2d	$⊢ x = y \to (z = ⋃ {\{x\}}^{-1} \leftrightarrow z = ⋃ {\{y\}}^{-1})$
23	18 22	anbi12d	$⊢ x = y \to ((x \in ((V \times V) \cup \{\emptyset\}) \land z = ⋃ {\{x\}}^{-1}) \leftrightarrow (y \in ((V \times V) \cup \{\emptyset\}) \land z = ⋃ {\{y\}}^{-1}))$
24		eqeq1	$⊢ z = w \to (z = ⋃ {\{y\}}^{-1} \leftrightarrow w = ⋃ {\{y\}}^{-1})$
25	24	anbi2d	$⊢ z = w \to ((y \in ((V \times V) \cup \{\emptyset\}) \land z = ⋃ {\{y\}}^{-1}) \leftrightarrow (y \in ((V \times V) \cup \{\emptyset\}) \land w = ⋃ {\{y\}}^{-1}))$
26		df-mpt	$⊢ (x \in ((V \times V) \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1}) = \{⟨x, z⟩ \| (x \in ((V \times V) \cup \{\emptyset\}) \land z = ⋃ {\{x\}}^{-1})\}$
27	14 17 23 25 26	brab	$⊢ y (x \in ((V \times V) \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1}) w \leftrightarrow (y \in ((V \times V) \cup \{\emptyset\}) \land w = ⋃ {\{y\}}^{-1})$
28		simplr	$⊢ ((y \in ((V \times V) \cup \{\emptyset\}) \land w = ⋃ {\{y\}}^{-1}) \land w F z) \to w = ⋃ {\{y\}}^{-1}$
29	17 15	breldm	$⊢ w F z \to w \in dom F$
30	29	adantl	$⊢ ((y \in ((V \times V) \cup \{\emptyset\}) \land w = ⋃ {\{y\}}^{-1}) \land w F z) \to w \in dom F$
31	28 30	eqeltrrd	$⊢ ((y \in ((V \times V) \cup \{\emptyset\}) \land w = ⋃ {\{y\}}^{-1}) \land w F z) \to ⋃ {\{y\}}^{-1} \in dom F$
32		elvv	$⊢ y \in (V \times V) \leftrightarrow \exists z \exists w y = ⟨z, w⟩$
33		opswap	$⊢ ⋃ {\{⟨z, w⟩\}}^{-1} = ⟨w, z⟩$
34	33	eleq1i	$⊢ ⋃ {\{⟨z, w⟩\}}^{-1} \in dom F \leftrightarrow ⟨w, z⟩ \in dom F$
35	15 17	opelcnv	$⊢ ⟨z, w⟩ \in {dom F}^{-1} \leftrightarrow ⟨w, z⟩ \in dom F$
36	34 35	bitr4i	$⊢ ⋃ {\{⟨z, w⟩\}}^{-1} \in dom F \leftrightarrow ⟨z, w⟩ \in {dom F}^{-1}$
37		sneq	$⊢ y = ⟨z, w⟩ \to \{y\} = \{⟨z, w⟩\}$
38	37	cnveqd	$⊢ y = ⟨z, w⟩ \to {\{y\}}^{-1} = {\{⟨z, w⟩\}}^{-1}$
39	38	unieqd	$⊢ y = ⟨z, w⟩ \to ⋃ {\{y\}}^{-1} = ⋃ {\{⟨z, w⟩\}}^{-1}$
40	39	eleq1d	$⊢ y = ⟨z, w⟩ \to (⋃ {\{y\}}^{-1} \in dom F \leftrightarrow ⋃ {\{⟨z, w⟩\}}^{-1} \in dom F)$
41		eleq1	$⊢ y = ⟨z, w⟩ \to (y \in {dom F}^{-1} \leftrightarrow ⟨z, w⟩ \in {dom F}^{-1})$
42	40 41	bibi12d	$⊢ y = ⟨z, w⟩ \to ((⋃ {\{y\}}^{-1} \in dom F \leftrightarrow y \in {dom F}^{-1}) \leftrightarrow (⋃ {\{⟨z, w⟩\}}^{-1} \in dom F \leftrightarrow ⟨z, w⟩ \in {dom F}^{-1}))$
43	36 42	mpbiri	$⊢ y = ⟨z, w⟩ \to (⋃ {\{y\}}^{-1} \in dom F \leftrightarrow y \in {dom F}^{-1})$
44	43	exlimivv	$⊢ \exists z \exists w y = ⟨z, w⟩ \to (⋃ {\{y\}}^{-1} \in dom F \leftrightarrow y \in {dom F}^{-1})$
45	32 44	sylbi	$⊢ y \in (V \times V) \to (⋃ {\{y\}}^{-1} \in dom F \leftrightarrow y \in {dom F}^{-1})$
46	45	biimpcd	$⊢ ⋃ {\{y\}}^{-1} \in dom F \to (y \in (V \times V) \to y \in {dom F}^{-1})$
47		elun1	$⊢ y \in {dom F}^{-1} \to y \in ({dom F}^{-1} \cup \{\emptyset\})$
48	46 47	syl6	$⊢ ⋃ {\{y\}}^{-1} \in dom F \to (y \in (V \times V) \to y \in ({dom F}^{-1} \cup \{\emptyset\}))$
49	31 48	syl	$⊢ ((y \in ((V \times V) \cup \{\emptyset\}) \land w = ⋃ {\{y\}}^{-1}) \land w F z) \to (y \in (V \times V) \to y \in ({dom F}^{-1} \cup \{\emptyset\}))$
50		elun2	$⊢ y \in \{\emptyset\} \to y \in ({dom F}^{-1} \cup \{\emptyset\})$
51	50	a1i	$⊢ ((y \in ((V \times V) \cup \{\emptyset\}) \land w = ⋃ {\{y\}}^{-1}) \land w F z) \to (y \in \{\emptyset\} \to y \in ({dom F}^{-1} \cup \{\emptyset\}))$
52		simpll	$⊢ ((y \in ((V \times V) \cup \{\emptyset\}) \land w = ⋃ {\{y\}}^{-1}) \land w F z) \to y \in ((V \times V) \cup \{\emptyset\})$
53		elun	$⊢ y \in ((V \times V) \cup \{\emptyset\}) \leftrightarrow (y \in (V \times V) \lor y \in \{\emptyset\})$
54	52 53	sylib	$⊢ ((y \in ((V \times V) \cup \{\emptyset\}) \land w = ⋃ {\{y\}}^{-1}) \land w F z) \to (y \in (V \times V) \lor y \in \{\emptyset\})$
55	49 51 54	mpjaod	$⊢ ((y \in ((V \times V) \cup \{\emptyset\}) \land w = ⋃ {\{y\}}^{-1}) \land w F z) \to y \in ({dom F}^{-1} \cup \{\emptyset\})$
56		simpr	$⊢ ((y \in ((V \times V) \cup \{\emptyset\}) \land w = ⋃ {\{y\}}^{-1}) \land w F z) \to w F z$
57	28 56	eqbrtrrd	$⊢ ((y \in ((V \times V) \cup \{\emptyset\}) \land w = ⋃ {\{y\}}^{-1}) \land w F z) \to ⋃ {\{y\}}^{-1} F z$
58	55 57	jca	$⊢ ((y \in ((V \times V) \cup \{\emptyset\}) \land w = ⋃ {\{y\}}^{-1}) \land w F z) \to (y \in ({dom F}^{-1} \cup \{\emptyset\}) \land ⋃ {\{y\}}^{-1} F z)$
59	27 58	sylanb	$⊢ (y (x \in ((V \times V) \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1}) w \land w F z) \to (y \in ({dom F}^{-1} \cup \{\emptyset\}) \land ⋃ {\{y\}}^{-1} F z)$
60		brtpos2	$⊢ z \in V \to (y tpos F z \leftrightarrow (y \in ({dom F}^{-1} \cup \{\emptyset\}) \land ⋃ {\{y\}}^{-1} F z))$
61	15 60	ax-mp	$⊢ y tpos F z \leftrightarrow (y \in ({dom F}^{-1} \cup \{\emptyset\}) \land ⋃ {\{y\}}^{-1} F z)$
62	59 61	sylibr	$⊢ (y (x \in ((V \times V) \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1}) w \land w F z) \to y tpos F z$
63		df-br	$⊢ y tpos F z \leftrightarrow ⟨y, z⟩ \in tpos F$
64	62 63	sylib	$⊢ (y (x \in ((V \times V) \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1}) w \land w F z) \to ⟨y, z⟩ \in tpos F$
65	64	exlimiv	$⊢ \exists w (y (x \in ((V \times V) \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1}) w \land w F z) \to ⟨y, z⟩ \in tpos F$
66	16 65	sylbi	$⊢ ⟨y, z⟩ \in (F \circ (x \in ((V \times V) \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1})) \to ⟨y, z⟩ \in tpos F$
67	13 66	relssi	$⊢ F \circ (x \in ((V \times V) \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1}) \subseteq tpos F$
68	12 67	eqssi	$⊢ tpos F = F \circ (x \in ((V \times V) \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1})$

Metamath Proof Explorer

Theorem dftpos4

Proof