Metamath Proof Explorer

Theorem dftpos5

Description: Alternate definition of tpos . (Contributed by Zhi Wang, 6-Oct-2025)

		Ref	Expression
	Assertion	dftpos5	$⊢ tpos F = F \circ ((x \in {dom F}^{-1} ⟼ ⋃ {\{x\}}^{-1}) \cup \{⟨\emptyset, \emptyset⟩\})$

Proof

Step	Hyp	Ref	Expression
1		df-tpos	$⊢ tpos F = F \circ (x \in ({dom F}^{-1} \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1})$
2		mptun	$⊢ (x \in ({dom F}^{-1} \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1}) = (x \in {dom F}^{-1} ⟼ ⋃ {\{x\}}^{-1}) \cup (x \in \{\emptyset\} ⟼ ⋃ {\{x\}}^{-1})$
3		0ex	$⊢ \emptyset \in V$
4		sneq	$⊢ x = \emptyset \to \{x\} = \{\emptyset\}$
5	4	cnveqd	$⊢ x = \emptyset \to {\{x\}}^{-1} = {\{\emptyset\}}^{-1}$
6	5	unieqd	$⊢ x = \emptyset \to ⋃ {\{x\}}^{-1} = ⋃ {\{\emptyset\}}^{-1}$
7		cnvsn0	$⊢ {\{\emptyset\}}^{-1} = \emptyset$
8	7	unieqi	$⊢ ⋃ {\{\emptyset\}}^{-1} = ⋃ \emptyset$
9		uni0	$⊢ ⋃ \emptyset = \emptyset$
10	8 9	eqtri	$⊢ ⋃ {\{\emptyset\}}^{-1} = \emptyset$
11	6 10	eqtrdi	$⊢ x = \emptyset \to ⋃ {\{x\}}^{-1} = \emptyset$
12	11	fmptsng	$⊢ (\emptyset \in V \land \emptyset \in V) \to \{⟨\emptyset, \emptyset⟩\} = (x \in \{\emptyset\} ⟼ ⋃ {\{x\}}^{-1})$
13	3 3 12	mp2an	$⊢ \{⟨\emptyset, \emptyset⟩\} = (x \in \{\emptyset\} ⟼ ⋃ {\{x\}}^{-1})$
14	13	uneq2i	$⊢ (x \in {dom F}^{-1} ⟼ ⋃ {\{x\}}^{-1}) \cup \{⟨\emptyset, \emptyset⟩\} = (x \in {dom F}^{-1} ⟼ ⋃ {\{x\}}^{-1}) \cup (x \in \{\emptyset\} ⟼ ⋃ {\{x\}}^{-1})$
15	2 14	eqtr4i	$⊢ (x \in ({dom F}^{-1} \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1}) = (x \in {dom F}^{-1} ⟼ ⋃ {\{x\}}^{-1}) \cup \{⟨\emptyset, \emptyset⟩\}$
16	15	coeq2i	$⊢ F \circ (x \in ({dom F}^{-1} \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1}) = F \circ ((x \in {dom F}^{-1} ⟼ ⋃ {\{x\}}^{-1}) \cup \{⟨\emptyset, \emptyset⟩\})$
17	1 16	eqtri	$⊢ tpos F = F \circ ((x \in {dom F}^{-1} ⟼ ⋃ {\{x\}}^{-1}) \cup \{⟨\emptyset, \emptyset⟩\})$