funtransport

Description: The TransportTo relationship is a function. (Contributed by Scott Fenton, 18-Oct-2013) (Revised by Mario Carneiro, 19-Apr-2014)

		Ref	Expression
	Assertion	funtransport	$⊢ Fun TransportTo$

Proof

Step	Hyp	Ref	Expression
1		reeanv	$⊢ \exists n \in ℕ \exists m \in ℕ (((p \in (𝔼 (n) \times 𝔼 (n)) \land q \in (𝔼 (n) \times 𝔼 (n)) \land 1^{st} (q) \neq 2^{nd} (q)) \land x = (ι r \in 𝔼 (n) \| (2^{nd} (q) Btwn ⟨1^{st} (q), r⟩ \land ⟨2^{nd} (q), r⟩ Cgr p))) \land ((p \in (𝔼 (m) \times 𝔼 (m)) \land q \in (𝔼 (m) \times 𝔼 (m)) \land 1^{st} (q) \neq 2^{nd} (q)) \land y = (ι r \in 𝔼 (m) \| (2^{nd} (q) Btwn ⟨1^{st} (q), r⟩ \land ⟨2^{nd} (q), r⟩ Cgr p)))) \leftrightarrow (\exists n \in ℕ ((p \in (𝔼 (n) \times 𝔼 (n)) \land q \in (𝔼 (n) \times 𝔼 (n)) \land 1^{st} (q) \neq 2^{nd} (q)) \land x = (ι r \in 𝔼 (n) \| (2^{nd} (q) Btwn ⟨1^{st} (q), r⟩ \land ⟨2^{nd} (q), r⟩ Cgr p))) \land \exists m \in ℕ ((p \in (𝔼 (m) \times 𝔼 (m)) \land q \in (𝔼 (m) \times 𝔼 (m)) \land 1^{st} (q) \neq 2^{nd} (q)) \land y = (ι r \in 𝔼 (m) \| (2^{nd} (q) Btwn ⟨1^{st} (q), r⟩ \land ⟨2^{nd} (q), r⟩ Cgr p))))$
2		simp1	$⊢ (p \in (𝔼 (n) \times 𝔼 (n)) \land q \in (𝔼 (n) \times 𝔼 (n)) \land 1^{st} (q) \neq 2^{nd} (q)) \to p \in (𝔼 (n) \times 𝔼 (n))$
3		simp1	$⊢ (p \in (𝔼 (m) \times 𝔼 (m)) \land q \in (𝔼 (m) \times 𝔼 (m)) \land 1^{st} (q) \neq 2^{nd} (q)) \to p \in (𝔼 (m) \times 𝔼 (m))$
4	2 3	anim12i	$⊢ ((p \in (𝔼 (n) \times 𝔼 (n)) \land q \in (𝔼 (n) \times 𝔼 (n)) \land 1^{st} (q) \neq 2^{nd} (q)) \land (p \in (𝔼 (m) \times 𝔼 (m)) \land q \in (𝔼 (m) \times 𝔼 (m)) \land 1^{st} (q) \neq 2^{nd} (q))) \to (p \in (𝔼 (n) \times 𝔼 (n)) \land p \in (𝔼 (m) \times 𝔼 (m)))$
5	4	anim1i	$⊢ (((p \in (𝔼 (n) \times 𝔼 (n)) \land q \in (𝔼 (n) \times 𝔼 (n)) \land 1^{st} (q) \neq 2^{nd} (q)) \land (p \in (𝔼 (m) \times 𝔼 (m)) \land q \in (𝔼 (m) \times 𝔼 (m)) \land 1^{st} (q) \neq 2^{nd} (q))) \land (x = (ι r \in 𝔼 (n) \| (2^{nd} (q) Btwn ⟨1^{st} (q), r⟩ \land ⟨2^{nd} (q), r⟩ Cgr p)) \land y = (ι r \in 𝔼 (m) \| (2^{nd} (q) Btwn ⟨1^{st} (q), r⟩ \land ⟨2^{nd} (q), r⟩ Cgr p)))) \to ((p \in (𝔼 (n) \times 𝔼 (n)) \land p \in (𝔼 (m) \times 𝔼 (m))) \land (x = (ι r \in 𝔼 (n) \| (2^{nd} (q) Btwn ⟨1^{st} (q), r⟩ \land ⟨2^{nd} (q), r⟩ Cgr p)) \land y = (ι r \in 𝔼 (m) \| (2^{nd} (q) Btwn ⟨1^{st} (q), r⟩ \land ⟨2^{nd} (q), r⟩ Cgr p))))$
6	5	an4s	$⊢ (((p \in (𝔼 (n) \times 𝔼 (n)) \land q \in (𝔼 (n) \times 𝔼 (n)) \land 1^{st} (q) \neq 2^{nd} (q)) \land x = (ι r \in 𝔼 (n) \| (2^{nd} (q) Btwn ⟨1^{st} (q), r⟩ \land ⟨2^{nd} (q), r⟩ Cgr p))) \land ((p \in (𝔼 (m) \times 𝔼 (m)) \land q \in (𝔼 (m) \times 𝔼 (m)) \land 1^{st} (q) \neq 2^{nd} (q)) \land y = (ι r \in 𝔼 (m) \| (2^{nd} (q) Btwn ⟨1^{st} (q), r⟩ \land ⟨2^{nd} (q), r⟩ Cgr p)))) \to ((p \in (𝔼 (n) \times 𝔼 (n)) \land p \in (𝔼 (m) \times 𝔼 (m))) \land (x = (ι r \in 𝔼 (n) \| (2^{nd} (q) Btwn ⟨1^{st} (q), r⟩ \land ⟨2^{nd} (q), r⟩ Cgr p)) \land y = (ι r \in 𝔼 (m) \| (2^{nd} (q) Btwn ⟨1^{st} (q), r⟩ \land ⟨2^{nd} (q), r⟩ Cgr p))))$
7		xp1st	$⊢ p \in (𝔼 (n) \times 𝔼 (n)) \to 1^{st} (p) \in 𝔼 (n)$
8		xp1st	$⊢ p \in (𝔼 (m) \times 𝔼 (m)) \to 1^{st} (p) \in 𝔼 (m)$
9		axdimuniq	$⊢ ((n \in ℕ \land 1^{st} (p) \in 𝔼 (n)) \land (m \in ℕ \land 1^{st} (p) \in 𝔼 (m))) \to n = m$
10		fveq2	$⊢ n = m \to 𝔼 (n) = 𝔼 (m)$
11	10	riotaeqdv	$⊢ n = m \to (ι r \in 𝔼 (n) \| (2^{nd} (q) Btwn ⟨1^{st} (q), r⟩ \land ⟨2^{nd} (q), r⟩ Cgr p)) = (ι r \in 𝔼 (m) \| (2^{nd} (q) Btwn ⟨1^{st} (q), r⟩ \land ⟨2^{nd} (q), r⟩ Cgr p))$
12	11	eqeq2d	$⊢ n = m \to (y = (ι r \in 𝔼 (n) \| (2^{nd} (q) Btwn ⟨1^{st} (q), r⟩ \land ⟨2^{nd} (q), r⟩ Cgr p)) \leftrightarrow y = (ι r \in 𝔼 (m) \| (2^{nd} (q) Btwn ⟨1^{st} (q), r⟩ \land ⟨2^{nd} (q), r⟩ Cgr p)))$
13	12	anbi2d	$⊢ n = m \to ((x = (ι r \in 𝔼 (n) \| (2^{nd} (q) Btwn ⟨1^{st} (q), r⟩ \land ⟨2^{nd} (q), r⟩ Cgr p)) \land y = (ι r \in 𝔼 (n) \| (2^{nd} (q) Btwn ⟨1^{st} (q), r⟩ \land ⟨2^{nd} (q), r⟩ Cgr p))) \leftrightarrow (x = (ι r \in 𝔼 (n) \| (2^{nd} (q) Btwn ⟨1^{st} (q), r⟩ \land ⟨2^{nd} (q), r⟩ Cgr p)) \land y = (ι r \in 𝔼 (m) \| (2^{nd} (q) Btwn ⟨1^{st} (q), r⟩ \land ⟨2^{nd} (q), r⟩ Cgr p))))$
14		eqtr3	$⊢ (x = (ι r \in 𝔼 (n) \| (2^{nd} (q) Btwn ⟨1^{st} (q), r⟩ \land ⟨2^{nd} (q), r⟩ Cgr p)) \land y = (ι r \in 𝔼 (n) \| (2^{nd} (q) Btwn ⟨1^{st} (q), r⟩ \land ⟨2^{nd} (q), r⟩ Cgr p))) \to x = y$
15	13 14	biimtrrdi	$⊢ n = m \to ((x = (ι r \in 𝔼 (n) \| (2^{nd} (q) Btwn ⟨1^{st} (q), r⟩ \land ⟨2^{nd} (q), r⟩ Cgr p)) \land y = (ι r \in 𝔼 (m) \| (2^{nd} (q) Btwn ⟨1^{st} (q), r⟩ \land ⟨2^{nd} (q), r⟩ Cgr p))) \to x = y)$
16	9 15	syl	$⊢ ((n \in ℕ \land 1^{st} (p) \in 𝔼 (n)) \land (m \in ℕ \land 1^{st} (p) \in 𝔼 (m))) \to ((x = (ι r \in 𝔼 (n) \| (2^{nd} (q) Btwn ⟨1^{st} (q), r⟩ \land ⟨2^{nd} (q), r⟩ Cgr p)) \land y = (ι r \in 𝔼 (m) \| (2^{nd} (q) Btwn ⟨1^{st} (q), r⟩ \land ⟨2^{nd} (q), r⟩ Cgr p))) \to x = y)$
17	16	an4s	$⊢ ((n \in ℕ \land m \in ℕ) \land (1^{st} (p) \in 𝔼 (n) \land 1^{st} (p) \in 𝔼 (m))) \to ((x = (ι r \in 𝔼 (n) \| (2^{nd} (q) Btwn ⟨1^{st} (q), r⟩ \land ⟨2^{nd} (q), r⟩ Cgr p)) \land y = (ι r \in 𝔼 (m) \| (2^{nd} (q) Btwn ⟨1^{st} (q), r⟩ \land ⟨2^{nd} (q), r⟩ Cgr p))) \to x = y)$
18	17	ex	$⊢ (n \in ℕ \land m \in ℕ) \to ((1^{st} (p) \in 𝔼 (n) \land 1^{st} (p) \in 𝔼 (m)) \to ((x = (ι r \in 𝔼 (n) \| (2^{nd} (q) Btwn ⟨1^{st} (q), r⟩ \land ⟨2^{nd} (q), r⟩ Cgr p)) \land y = (ι r \in 𝔼 (m) \| (2^{nd} (q) Btwn ⟨1^{st} (q), r⟩ \land ⟨2^{nd} (q), r⟩ Cgr p))) \to x = y))$
19	7 8 18	syl2ani	$⊢ (n \in ℕ \land m \in ℕ) \to ((p \in (𝔼 (n) \times 𝔼 (n)) \land p \in (𝔼 (m) \times 𝔼 (m))) \to ((x = (ι r \in 𝔼 (n) \| (2^{nd} (q) Btwn ⟨1^{st} (q), r⟩ \land ⟨2^{nd} (q), r⟩ Cgr p)) \land y = (ι r \in 𝔼 (m) \| (2^{nd} (q) Btwn ⟨1^{st} (q), r⟩ \land ⟨2^{nd} (q), r⟩ Cgr p))) \to x = y))$
20	19	impd	$⊢ (n \in ℕ \land m \in ℕ) \to (((p \in (𝔼 (n) \times 𝔼 (n)) \land p \in (𝔼 (m) \times 𝔼 (m))) \land (x = (ι r \in 𝔼 (n) \| (2^{nd} (q) Btwn ⟨1^{st} (q), r⟩ \land ⟨2^{nd} (q), r⟩ Cgr p)) \land y = (ι r \in 𝔼 (m) \| (2^{nd} (q) Btwn ⟨1^{st} (q), r⟩ \land ⟨2^{nd} (q), r⟩ Cgr p)))) \to x = y)$
21	6 20	syl5	$⊢ (n \in ℕ \land m \in ℕ) \to ((((p \in (𝔼 (n) \times 𝔼 (n)) \land q \in (𝔼 (n) \times 𝔼 (n)) \land 1^{st} (q) \neq 2^{nd} (q)) \land x = (ι r \in 𝔼 (n) \| (2^{nd} (q) Btwn ⟨1^{st} (q), r⟩ \land ⟨2^{nd} (q), r⟩ Cgr p))) \land ((p \in (𝔼 (m) \times 𝔼 (m)) \land q \in (𝔼 (m) \times 𝔼 (m)) \land 1^{st} (q) \neq 2^{nd} (q)) \land y = (ι r \in 𝔼 (m) \| (2^{nd} (q) Btwn ⟨1^{st} (q), r⟩ \land ⟨2^{nd} (q), r⟩ Cgr p)))) \to x = y)$
22	21	rexlimivv	$⊢ \exists n \in ℕ \exists m \in ℕ (((p \in (𝔼 (n) \times 𝔼 (n)) \land q \in (𝔼 (n) \times 𝔼 (n)) \land 1^{st} (q) \neq 2^{nd} (q)) \land x = (ι r \in 𝔼 (n) \| (2^{nd} (q) Btwn ⟨1^{st} (q), r⟩ \land ⟨2^{nd} (q), r⟩ Cgr p))) \land ((p \in (𝔼 (m) \times 𝔼 (m)) \land q \in (𝔼 (m) \times 𝔼 (m)) \land 1^{st} (q) \neq 2^{nd} (q)) \land y = (ι r \in 𝔼 (m) \| (2^{nd} (q) Btwn ⟨1^{st} (q), r⟩ \land ⟨2^{nd} (q), r⟩ Cgr p)))) \to x = y$
23	1 22	sylbir	$⊢ (\exists n \in ℕ ((p \in (𝔼 (n) \times 𝔼 (n)) \land q \in (𝔼 (n) \times 𝔼 (n)) \land 1^{st} (q) \neq 2^{nd} (q)) \land x = (ι r \in 𝔼 (n) \| (2^{nd} (q) Btwn ⟨1^{st} (q), r⟩ \land ⟨2^{nd} (q), r⟩ Cgr p))) \land \exists m \in ℕ ((p \in (𝔼 (m) \times 𝔼 (m)) \land q \in (𝔼 (m) \times 𝔼 (m)) \land 1^{st} (q) \neq 2^{nd} (q)) \land y = (ι r \in 𝔼 (m) \| (2^{nd} (q) Btwn ⟨1^{st} (q), r⟩ \land ⟨2^{nd} (q), r⟩ Cgr p)))) \to x = y$
24	23	gen2	$⊢ \forall x \forall y ((\exists n \in ℕ ((p \in (𝔼 (n) \times 𝔼 (n)) \land q \in (𝔼 (n) \times 𝔼 (n)) \land 1^{st} (q) \neq 2^{nd} (q)) \land x = (ι r \in 𝔼 (n) \| (2^{nd} (q) Btwn ⟨1^{st} (q), r⟩ \land ⟨2^{nd} (q), r⟩ Cgr p))) \land \exists m \in ℕ ((p \in (𝔼 (m) \times 𝔼 (m)) \land q \in (𝔼 (m) \times 𝔼 (m)) \land 1^{st} (q) \neq 2^{nd} (q)) \land y = (ι r \in 𝔼 (m) \| (2^{nd} (q) Btwn ⟨1^{st} (q), r⟩ \land ⟨2^{nd} (q), r⟩ Cgr p)))) \to x = y)$
25		eqeq1	$⊢ x = y \to (x = (ι r \in 𝔼 (n) \| (2^{nd} (q) Btwn ⟨1^{st} (q), r⟩ \land ⟨2^{nd} (q), r⟩ Cgr p)) \leftrightarrow y = (ι r \in 𝔼 (n) \| (2^{nd} (q) Btwn ⟨1^{st} (q), r⟩ \land ⟨2^{nd} (q), r⟩ Cgr p)))$
26	25	anbi2d	$⊢ x = y \to (((p \in (𝔼 (n) \times 𝔼 (n)) \land q \in (𝔼 (n) \times 𝔼 (n)) \land 1^{st} (q) \neq 2^{nd} (q)) \land x = (ι r \in 𝔼 (n) \| (2^{nd} (q) Btwn ⟨1^{st} (q), r⟩ \land ⟨2^{nd} (q), r⟩ Cgr p))) \leftrightarrow ((p \in (𝔼 (n) \times 𝔼 (n)) \land q \in (𝔼 (n) \times 𝔼 (n)) \land 1^{st} (q) \neq 2^{nd} (q)) \land y = (ι r \in 𝔼 (n) \| (2^{nd} (q) Btwn ⟨1^{st} (q), r⟩ \land ⟨2^{nd} (q), r⟩ Cgr p))))$
27	26	rexbidv	$⊢ x = y \to (\exists n \in ℕ ((p \in (𝔼 (n) \times 𝔼 (n)) \land q \in (𝔼 (n) \times 𝔼 (n)) \land 1^{st} (q) \neq 2^{nd} (q)) \land x = (ι r \in 𝔼 (n) \| (2^{nd} (q) Btwn ⟨1^{st} (q), r⟩ \land ⟨2^{nd} (q), r⟩ Cgr p))) \leftrightarrow \exists n \in ℕ ((p \in (𝔼 (n) \times 𝔼 (n)) \land q \in (𝔼 (n) \times 𝔼 (n)) \land 1^{st} (q) \neq 2^{nd} (q)) \land y = (ι r \in 𝔼 (n) \| (2^{nd} (q) Btwn ⟨1^{st} (q), r⟩ \land ⟨2^{nd} (q), r⟩ Cgr p))))$
28	10	sqxpeqd	$⊢ n = m \to 𝔼 (n) \times 𝔼 (n) = 𝔼 (m) \times 𝔼 (m)$
29	28	eleq2d	$⊢ n = m \to (p \in (𝔼 (n) \times 𝔼 (n)) \leftrightarrow p \in (𝔼 (m) \times 𝔼 (m)))$
30	28	eleq2d	$⊢ n = m \to (q \in (𝔼 (n) \times 𝔼 (n)) \leftrightarrow q \in (𝔼 (m) \times 𝔼 (m)))$
31	29 30	3anbi12d	$⊢ n = m \to ((p \in (𝔼 (n) \times 𝔼 (n)) \land q \in (𝔼 (n) \times 𝔼 (n)) \land 1^{st} (q) \neq 2^{nd} (q)) \leftrightarrow (p \in (𝔼 (m) \times 𝔼 (m)) \land q \in (𝔼 (m) \times 𝔼 (m)) \land 1^{st} (q) \neq 2^{nd} (q)))$
32	31 12	anbi12d	$⊢ n = m \to (((p \in (𝔼 (n) \times 𝔼 (n)) \land q \in (𝔼 (n) \times 𝔼 (n)) \land 1^{st} (q) \neq 2^{nd} (q)) \land y = (ι r \in 𝔼 (n) \| (2^{nd} (q) Btwn ⟨1^{st} (q), r⟩ \land ⟨2^{nd} (q), r⟩ Cgr p))) \leftrightarrow ((p \in (𝔼 (m) \times 𝔼 (m)) \land q \in (𝔼 (m) \times 𝔼 (m)) \land 1^{st} (q) \neq 2^{nd} (q)) \land y = (ι r \in 𝔼 (m) \| (2^{nd} (q) Btwn ⟨1^{st} (q), r⟩ \land ⟨2^{nd} (q), r⟩ Cgr p))))$
33	32	cbvrexvw	$⊢ \exists n \in ℕ ((p \in (𝔼 (n) \times 𝔼 (n)) \land q \in (𝔼 (n) \times 𝔼 (n)) \land 1^{st} (q) \neq 2^{nd} (q)) \land y = (ι r \in 𝔼 (n) \| (2^{nd} (q) Btwn ⟨1^{st} (q), r⟩ \land ⟨2^{nd} (q), r⟩ Cgr p))) \leftrightarrow \exists m \in ℕ ((p \in (𝔼 (m) \times 𝔼 (m)) \land q \in (𝔼 (m) \times 𝔼 (m)) \land 1^{st} (q) \neq 2^{nd} (q)) \land y = (ι r \in 𝔼 (m) \| (2^{nd} (q) Btwn ⟨1^{st} (q), r⟩ \land ⟨2^{nd} (q), r⟩ Cgr p)))$
34	27 33	bitrdi	$⊢ x = y \to (\exists n \in ℕ ((p \in (𝔼 (n) \times 𝔼 (n)) \land q \in (𝔼 (n) \times 𝔼 (n)) \land 1^{st} (q) \neq 2^{nd} (q)) \land x = (ι r \in 𝔼 (n) \| (2^{nd} (q) Btwn ⟨1^{st} (q), r⟩ \land ⟨2^{nd} (q), r⟩ Cgr p))) \leftrightarrow \exists m \in ℕ ((p \in (𝔼 (m) \times 𝔼 (m)) \land q \in (𝔼 (m) \times 𝔼 (m)) \land 1^{st} (q) \neq 2^{nd} (q)) \land y = (ι r \in 𝔼 (m) \| (2^{nd} (q) Btwn ⟨1^{st} (q), r⟩ \land ⟨2^{nd} (q), r⟩ Cgr p))))$
35	34	mo4	$⊢ \exists^{*} x \exists n \in ℕ ((p \in (𝔼 (n) \times 𝔼 (n)) \land q \in (𝔼 (n) \times 𝔼 (n)) \land 1^{st} (q) \neq 2^{nd} (q)) \land x = (ι r \in 𝔼 (n) \| (2^{nd} (q) Btwn ⟨1^{st} (q), r⟩ \land ⟨2^{nd} (q), r⟩ Cgr p))) \leftrightarrow \forall x \forall y ((\exists n \in ℕ ((p \in (𝔼 (n) \times 𝔼 (n)) \land q \in (𝔼 (n) \times 𝔼 (n)) \land 1^{st} (q) \neq 2^{nd} (q)) \land x = (ι r \in 𝔼 (n) \| (2^{nd} (q) Btwn ⟨1^{st} (q), r⟩ \land ⟨2^{nd} (q), r⟩ Cgr p))) \land \exists m \in ℕ ((p \in (𝔼 (m) \times 𝔼 (m)) \land q \in (𝔼 (m) \times 𝔼 (m)) \land 1^{st} (q) \neq 2^{nd} (q)) \land y = (ι r \in 𝔼 (m) \| (2^{nd} (q) Btwn ⟨1^{st} (q), r⟩ \land ⟨2^{nd} (q), r⟩ Cgr p)))) \to x = y)$
36	24 35	mpbir	$⊢ \exists^{*} x \exists n \in ℕ ((p \in (𝔼 (n) \times 𝔼 (n)) \land q \in (𝔼 (n) \times 𝔼 (n)) \land 1^{st} (q) \neq 2^{nd} (q)) \land x = (ι r \in 𝔼 (n) \| (2^{nd} (q) Btwn ⟨1^{st} (q), r⟩ \land ⟨2^{nd} (q), r⟩ Cgr p)))$
37	36	funoprab	$⊢ Fun \{⟨⟨p, q⟩, x⟩ \| \exists n \in ℕ ((p \in (𝔼 (n) \times 𝔼 (n)) \land q \in (𝔼 (n) \times 𝔼 (n)) \land 1^{st} (q) \neq 2^{nd} (q)) \land x = (ι r \in 𝔼 (n) \| (2^{nd} (q) Btwn ⟨1^{st} (q), r⟩ \land ⟨2^{nd} (q), r⟩ Cgr p)))\}$
38		df-transport	$⊢ TransportTo = \{⟨⟨p, q⟩, x⟩ \| \exists n \in ℕ ((p \in (𝔼 (n) \times 𝔼 (n)) \land q \in (𝔼 (n) \times 𝔼 (n)) \land 1^{st} (q) \neq 2^{nd} (q)) \land x = (ι r \in 𝔼 (n) \| (2^{nd} (q) Btwn ⟨1^{st} (q), r⟩ \land ⟨2^{nd} (q), r⟩ Cgr p)))\}$
39	38	funeqi	$⊢ Fun TransportTo \leftrightarrow Fun \{⟨⟨p, q⟩, x⟩ \| \exists n \in ℕ ((p \in (𝔼 (n) \times 𝔼 (n)) \land q \in (𝔼 (n) \times 𝔼 (n)) \land 1^{st} (q) \neq 2^{nd} (q)) \land x = (ι r \in 𝔼 (n) \| (2^{nd} (q) Btwn ⟨1^{st} (q), r⟩ \land ⟨2^{nd} (q), r⟩ Cgr p)))\}$
40	37 39	mpbir	$⊢ Fun TransportTo$

Metamath Proof Explorer

Theorem funtransport

Proof