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	⊢ ( ∃ 𝑛 ∈ ℕ ∃ 𝑚 ∈ ℕ ( ( ( 𝑝 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ 𝑞 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ ( 1^st ‘ 𝑞 ) ≠ ( 2^nd ‘ 𝑞 ) ) ∧ 𝑥 = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑛 ) ( ( 2^nd ‘ 𝑞 ) Btwn ⟨ ( 1^st ‘ 𝑞 ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ 𝑞 ) , 𝑟 ⟩ Cgr 𝑝 ) ) ) ∧ ( ( 𝑝 ∈ ( ( 𝔼 ‘ 𝑚 ) × ( 𝔼 ‘ 𝑚 ) ) ∧ 𝑞 ∈ ( ( 𝔼 ‘ 𝑚 ) × ( 𝔼 ‘ 𝑚 ) ) ∧ ( 1^st ‘ 𝑞 ) ≠ ( 2^nd ‘ 𝑞 ) ) ∧ 𝑦 = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑚 ) ( ( 2^nd ‘ 𝑞 ) Btwn ⟨ ( 1^st ‘ 𝑞 ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ 𝑞 ) , 𝑟 ⟩ Cgr 𝑝 ) ) ) ) ↔ ( ∃ 𝑛 ∈ ℕ ( ( 𝑝 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ 𝑞 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ ( 1^st ‘ 𝑞 ) ≠ ( 2^nd ‘ 𝑞 ) ) ∧ 𝑥 = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑛 ) ( ( 2^nd ‘ 𝑞 ) Btwn ⟨ ( 1^st ‘ 𝑞 ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ 𝑞 ) , 𝑟 ⟩ Cgr 𝑝 ) ) ) ∧ ∃ 𝑚 ∈ ℕ ( ( 𝑝 ∈ ( ( 𝔼 ‘ 𝑚 ) × ( 𝔼 ‘ 𝑚 ) ) ∧ 𝑞 ∈ ( ( 𝔼 ‘ 𝑚 ) × ( 𝔼 ‘ 𝑚 ) ) ∧ ( 1^st ‘ 𝑞 ) ≠ ( 2^nd ‘ 𝑞 ) ) ∧ 𝑦 = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑚 ) ( ( 2^nd ‘ 𝑞 ) Btwn ⟨ ( 1^st ‘ 𝑞 ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ 𝑞 ) , 𝑟 ⟩ Cgr 𝑝 ) ) ) ) )
2		simp1	⊢ ( ( 𝑝 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ 𝑞 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ ( 1^st ‘ 𝑞 ) ≠ ( 2^nd ‘ 𝑞 ) ) → 𝑝 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) )
3		simp1	⊢ ( ( 𝑝 ∈ ( ( 𝔼 ‘ 𝑚 ) × ( 𝔼 ‘ 𝑚 ) ) ∧ 𝑞 ∈ ( ( 𝔼 ‘ 𝑚 ) × ( 𝔼 ‘ 𝑚 ) ) ∧ ( 1^st ‘ 𝑞 ) ≠ ( 2^nd ‘ 𝑞 ) ) → 𝑝 ∈ ( ( 𝔼 ‘ 𝑚 ) × ( 𝔼 ‘ 𝑚 ) ) )
4	2 3	anim12i	⊢ ( ( ( 𝑝 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ 𝑞 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ ( 1^st ‘ 𝑞 ) ≠ ( 2^nd ‘ 𝑞 ) ) ∧ ( 𝑝 ∈ ( ( 𝔼 ‘ 𝑚 ) × ( 𝔼 ‘ 𝑚 ) ) ∧ 𝑞 ∈ ( ( 𝔼 ‘ 𝑚 ) × ( 𝔼 ‘ 𝑚 ) ) ∧ ( 1^st ‘ 𝑞 ) ≠ ( 2^nd ‘ 𝑞 ) ) ) → ( 𝑝 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ 𝑝 ∈ ( ( 𝔼 ‘ 𝑚 ) × ( 𝔼 ‘ 𝑚 ) ) ) )
5	4	anim1i	⊢ ( ( ( ( 𝑝 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ 𝑞 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ ( 1^st ‘ 𝑞 ) ≠ ( 2^nd ‘ 𝑞 ) ) ∧ ( 𝑝 ∈ ( ( 𝔼 ‘ 𝑚 ) × ( 𝔼 ‘ 𝑚 ) ) ∧ 𝑞 ∈ ( ( 𝔼 ‘ 𝑚 ) × ( 𝔼 ‘ 𝑚 ) ) ∧ ( 1^st ‘ 𝑞 ) ≠ ( 2^nd ‘ 𝑞 ) ) ) ∧ ( 𝑥 = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑛 ) ( ( 2^nd ‘ 𝑞 ) Btwn ⟨ ( 1^st ‘ 𝑞 ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ 𝑞 ) , 𝑟 ⟩ Cgr 𝑝 ) ) ∧ 𝑦 = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑚 ) ( ( 2^nd ‘ 𝑞 ) Btwn ⟨ ( 1^st ‘ 𝑞 ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ 𝑞 ) , 𝑟 ⟩ Cgr 𝑝 ) ) ) ) → ( ( 𝑝 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ 𝑝 ∈ ( ( 𝔼 ‘ 𝑚 ) × ( 𝔼 ‘ 𝑚 ) ) ) ∧ ( 𝑥 = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑛 ) ( ( 2^nd ‘ 𝑞 ) Btwn ⟨ ( 1^st ‘ 𝑞 ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ 𝑞 ) , 𝑟 ⟩ Cgr 𝑝 ) ) ∧ 𝑦 = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑚 ) ( ( 2^nd ‘ 𝑞 ) Btwn ⟨ ( 1^st ‘ 𝑞 ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ 𝑞 ) , 𝑟 ⟩ Cgr 𝑝 ) ) ) ) )
6	5	an4s	⊢ ( ( ( ( 𝑝 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ 𝑞 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ ( 1^st ‘ 𝑞 ) ≠ ( 2^nd ‘ 𝑞 ) ) ∧ 𝑥 = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑛 ) ( ( 2^nd ‘ 𝑞 ) Btwn ⟨ ( 1^st ‘ 𝑞 ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ 𝑞 ) , 𝑟 ⟩ Cgr 𝑝 ) ) ) ∧ ( ( 𝑝 ∈ ( ( 𝔼 ‘ 𝑚 ) × ( 𝔼 ‘ 𝑚 ) ) ∧ 𝑞 ∈ ( ( 𝔼 ‘ 𝑚 ) × ( 𝔼 ‘ 𝑚 ) ) ∧ ( 1^st ‘ 𝑞 ) ≠ ( 2^nd ‘ 𝑞 ) ) ∧ 𝑦 = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑚 ) ( ( 2^nd ‘ 𝑞 ) Btwn ⟨ ( 1^st ‘ 𝑞 ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ 𝑞 ) , 𝑟 ⟩ Cgr 𝑝 ) ) ) ) → ( ( 𝑝 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ 𝑝 ∈ ( ( 𝔼 ‘ 𝑚 ) × ( 𝔼 ‘ 𝑚 ) ) ) ∧ ( 𝑥 = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑛 ) ( ( 2^nd ‘ 𝑞 ) Btwn ⟨ ( 1^st ‘ 𝑞 ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ 𝑞 ) , 𝑟 ⟩ Cgr 𝑝 ) ) ∧ 𝑦 = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑚 ) ( ( 2^nd ‘ 𝑞 ) Btwn ⟨ ( 1^st ‘ 𝑞 ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ 𝑞 ) , 𝑟 ⟩ Cgr 𝑝 ) ) ) ) )
7		xp1st	⊢ ( 𝑝 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) → ( 1^st ‘ 𝑝 ) ∈ ( 𝔼 ‘ 𝑛 ) )
8		xp1st	⊢ ( 𝑝 ∈ ( ( 𝔼 ‘ 𝑚 ) × ( 𝔼 ‘ 𝑚 ) ) → ( 1^st ‘ 𝑝 ) ∈ ( 𝔼 ‘ 𝑚 ) )
9		axdimuniq	⊢ ( ( ( 𝑛 ∈ ℕ ∧ ( 1^st ‘ 𝑝 ) ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝑚 ∈ ℕ ∧ ( 1^st ‘ 𝑝 ) ∈ ( 𝔼 ‘ 𝑚 ) ) ) → 𝑛 = 𝑚 )
10		fveq2	⊢ ( 𝑛 = 𝑚 → ( 𝔼 ‘ 𝑛 ) = ( 𝔼 ‘ 𝑚 ) )
11	10	riotaeqdv	⊢ ( 𝑛 = 𝑚 → ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑛 ) ( ( 2^nd ‘ 𝑞 ) Btwn ⟨ ( 1^st ‘ 𝑞 ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ 𝑞 ) , 𝑟 ⟩ Cgr 𝑝 ) ) = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑚 ) ( ( 2^nd ‘ 𝑞 ) Btwn ⟨ ( 1^st ‘ 𝑞 ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ 𝑞 ) , 𝑟 ⟩ Cgr 𝑝 ) ) )
12	11	eqeq2d	⊢ ( 𝑛 = 𝑚 → ( 𝑦 = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑛 ) ( ( 2^nd ‘ 𝑞 ) Btwn ⟨ ( 1^st ‘ 𝑞 ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ 𝑞 ) , 𝑟 ⟩ Cgr 𝑝 ) ) ↔ 𝑦 = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑚 ) ( ( 2^nd ‘ 𝑞 ) Btwn ⟨ ( 1^st ‘ 𝑞 ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ 𝑞 ) , 𝑟 ⟩ Cgr 𝑝 ) ) ) )
13	12	anbi2d	⊢ ( 𝑛 = 𝑚 → ( ( 𝑥 = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑛 ) ( ( 2^nd ‘ 𝑞 ) Btwn ⟨ ( 1^st ‘ 𝑞 ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ 𝑞 ) , 𝑟 ⟩ Cgr 𝑝 ) ) ∧ 𝑦 = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑛 ) ( ( 2^nd ‘ 𝑞 ) Btwn ⟨ ( 1^st ‘ 𝑞 ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ 𝑞 ) , 𝑟 ⟩ Cgr 𝑝 ) ) ) ↔ ( 𝑥 = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑛 ) ( ( 2^nd ‘ 𝑞 ) Btwn ⟨ ( 1^st ‘ 𝑞 ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ 𝑞 ) , 𝑟 ⟩ Cgr 𝑝 ) ) ∧ 𝑦 = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑚 ) ( ( 2^nd ‘ 𝑞 ) Btwn ⟨ ( 1^st ‘ 𝑞 ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ 𝑞 ) , 𝑟 ⟩ Cgr 𝑝 ) ) ) ) )
14		eqtr3	⊢ ( ( 𝑥 = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑛 ) ( ( 2^nd ‘ 𝑞 ) Btwn ⟨ ( 1^st ‘ 𝑞 ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ 𝑞 ) , 𝑟 ⟩ Cgr 𝑝 ) ) ∧ 𝑦 = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑛 ) ( ( 2^nd ‘ 𝑞 ) Btwn ⟨ ( 1^st ‘ 𝑞 ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ 𝑞 ) , 𝑟 ⟩ Cgr 𝑝 ) ) ) → 𝑥 = 𝑦 )
15	13 14	syl6bir	⊢ ( 𝑛 = 𝑚 → ( ( 𝑥 = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑛 ) ( ( 2^nd ‘ 𝑞 ) Btwn ⟨ ( 1^st ‘ 𝑞 ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ 𝑞 ) , 𝑟 ⟩ Cgr 𝑝 ) ) ∧ 𝑦 = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑚 ) ( ( 2^nd ‘ 𝑞 ) Btwn ⟨ ( 1^st ‘ 𝑞 ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ 𝑞 ) , 𝑟 ⟩ Cgr 𝑝 ) ) ) → 𝑥 = 𝑦 ) )
16	9 15	syl	⊢ ( ( ( 𝑛 ∈ ℕ ∧ ( 1^st ‘ 𝑝 ) ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝑚 ∈ ℕ ∧ ( 1^st ‘ 𝑝 ) ∈ ( 𝔼 ‘ 𝑚 ) ) ) → ( ( 𝑥 = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑛 ) ( ( 2^nd ‘ 𝑞 ) Btwn ⟨ ( 1^st ‘ 𝑞 ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ 𝑞 ) , 𝑟 ⟩ Cgr 𝑝 ) ) ∧ 𝑦 = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑚 ) ( ( 2^nd ‘ 𝑞 ) Btwn ⟨ ( 1^st ‘ 𝑞 ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ 𝑞 ) , 𝑟 ⟩ Cgr 𝑝 ) ) ) → 𝑥 = 𝑦 ) )
17	16	an4s	⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ ) ∧ ( ( 1^st ‘ 𝑝 ) ∈ ( 𝔼 ‘ 𝑛 ) ∧ ( 1^st ‘ 𝑝 ) ∈ ( 𝔼 ‘ 𝑚 ) ) ) → ( ( 𝑥 = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑛 ) ( ( 2^nd ‘ 𝑞 ) Btwn ⟨ ( 1^st ‘ 𝑞 ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ 𝑞 ) , 𝑟 ⟩ Cgr 𝑝 ) ) ∧ 𝑦 = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑚 ) ( ( 2^nd ‘ 𝑞 ) Btwn ⟨ ( 1^st ‘ 𝑞 ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ 𝑞 ) , 𝑟 ⟩ Cgr 𝑝 ) ) ) → 𝑥 = 𝑦 ) )
18	17	ex	⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ ) → ( ( ( 1^st ‘ 𝑝 ) ∈ ( 𝔼 ‘ 𝑛 ) ∧ ( 1^st ‘ 𝑝 ) ∈ ( 𝔼 ‘ 𝑚 ) ) → ( ( 𝑥 = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑛 ) ( ( 2^nd ‘ 𝑞 ) Btwn ⟨ ( 1^st ‘ 𝑞 ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ 𝑞 ) , 𝑟 ⟩ Cgr 𝑝 ) ) ∧ 𝑦 = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑚 ) ( ( 2^nd ‘ 𝑞 ) Btwn ⟨ ( 1^st ‘ 𝑞 ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ 𝑞 ) , 𝑟 ⟩ Cgr 𝑝 ) ) ) → 𝑥 = 𝑦 ) ) )
19	7 8 18	syl2ani	⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ ) → ( ( 𝑝 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ 𝑝 ∈ ( ( 𝔼 ‘ 𝑚 ) × ( 𝔼 ‘ 𝑚 ) ) ) → ( ( 𝑥 = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑛 ) ( ( 2^nd ‘ 𝑞 ) Btwn ⟨ ( 1^st ‘ 𝑞 ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ 𝑞 ) , 𝑟 ⟩ Cgr 𝑝 ) ) ∧ 𝑦 = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑚 ) ( ( 2^nd ‘ 𝑞 ) Btwn ⟨ ( 1^st ‘ 𝑞 ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ 𝑞 ) , 𝑟 ⟩ Cgr 𝑝 ) ) ) → 𝑥 = 𝑦 ) ) )
20	19	impd	⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ ) → ( ( ( 𝑝 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ 𝑝 ∈ ( ( 𝔼 ‘ 𝑚 ) × ( 𝔼 ‘ 𝑚 ) ) ) ∧ ( 𝑥 = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑛 ) ( ( 2^nd ‘ 𝑞 ) Btwn ⟨ ( 1^st ‘ 𝑞 ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ 𝑞 ) , 𝑟 ⟩ Cgr 𝑝 ) ) ∧ 𝑦 = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑚 ) ( ( 2^nd ‘ 𝑞 ) Btwn ⟨ ( 1^st ‘ 𝑞 ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ 𝑞 ) , 𝑟 ⟩ Cgr 𝑝 ) ) ) ) → 𝑥 = 𝑦 ) )
21	6 20	syl5	⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ ) → ( ( ( ( 𝑝 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ 𝑞 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ ( 1^st ‘ 𝑞 ) ≠ ( 2^nd ‘ 𝑞 ) ) ∧ 𝑥 = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑛 ) ( ( 2^nd ‘ 𝑞 ) Btwn ⟨ ( 1^st ‘ 𝑞 ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ 𝑞 ) , 𝑟 ⟩ Cgr 𝑝 ) ) ) ∧ ( ( 𝑝 ∈ ( ( 𝔼 ‘ 𝑚 ) × ( 𝔼 ‘ 𝑚 ) ) ∧ 𝑞 ∈ ( ( 𝔼 ‘ 𝑚 ) × ( 𝔼 ‘ 𝑚 ) ) ∧ ( 1^st ‘ 𝑞 ) ≠ ( 2^nd ‘ 𝑞 ) ) ∧ 𝑦 = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑚 ) ( ( 2^nd ‘ 𝑞 ) Btwn ⟨ ( 1^st ‘ 𝑞 ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ 𝑞 ) , 𝑟 ⟩ Cgr 𝑝 ) ) ) ) → 𝑥 = 𝑦 ) )
22	21	rexlimivv	⊢ ( ∃ 𝑛 ∈ ℕ ∃ 𝑚 ∈ ℕ ( ( ( 𝑝 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ 𝑞 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ ( 1^st ‘ 𝑞 ) ≠ ( 2^nd ‘ 𝑞 ) ) ∧ 𝑥 = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑛 ) ( ( 2^nd ‘ 𝑞 ) Btwn ⟨ ( 1^st ‘ 𝑞 ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ 𝑞 ) , 𝑟 ⟩ Cgr 𝑝 ) ) ) ∧ ( ( 𝑝 ∈ ( ( 𝔼 ‘ 𝑚 ) × ( 𝔼 ‘ 𝑚 ) ) ∧ 𝑞 ∈ ( ( 𝔼 ‘ 𝑚 ) × ( 𝔼 ‘ 𝑚 ) ) ∧ ( 1^st ‘ 𝑞 ) ≠ ( 2^nd ‘ 𝑞 ) ) ∧ 𝑦 = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑚 ) ( ( 2^nd ‘ 𝑞 ) Btwn ⟨ ( 1^st ‘ 𝑞 ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ 𝑞 ) , 𝑟 ⟩ Cgr 𝑝 ) ) ) ) → 𝑥 = 𝑦 )
23	1 22	sylbir	⊢ ( ( ∃ 𝑛 ∈ ℕ ( ( 𝑝 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ 𝑞 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ ( 1^st ‘ 𝑞 ) ≠ ( 2^nd ‘ 𝑞 ) ) ∧ 𝑥 = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑛 ) ( ( 2^nd ‘ 𝑞 ) Btwn ⟨ ( 1^st ‘ 𝑞 ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ 𝑞 ) , 𝑟 ⟩ Cgr 𝑝 ) ) ) ∧ ∃ 𝑚 ∈ ℕ ( ( 𝑝 ∈ ( ( 𝔼 ‘ 𝑚 ) × ( 𝔼 ‘ 𝑚 ) ) ∧ 𝑞 ∈ ( ( 𝔼 ‘ 𝑚 ) × ( 𝔼 ‘ 𝑚 ) ) ∧ ( 1^st ‘ 𝑞 ) ≠ ( 2^nd ‘ 𝑞 ) ) ∧ 𝑦 = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑚 ) ( ( 2^nd ‘ 𝑞 ) Btwn ⟨ ( 1^st ‘ 𝑞 ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ 𝑞 ) , 𝑟 ⟩ Cgr 𝑝 ) ) ) ) → 𝑥 = 𝑦 )
24	23	gen2	⊢ ∀ 𝑥 ∀ 𝑦 ( ( ∃ 𝑛 ∈ ℕ ( ( 𝑝 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ 𝑞 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ ( 1^st ‘ 𝑞 ) ≠ ( 2^nd ‘ 𝑞 ) ) ∧ 𝑥 = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑛 ) ( ( 2^nd ‘ 𝑞 ) Btwn ⟨ ( 1^st ‘ 𝑞 ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ 𝑞 ) , 𝑟 ⟩ Cgr 𝑝 ) ) ) ∧ ∃ 𝑚 ∈ ℕ ( ( 𝑝 ∈ ( ( 𝔼 ‘ 𝑚 ) × ( 𝔼 ‘ 𝑚 ) ) ∧ 𝑞 ∈ ( ( 𝔼 ‘ 𝑚 ) × ( 𝔼 ‘ 𝑚 ) ) ∧ ( 1^st ‘ 𝑞 ) ≠ ( 2^nd ‘ 𝑞 ) ) ∧ 𝑦 = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑚 ) ( ( 2^nd ‘ 𝑞 ) Btwn ⟨ ( 1^st ‘ 𝑞 ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ 𝑞 ) , 𝑟 ⟩ Cgr 𝑝 ) ) ) ) → 𝑥 = 𝑦 )
25		eqeq1	⊢ ( 𝑥 = 𝑦 → ( 𝑥 = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑛 ) ( ( 2^nd ‘ 𝑞 ) Btwn ⟨ ( 1^st ‘ 𝑞 ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ 𝑞 ) , 𝑟 ⟩ Cgr 𝑝 ) ) ↔ 𝑦 = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑛 ) ( ( 2^nd ‘ 𝑞 ) Btwn ⟨ ( 1^st ‘ 𝑞 ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ 𝑞 ) , 𝑟 ⟩ Cgr 𝑝 ) ) ) )
26	25	anbi2d	⊢ ( 𝑥 = 𝑦 → ( ( ( 𝑝 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ 𝑞 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ ( 1^st ‘ 𝑞 ) ≠ ( 2^nd ‘ 𝑞 ) ) ∧ 𝑥 = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑛 ) ( ( 2^nd ‘ 𝑞 ) Btwn ⟨ ( 1^st ‘ 𝑞 ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ 𝑞 ) , 𝑟 ⟩ Cgr 𝑝 ) ) ) ↔ ( ( 𝑝 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ 𝑞 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ ( 1^st ‘ 𝑞 ) ≠ ( 2^nd ‘ 𝑞 ) ) ∧ 𝑦 = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑛 ) ( ( 2^nd ‘ 𝑞 ) Btwn ⟨ ( 1^st ‘ 𝑞 ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ 𝑞 ) , 𝑟 ⟩ Cgr 𝑝 ) ) ) ) )
27	26	rexbidv	⊢ ( 𝑥 = 𝑦 → ( ∃ 𝑛 ∈ ℕ ( ( 𝑝 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ 𝑞 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ ( 1^st ‘ 𝑞 ) ≠ ( 2^nd ‘ 𝑞 ) ) ∧ 𝑥 = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑛 ) ( ( 2^nd ‘ 𝑞 ) Btwn ⟨ ( 1^st ‘ 𝑞 ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ 𝑞 ) , 𝑟 ⟩ Cgr 𝑝 ) ) ) ↔ ∃ 𝑛 ∈ ℕ ( ( 𝑝 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ 𝑞 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ ( 1^st ‘ 𝑞 ) ≠ ( 2^nd ‘ 𝑞 ) ) ∧ 𝑦 = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑛 ) ( ( 2^nd ‘ 𝑞 ) Btwn ⟨ ( 1^st ‘ 𝑞 ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ 𝑞 ) , 𝑟 ⟩ Cgr 𝑝 ) ) ) ) )
28	10	sqxpeqd	⊢ ( 𝑛 = 𝑚 → ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) = ( ( 𝔼 ‘ 𝑚 ) × ( 𝔼 ‘ 𝑚 ) ) )
29	28	eleq2d	⊢ ( 𝑛 = 𝑚 → ( 𝑝 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ↔ 𝑝 ∈ ( ( 𝔼 ‘ 𝑚 ) × ( 𝔼 ‘ 𝑚 ) ) ) )
30	28	eleq2d	⊢ ( 𝑛 = 𝑚 → ( 𝑞 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ↔ 𝑞 ∈ ( ( 𝔼 ‘ 𝑚 ) × ( 𝔼 ‘ 𝑚 ) ) ) )
31	29 30	3anbi12d	⊢ ( 𝑛 = 𝑚 → ( ( 𝑝 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ 𝑞 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ ( 1^st ‘ 𝑞 ) ≠ ( 2^nd ‘ 𝑞 ) ) ↔ ( 𝑝 ∈ ( ( 𝔼 ‘ 𝑚 ) × ( 𝔼 ‘ 𝑚 ) ) ∧ 𝑞 ∈ ( ( 𝔼 ‘ 𝑚 ) × ( 𝔼 ‘ 𝑚 ) ) ∧ ( 1^st ‘ 𝑞 ) ≠ ( 2^nd ‘ 𝑞 ) ) ) )
32	31 12	anbi12d	⊢ ( 𝑛 = 𝑚 → ( ( ( 𝑝 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ 𝑞 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ ( 1^st ‘ 𝑞 ) ≠ ( 2^nd ‘ 𝑞 ) ) ∧ 𝑦 = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑛 ) ( ( 2^nd ‘ 𝑞 ) Btwn ⟨ ( 1^st ‘ 𝑞 ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ 𝑞 ) , 𝑟 ⟩ Cgr 𝑝 ) ) ) ↔ ( ( 𝑝 ∈ ( ( 𝔼 ‘ 𝑚 ) × ( 𝔼 ‘ 𝑚 ) ) ∧ 𝑞 ∈ ( ( 𝔼 ‘ 𝑚 ) × ( 𝔼 ‘ 𝑚 ) ) ∧ ( 1^st ‘ 𝑞 ) ≠ ( 2^nd ‘ 𝑞 ) ) ∧ 𝑦 = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑚 ) ( ( 2^nd ‘ 𝑞 ) Btwn ⟨ ( 1^st ‘ 𝑞 ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ 𝑞 ) , 𝑟 ⟩ Cgr 𝑝 ) ) ) ) )
33	32	cbvrexvw	⊢ ( ∃ 𝑛 ∈ ℕ ( ( 𝑝 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ 𝑞 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ ( 1^st ‘ 𝑞 ) ≠ ( 2^nd ‘ 𝑞 ) ) ∧ 𝑦 = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑛 ) ( ( 2^nd ‘ 𝑞 ) Btwn ⟨ ( 1^st ‘ 𝑞 ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ 𝑞 ) , 𝑟 ⟩ Cgr 𝑝 ) ) ) ↔ ∃ 𝑚 ∈ ℕ ( ( 𝑝 ∈ ( ( 𝔼 ‘ 𝑚 ) × ( 𝔼 ‘ 𝑚 ) ) ∧ 𝑞 ∈ ( ( 𝔼 ‘ 𝑚 ) × ( 𝔼 ‘ 𝑚 ) ) ∧ ( 1^st ‘ 𝑞 ) ≠ ( 2^nd ‘ 𝑞 ) ) ∧ 𝑦 = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑚 ) ( ( 2^nd ‘ 𝑞 ) Btwn ⟨ ( 1^st ‘ 𝑞 ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ 𝑞 ) , 𝑟 ⟩ Cgr 𝑝 ) ) ) )
34	27 33	bitrdi	⊢ ( 𝑥 = 𝑦 → ( ∃ 𝑛 ∈ ℕ ( ( 𝑝 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ 𝑞 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ ( 1^st ‘ 𝑞 ) ≠ ( 2^nd ‘ 𝑞 ) ) ∧ 𝑥 = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑛 ) ( ( 2^nd ‘ 𝑞 ) Btwn ⟨ ( 1^st ‘ 𝑞 ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ 𝑞 ) , 𝑟 ⟩ Cgr 𝑝 ) ) ) ↔ ∃ 𝑚 ∈ ℕ ( ( 𝑝 ∈ ( ( 𝔼 ‘ 𝑚 ) × ( 𝔼 ‘ 𝑚 ) ) ∧ 𝑞 ∈ ( ( 𝔼 ‘ 𝑚 ) × ( 𝔼 ‘ 𝑚 ) ) ∧ ( 1^st ‘ 𝑞 ) ≠ ( 2^nd ‘ 𝑞 ) ) ∧ 𝑦 = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑚 ) ( ( 2^nd ‘ 𝑞 ) Btwn ⟨ ( 1^st ‘ 𝑞 ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ 𝑞 ) , 𝑟 ⟩ Cgr 𝑝 ) ) ) ) )
35	34	mo4	⊢ ( ∃* 𝑥 ∃ 𝑛 ∈ ℕ ( ( 𝑝 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ 𝑞 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ ( 1^st ‘ 𝑞 ) ≠ ( 2^nd ‘ 𝑞 ) ) ∧ 𝑥 = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑛 ) ( ( 2^nd ‘ 𝑞 ) Btwn ⟨ ( 1^st ‘ 𝑞 ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ 𝑞 ) , 𝑟 ⟩ Cgr 𝑝 ) ) ) ↔ ∀ 𝑥 ∀ 𝑦 ( ( ∃ 𝑛 ∈ ℕ ( ( 𝑝 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ 𝑞 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ ( 1^st ‘ 𝑞 ) ≠ ( 2^nd ‘ 𝑞 ) ) ∧ 𝑥 = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑛 ) ( ( 2^nd ‘ 𝑞 ) Btwn ⟨ ( 1^st ‘ 𝑞 ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ 𝑞 ) , 𝑟 ⟩ Cgr 𝑝 ) ) ) ∧ ∃ 𝑚 ∈ ℕ ( ( 𝑝 ∈ ( ( 𝔼 ‘ 𝑚 ) × ( 𝔼 ‘ 𝑚 ) ) ∧ 𝑞 ∈ ( ( 𝔼 ‘ 𝑚 ) × ( 𝔼 ‘ 𝑚 ) ) ∧ ( 1^st ‘ 𝑞 ) ≠ ( 2^nd ‘ 𝑞 ) ) ∧ 𝑦 = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑚 ) ( ( 2^nd ‘ 𝑞 ) Btwn ⟨ ( 1^st ‘ 𝑞 ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ 𝑞 ) , 𝑟 ⟩ Cgr 𝑝 ) ) ) ) → 𝑥 = 𝑦 ) )
36	24 35	mpbir	⊢ ∃* 𝑥 ∃ 𝑛 ∈ ℕ ( ( 𝑝 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ 𝑞 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ ( 1^st ‘ 𝑞 ) ≠ ( 2^nd ‘ 𝑞 ) ) ∧ 𝑥 = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑛 ) ( ( 2^nd ‘ 𝑞 ) Btwn ⟨ ( 1^st ‘ 𝑞 ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ 𝑞 ) , 𝑟 ⟩ Cgr 𝑝 ) ) )
37	36	funoprab	⊢ Fun { ⟨ ⟨ 𝑝 , 𝑞 ⟩ , 𝑥 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑝 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ 𝑞 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ ( 1^st ‘ 𝑞 ) ≠ ( 2^nd ‘ 𝑞 ) ) ∧ 𝑥 = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑛 ) ( ( 2^nd ‘ 𝑞 ) Btwn ⟨ ( 1^st ‘ 𝑞 ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ 𝑞 ) , 𝑟 ⟩ Cgr 𝑝 ) ) ) }
38		df-transport	⊢ TransportTo = { ⟨ ⟨ 𝑝 , 𝑞 ⟩ , 𝑥 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑝 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ 𝑞 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ ( 1^st ‘ 𝑞 ) ≠ ( 2^nd ‘ 𝑞 ) ) ∧ 𝑥 = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑛 ) ( ( 2^nd ‘ 𝑞 ) Btwn ⟨ ( 1^st ‘ 𝑞 ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ 𝑞 ) , 𝑟 ⟩ Cgr 𝑝 ) ) ) }
39	38	funeqi	⊢ ( Fun TransportTo ↔ Fun { ⟨ ⟨ 𝑝 , 𝑞 ⟩ , 𝑥 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑝 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ 𝑞 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ ( 1^st ‘ 𝑞 ) ≠ ( 2^nd ‘ 𝑞 ) ) ∧ 𝑥 = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑛 ) ( ( 2^nd ‘ 𝑞 ) Btwn ⟨ ( 1^st ‘ 𝑞 ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ 𝑞 ) , 𝑟 ⟩ Cgr 𝑝 ) ) ) } )
40	37 39	mpbir	⊢ Fun TransportTo

Metamath Proof Explorer

Theorem funtransport

Proof