rntpos

Description: The range of tpos F when dom F is a relation. (Contributed by Mario Carneiro, 10-Sep-2015)

		Ref	Expression
	Assertion	rntpos	$⊢ Rel dom F \to ran tpos F = ran F$

Proof

Step	Hyp	Ref	Expression
1		vex	$⊢ z \in V$
2	1	elrn	$⊢ z \in ran tpos F \leftrightarrow \exists w w tpos F z$
3		vex	$⊢ w \in V$
4	3 1	breldm	$⊢ w tpos F z \to w \in dom tpos F$
5		dmtpos	$⊢ Rel dom F \to dom tpos F = {dom F}^{-1}$
6	5	eleq2d	$⊢ Rel dom F \to (w \in dom tpos F \leftrightarrow w \in {dom F}^{-1})$
7	4 6	imbitrid	$⊢ Rel dom F \to (w tpos F z \to w \in {dom F}^{-1})$
8		relcnv	$⊢ Rel {dom F}^{-1}$
9		elrel	$⊢ (Rel {dom F}^{-1} \land w \in {dom F}^{-1}) \to \exists x \exists y w = ⟨x, y⟩$
10	8 9	mpan	$⊢ w \in {dom F}^{-1} \to \exists x \exists y w = ⟨x, y⟩$
11	7 10	syl6	$⊢ Rel dom F \to (w tpos F z \to \exists x \exists y w = ⟨x, y⟩)$
12		breq1	$⊢ w = ⟨x, y⟩ \to (w tpos F z \leftrightarrow ⟨x, y⟩ tpos F z)$
13		brtpos	$⊢ z \in V \to (⟨x, y⟩ tpos F z \leftrightarrow ⟨y, x⟩ F z)$
14	13	elv	$⊢ ⟨x, y⟩ tpos F z \leftrightarrow ⟨y, x⟩ F z$
15	12 14	bitrdi	$⊢ w = ⟨x, y⟩ \to (w tpos F z \leftrightarrow ⟨y, x⟩ F z)$
16		opex	$⊢ ⟨y, x⟩ \in V$
17	16 1	brelrn	$⊢ ⟨y, x⟩ F z \to z \in ran F$
18	15 17	biimtrdi	$⊢ w = ⟨x, y⟩ \to (w tpos F z \to z \in ran F)$
19	18	exlimivv	$⊢ \exists x \exists y w = ⟨x, y⟩ \to (w tpos F z \to z \in ran F)$
20	11 19	syli	$⊢ Rel dom F \to (w tpos F z \to z \in ran F)$
21	20	exlimdv	$⊢ Rel dom F \to (\exists w w tpos F z \to z \in ran F)$
22	2 21	biimtrid	$⊢ Rel dom F \to (z \in ran tpos F \to z \in ran F)$
23	1	elrn	$⊢ z \in ran F \leftrightarrow \exists w w F z$
24	3 1	breldm	$⊢ w F z \to w \in dom F$
25		elrel	$⊢ (Rel dom F \land w \in dom F) \to \exists y \exists x w = ⟨y, x⟩$
26	25	ex	$⊢ Rel dom F \to (w \in dom F \to \exists y \exists x w = ⟨y, x⟩)$
27	24 26	syl5	$⊢ Rel dom F \to (w F z \to \exists y \exists x w = ⟨y, x⟩)$
28		breq1	$⊢ w = ⟨y, x⟩ \to (w F z \leftrightarrow ⟨y, x⟩ F z)$
29	28 14	bitr4di	$⊢ w = ⟨y, x⟩ \to (w F z \leftrightarrow ⟨x, y⟩ tpos F z)$
30		opex	$⊢ ⟨x, y⟩ \in V$
31	30 1	brelrn	$⊢ ⟨x, y⟩ tpos F z \to z \in ran tpos F$
32	29 31	biimtrdi	$⊢ w = ⟨y, x⟩ \to (w F z \to z \in ran tpos F)$
33	32	exlimivv	$⊢ \exists y \exists x w = ⟨y, x⟩ \to (w F z \to z \in ran tpos F)$
34	27 33	syli	$⊢ Rel dom F \to (w F z \to z \in ran tpos F)$
35	34	exlimdv	$⊢ Rel dom F \to (\exists w w F z \to z \in ran tpos F)$
36	23 35	biimtrid	$⊢ Rel dom F \to (z \in ran F \to z \in ran tpos F)$
37	22 36	impbid	$⊢ Rel dom F \to (z \in ran tpos F \leftrightarrow z \in ran F)$
38	37	eqrdv	$⊢ Rel dom F \to ran tpos F = ran F$

Metamath Proof Explorer

Theorem rntpos

Proof