fvtransport

Description: Calculate the value of the TransportTo function. This function takes four points, A through D , where C and D are distinct. It then returns the point that extends C D by the length of A B . (Contributed by Scott Fenton, 18-Oct-2013) (Revised by Mario Carneiro, 19-Apr-2014)

		Ref	Expression
	Assertion	fvtransport	⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝐶 ≠ 𝐷 ) ) → ( ⟨ 𝐴 , 𝐵 ⟩ TransportTo ⟨ 𝐶 , 𝐷 ⟩ ) = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐷 Btwn ⟨ 𝐶 , 𝑟 ⟩ ∧ ⟨ 𝐷 , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) )

Proof

Step	Hyp	Ref	Expression
1		df-ov	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ TransportTo ⟨ 𝐶 , 𝐷 ⟩ ) = ( TransportTo ‘ ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ )
2		opelxpi	⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ( 𝔼 ‘ 𝑁 ) × ( 𝔼 ‘ 𝑁 ) ) )
3	2	3ad2ant1	⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝐶 ≠ 𝐷 ) → ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ( 𝔼 ‘ 𝑁 ) × ( 𝔼 ‘ 𝑁 ) ) )
4		opelxpi	⊢ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) → ⟨ 𝐶 , 𝐷 ⟩ ∈ ( ( 𝔼 ‘ 𝑁 ) × ( 𝔼 ‘ 𝑁 ) ) )
5	4	3ad2ant2	⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝐶 ≠ 𝐷 ) → ⟨ 𝐶 , 𝐷 ⟩ ∈ ( ( 𝔼 ‘ 𝑁 ) × ( 𝔼 ‘ 𝑁 ) ) )
6		simp3	⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝐶 ≠ 𝐷 ) → 𝐶 ≠ 𝐷 )
7		op1stg	⊢ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 1^st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) = 𝐶 )
8	7	3ad2ant2	⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝐶 ≠ 𝐷 ) → ( 1^st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) = 𝐶 )
9		op2ndg	⊢ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) = 𝐷 )
10	9	3ad2ant2	⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝐶 ≠ 𝐷 ) → ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) = 𝐷 )
11	6 8 10	3netr4d	⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝐶 ≠ 𝐷 ) → ( 1^st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ≠ ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) )
12	3 5 11	3jca	⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝐶 ≠ 𝐷 ) → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ( 𝔼 ‘ 𝑁 ) × ( 𝔼 ‘ 𝑁 ) ) ∧ ⟨ 𝐶 , 𝐷 ⟩ ∈ ( ( 𝔼 ‘ 𝑁 ) × ( 𝔼 ‘ 𝑁 ) ) ∧ ( 1^st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ≠ ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ) )
13	8	opeq1d	⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝐶 ≠ 𝐷 ) → ⟨ ( 1^st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) , 𝑟 ⟩ = ⟨ 𝐶 , 𝑟 ⟩ )
14	10 13	breq12d	⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝐶 ≠ 𝐷 ) → ( ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) Btwn ⟨ ( 1^st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) , 𝑟 ⟩ ↔ 𝐷 Btwn ⟨ 𝐶 , 𝑟 ⟩ ) )
15	10	opeq1d	⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝐶 ≠ 𝐷 ) → ⟨ ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) , 𝑟 ⟩ = ⟨ 𝐷 , 𝑟 ⟩ )
16	15	breq1d	⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝐶 ≠ 𝐷 ) → ( ⟨ ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ↔ ⟨ 𝐷 , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) )
17	14 16	anbi12d	⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝐶 ≠ 𝐷 ) → ( ( ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) Btwn ⟨ ( 1^st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ↔ ( 𝐷 Btwn ⟨ 𝐶 , 𝑟 ⟩ ∧ ⟨ 𝐷 , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) )
18	17	riotabidv	⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝐶 ≠ 𝐷 ) → ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ( ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) Btwn ⟨ ( 1^st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐷 Btwn ⟨ 𝐶 , 𝑟 ⟩ ∧ ⟨ 𝐷 , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) )
19	18	eqcomd	⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝐶 ≠ 𝐷 ) → ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐷 Btwn ⟨ 𝐶 , 𝑟 ⟩ ∧ ⟨ 𝐷 , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ( ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) Btwn ⟨ ( 1^st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) )
20	12 19	jca	⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝐶 ≠ 𝐷 ) → ( ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ( 𝔼 ‘ 𝑁 ) × ( 𝔼 ‘ 𝑁 ) ) ∧ ⟨ 𝐶 , 𝐷 ⟩ ∈ ( ( 𝔼 ‘ 𝑁 ) × ( 𝔼 ‘ 𝑁 ) ) ∧ ( 1^st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ≠ ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐷 Btwn ⟨ 𝐶 , 𝑟 ⟩ ∧ ⟨ 𝐷 , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ( ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) Btwn ⟨ ( 1^st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ) )
21		fveq2	⊢ ( 𝑛 = 𝑁 → ( 𝔼 ‘ 𝑛 ) = ( 𝔼 ‘ 𝑁 ) )
22	21	sqxpeqd	⊢ ( 𝑛 = 𝑁 → ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) = ( ( 𝔼 ‘ 𝑁 ) × ( 𝔼 ‘ 𝑁 ) ) )
23	22	eleq2d	⊢ ( 𝑛 = 𝑁 → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ( 𝔼 ‘ 𝑁 ) × ( 𝔼 ‘ 𝑁 ) ) ) )
24	22	eleq2d	⊢ ( 𝑛 = 𝑁 → ( ⟨ 𝐶 , 𝐷 ⟩ ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ↔ ⟨ 𝐶 , 𝐷 ⟩ ∈ ( ( 𝔼 ‘ 𝑁 ) × ( 𝔼 ‘ 𝑁 ) ) ) )
25	23 24	3anbi12d	⊢ ( 𝑛 = 𝑁 → ( ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ ⟨ 𝐶 , 𝐷 ⟩ ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ ( 1^st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ≠ ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ) ↔ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ( 𝔼 ‘ 𝑁 ) × ( 𝔼 ‘ 𝑁 ) ) ∧ ⟨ 𝐶 , 𝐷 ⟩ ∈ ( ( 𝔼 ‘ 𝑁 ) × ( 𝔼 ‘ 𝑁 ) ) ∧ ( 1^st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ≠ ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ) ) )
26	21	riotaeqdv	⊢ ( 𝑛 = 𝑁 → ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑛 ) ( ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) Btwn ⟨ ( 1^st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ( ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) Btwn ⟨ ( 1^st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) )
27	26	eqeq2d	⊢ ( 𝑛 = 𝑁 → ( ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐷 Btwn ⟨ 𝐶 , 𝑟 ⟩ ∧ ⟨ 𝐷 , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑛 ) ( ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) Btwn ⟨ ( 1^st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ↔ ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐷 Btwn ⟨ 𝐶 , 𝑟 ⟩ ∧ ⟨ 𝐷 , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ( ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) Btwn ⟨ ( 1^st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ) )
28	25 27	anbi12d	⊢ ( 𝑛 = 𝑁 → ( ( ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ ⟨ 𝐶 , 𝐷 ⟩ ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ ( 1^st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ≠ ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐷 Btwn ⟨ 𝐶 , 𝑟 ⟩ ∧ ⟨ 𝐷 , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑛 ) ( ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) Btwn ⟨ ( 1^st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ) ↔ ( ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ( 𝔼 ‘ 𝑁 ) × ( 𝔼 ‘ 𝑁 ) ) ∧ ⟨ 𝐶 , 𝐷 ⟩ ∈ ( ( 𝔼 ‘ 𝑁 ) × ( 𝔼 ‘ 𝑁 ) ) ∧ ( 1^st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ≠ ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐷 Btwn ⟨ 𝐶 , 𝑟 ⟩ ∧ ⟨ 𝐷 , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ( ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) Btwn ⟨ ( 1^st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ) ) )
29	28	rspcev	⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ( 𝔼 ‘ 𝑁 ) × ( 𝔼 ‘ 𝑁 ) ) ∧ ⟨ 𝐶 , 𝐷 ⟩ ∈ ( ( 𝔼 ‘ 𝑁 ) × ( 𝔼 ‘ 𝑁 ) ) ∧ ( 1^st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ≠ ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐷 Btwn ⟨ 𝐶 , 𝑟 ⟩ ∧ ⟨ 𝐷 , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ( ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) Btwn ⟨ ( 1^st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ) ) → ∃ 𝑛 ∈ ℕ ( ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ ⟨ 𝐶 , 𝐷 ⟩ ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ ( 1^st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ≠ ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐷 Btwn ⟨ 𝐶 , 𝑟 ⟩ ∧ ⟨ 𝐷 , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑛 ) ( ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) Btwn ⟨ ( 1^st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ) )
30	20 29	sylan2	⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝐶 ≠ 𝐷 ) ) → ∃ 𝑛 ∈ ℕ ( ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ ⟨ 𝐶 , 𝐷 ⟩ ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ ( 1^st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ≠ ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐷 Btwn ⟨ 𝐶 , 𝑟 ⟩ ∧ ⟨ 𝐷 , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑛 ) ( ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) Btwn ⟨ ( 1^st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ) )
31		df-br	⊢ ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ TransportTo ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐷 Btwn ⟨ 𝐶 , 𝑟 ⟩ ∧ ⟨ 𝐷 , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ↔ ⟨ ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ , ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐷 Btwn ⟨ 𝐶 , 𝑟 ⟩ ∧ ⟨ 𝐷 , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ⟩ ∈ TransportTo )
32		df-transport	⊢ TransportTo = { ⟨ ⟨ 𝑝 , 𝑞 ⟩ , 𝑥 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑝 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ 𝑞 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ ( 1^st ‘ 𝑞 ) ≠ ( 2^nd ‘ 𝑞 ) ) ∧ 𝑥 = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑛 ) ( ( 2^nd ‘ 𝑞 ) Btwn ⟨ ( 1^st ‘ 𝑞 ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ 𝑞 ) , 𝑟 ⟩ Cgr 𝑝 ) ) ) }
33	32	eleq2i	⊢ ( ⟨ ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ , ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐷 Btwn ⟨ 𝐶 , 𝑟 ⟩ ∧ ⟨ 𝐷 , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ⟩ ∈ TransportTo ↔ ⟨ ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ , ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐷 Btwn ⟨ 𝐶 , 𝑟 ⟩ ∧ ⟨ 𝐷 , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ⟩ ∈ { ⟨ ⟨ 𝑝 , 𝑞 ⟩ , 𝑥 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑝 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ 𝑞 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ ( 1^st ‘ 𝑞 ) ≠ ( 2^nd ‘ 𝑞 ) ) ∧ 𝑥 = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑛 ) ( ( 2^nd ‘ 𝑞 ) Btwn ⟨ ( 1^st ‘ 𝑞 ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ 𝑞 ) , 𝑟 ⟩ Cgr 𝑝 ) ) ) } )
34		opex	⊢ ⟨ 𝐴 , 𝐵 ⟩ ∈ V
35		opex	⊢ ⟨ 𝐶 , 𝐷 ⟩ ∈ V
36		riotaex	⊢ ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐷 Btwn ⟨ 𝐶 , 𝑟 ⟩ ∧ ⟨ 𝐷 , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ∈ V
37		eleq1	⊢ ( 𝑝 = ⟨ 𝐴 , 𝐵 ⟩ → ( 𝑝 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ) )
38	37	3anbi1d	⊢ ( 𝑝 = ⟨ 𝐴 , 𝐵 ⟩ → ( ( 𝑝 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ 𝑞 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ ( 1^st ‘ 𝑞 ) ≠ ( 2^nd ‘ 𝑞 ) ) ↔ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ 𝑞 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ ( 1^st ‘ 𝑞 ) ≠ ( 2^nd ‘ 𝑞 ) ) ) )
39		breq2	⊢ ( 𝑝 = ⟨ 𝐴 , 𝐵 ⟩ → ( ⟨ ( 2^nd ‘ 𝑞 ) , 𝑟 ⟩ Cgr 𝑝 ↔ ⟨ ( 2^nd ‘ 𝑞 ) , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) )
40	39	anbi2d	⊢ ( 𝑝 = ⟨ 𝐴 , 𝐵 ⟩ → ( ( ( 2^nd ‘ 𝑞 ) Btwn ⟨ ( 1^st ‘ 𝑞 ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ 𝑞 ) , 𝑟 ⟩ Cgr 𝑝 ) ↔ ( ( 2^nd ‘ 𝑞 ) Btwn ⟨ ( 1^st ‘ 𝑞 ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ 𝑞 ) , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) )
41	40	riotabidv	⊢ ( 𝑝 = ⟨ 𝐴 , 𝐵 ⟩ → ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑛 ) ( ( 2^nd ‘ 𝑞 ) Btwn ⟨ ( 1^st ‘ 𝑞 ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ 𝑞 ) , 𝑟 ⟩ Cgr 𝑝 ) ) = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑛 ) ( ( 2^nd ‘ 𝑞 ) Btwn ⟨ ( 1^st ‘ 𝑞 ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ 𝑞 ) , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) )
42	41	eqeq2d	⊢ ( 𝑝 = ⟨ 𝐴 , 𝐵 ⟩ → ( 𝑥 = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑛 ) ( ( 2^nd ‘ 𝑞 ) Btwn ⟨ ( 1^st ‘ 𝑞 ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ 𝑞 ) , 𝑟 ⟩ Cgr 𝑝 ) ) ↔ 𝑥 = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑛 ) ( ( 2^nd ‘ 𝑞 ) Btwn ⟨ ( 1^st ‘ 𝑞 ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ 𝑞 ) , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ) )
43	38 42	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 ⟨ 𝐴 , 𝐵 ⟩ ) ) ) ) )
44	43	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 ⟨ 𝐴 , 𝐵 ⟩ ) ) ) ) )
45		eleq1	⊢ ( 𝑞 = ⟨ 𝐶 , 𝐷 ⟩ → ( 𝑞 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ↔ ⟨ 𝐶 , 𝐷 ⟩ ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ) )
46		fveq2	⊢ ( 𝑞 = ⟨ 𝐶 , 𝐷 ⟩ → ( 1^st ‘ 𝑞 ) = ( 1^st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) )
47		fveq2	⊢ ( 𝑞 = ⟨ 𝐶 , 𝐷 ⟩ → ( 2^nd ‘ 𝑞 ) = ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) )
48	46 47	neeq12d	⊢ ( 𝑞 = ⟨ 𝐶 , 𝐷 ⟩ → ( ( 1^st ‘ 𝑞 ) ≠ ( 2^nd ‘ 𝑞 ) ↔ ( 1^st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ≠ ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ) )
49	45 48	3anbi23d	⊢ ( 𝑞 = ⟨ 𝐶 , 𝐷 ⟩ → ( ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ 𝑞 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ ( 1^st ‘ 𝑞 ) ≠ ( 2^nd ‘ 𝑞 ) ) ↔ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ ⟨ 𝐶 , 𝐷 ⟩ ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ ( 1^st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ≠ ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ) ) )
50	46	opeq1d	⊢ ( 𝑞 = ⟨ 𝐶 , 𝐷 ⟩ → ⟨ ( 1^st ‘ 𝑞 ) , 𝑟 ⟩ = ⟨ ( 1^st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) , 𝑟 ⟩ )
51	47 50	breq12d	⊢ ( 𝑞 = ⟨ 𝐶 , 𝐷 ⟩ → ( ( 2^nd ‘ 𝑞 ) Btwn ⟨ ( 1^st ‘ 𝑞 ) , 𝑟 ⟩ ↔ ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) Btwn ⟨ ( 1^st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) , 𝑟 ⟩ ) )
52	47	opeq1d	⊢ ( 𝑞 = ⟨ 𝐶 , 𝐷 ⟩ → ⟨ ( 2^nd ‘ 𝑞 ) , 𝑟 ⟩ = ⟨ ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) , 𝑟 ⟩ )
53	52	breq1d	⊢ ( 𝑞 = ⟨ 𝐶 , 𝐷 ⟩ → ( ⟨ ( 2^nd ‘ 𝑞 ) , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ↔ ⟨ ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) )
54	51 53	anbi12d	⊢ ( 𝑞 = ⟨ 𝐶 , 𝐷 ⟩ → ( ( ( 2^nd ‘ 𝑞 ) Btwn ⟨ ( 1^st ‘ 𝑞 ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ 𝑞 ) , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ↔ ( ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) Btwn ⟨ ( 1^st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) )
55	54	riotabidv	⊢ ( 𝑞 = ⟨ 𝐶 , 𝐷 ⟩ → ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑛 ) ( ( 2^nd ‘ 𝑞 ) Btwn ⟨ ( 1^st ‘ 𝑞 ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ 𝑞 ) , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑛 ) ( ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) Btwn ⟨ ( 1^st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) )
56	55	eqeq2d	⊢ ( 𝑞 = ⟨ 𝐶 , 𝐷 ⟩ → ( 𝑥 = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑛 ) ( ( 2^nd ‘ 𝑞 ) Btwn ⟨ ( 1^st ‘ 𝑞 ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ 𝑞 ) , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ↔ 𝑥 = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑛 ) ( ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) Btwn ⟨ ( 1^st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ) )
57	49 56	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 ⟨ 𝐴 , 𝐵 ⟩ ) ) ) ) )
58	57	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 ⟨ 𝐴 , 𝐵 ⟩ ) ) ) ) )
59		eqeq1	⊢ ( 𝑥 = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐷 Btwn ⟨ 𝐶 , 𝑟 ⟩ ∧ ⟨ 𝐷 , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) → ( 𝑥 = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑛 ) ( ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) Btwn ⟨ ( 1^st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ↔ ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐷 Btwn ⟨ 𝐶 , 𝑟 ⟩ ∧ ⟨ 𝐷 , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑛 ) ( ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) Btwn ⟨ ( 1^st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ) )
60	59	anbi2d	⊢ ( 𝑥 = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐷 Btwn ⟨ 𝐶 , 𝑟 ⟩ ∧ ⟨ 𝐷 , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) → ( ( ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ ⟨ 𝐶 , 𝐷 ⟩ ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ ( 1^st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ≠ ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ 𝑥 = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑛 ) ( ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) Btwn ⟨ ( 1^st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ) ↔ ( ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ ⟨ 𝐶 , 𝐷 ⟩ ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ ( 1^st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ≠ ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐷 Btwn ⟨ 𝐶 , 𝑟 ⟩ ∧ ⟨ 𝐷 , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑛 ) ( ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) Btwn ⟨ ( 1^st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ) ) )
61	60	rexbidv	⊢ ( 𝑥 = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐷 Btwn ⟨ 𝐶 , 𝑟 ⟩ ∧ ⟨ 𝐷 , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) → ( ∃ 𝑛 ∈ ℕ ( ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ ⟨ 𝐶 , 𝐷 ⟩ ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ ( 1^st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ≠ ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ 𝑥 = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑛 ) ( ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) Btwn ⟨ ( 1^st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ) ↔ ∃ 𝑛 ∈ ℕ ( ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ ⟨ 𝐶 , 𝐷 ⟩ ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ ( 1^st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ≠ ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐷 Btwn ⟨ 𝐶 , 𝑟 ⟩ ∧ ⟨ 𝐷 , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑛 ) ( ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) Btwn ⟨ ( 1^st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ) ) )
62	44 58 61	eloprabg	⊢ ( ( ⟨ 𝐴 , 𝐵 ⟩ ∈ V ∧ ⟨ 𝐶 , 𝐷 ⟩ ∈ V ∧ ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐷 Btwn ⟨ 𝐶 , 𝑟 ⟩ ∧ ⟨ 𝐷 , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ∈ V ) → ( ⟨ ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ , ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐷 Btwn ⟨ 𝐶 , 𝑟 ⟩ ∧ ⟨ 𝐷 , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ⟩ ∈ { ⟨ ⟨ 𝑝 , 𝑞 ⟩ , 𝑥 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑝 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ 𝑞 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ ( 1^st ‘ 𝑞 ) ≠ ( 2^nd ‘ 𝑞 ) ) ∧ 𝑥 = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑛 ) ( ( 2^nd ‘ 𝑞 ) Btwn ⟨ ( 1^st ‘ 𝑞 ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ 𝑞 ) , 𝑟 ⟩ Cgr 𝑝 ) ) ) } ↔ ∃ 𝑛 ∈ ℕ ( ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ ⟨ 𝐶 , 𝐷 ⟩ ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ ( 1^st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ≠ ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐷 Btwn ⟨ 𝐶 , 𝑟 ⟩ ∧ ⟨ 𝐷 , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑛 ) ( ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) Btwn ⟨ ( 1^st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ) ) )
63	34 35 36 62	mp3an	⊢ ( ⟨ ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ , ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐷 Btwn ⟨ 𝐶 , 𝑟 ⟩ ∧ ⟨ 𝐷 , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ⟩ ∈ { ⟨ ⟨ 𝑝 , 𝑞 ⟩ , 𝑥 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑝 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ 𝑞 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ ( 1^st ‘ 𝑞 ) ≠ ( 2^nd ‘ 𝑞 ) ) ∧ 𝑥 = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑛 ) ( ( 2^nd ‘ 𝑞 ) Btwn ⟨ ( 1^st ‘ 𝑞 ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ 𝑞 ) , 𝑟 ⟩ Cgr 𝑝 ) ) ) } ↔ ∃ 𝑛 ∈ ℕ ( ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ ⟨ 𝐶 , 𝐷 ⟩ ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ ( 1^st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ≠ ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐷 Btwn ⟨ 𝐶 , 𝑟 ⟩ ∧ ⟨ 𝐷 , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑛 ) ( ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) Btwn ⟨ ( 1^st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ) )
64	31 33 63	3bitri	⊢ ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ TransportTo ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐷 Btwn ⟨ 𝐶 , 𝑟 ⟩ ∧ ⟨ 𝐷 , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ↔ ∃ 𝑛 ∈ ℕ ( ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ ⟨ 𝐶 , 𝐷 ⟩ ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ ( 1^st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ≠ ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐷 Btwn ⟨ 𝐶 , 𝑟 ⟩ ∧ ⟨ 𝐷 , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑛 ) ( ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) Btwn ⟨ ( 1^st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ) )
65		funtransport	⊢ Fun TransportTo
66		funbrfv	⊢ ( Fun TransportTo → ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ TransportTo ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐷 Btwn ⟨ 𝐶 , 𝑟 ⟩ ∧ ⟨ 𝐷 , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) → ( TransportTo ‘ ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ ) = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐷 Btwn ⟨ 𝐶 , 𝑟 ⟩ ∧ ⟨ 𝐷 , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ) )
67	65 66	ax-mp	⊢ ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ TransportTo ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐷 Btwn ⟨ 𝐶 , 𝑟 ⟩ ∧ ⟨ 𝐷 , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) → ( TransportTo ‘ ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ ) = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐷 Btwn ⟨ 𝐶 , 𝑟 ⟩ ∧ ⟨ 𝐷 , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) )
68	64 67	sylbir	⊢ ( ∃ 𝑛 ∈ ℕ ( ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ ⟨ 𝐶 , 𝐷 ⟩ ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ ( 1^st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ≠ ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ) ∧ ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐷 Btwn ⟨ 𝐶 , 𝑟 ⟩ ∧ ⟨ 𝐷 , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑛 ) ( ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) Btwn ⟨ ( 1^st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ) → ( TransportTo ‘ ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ ) = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐷 Btwn ⟨ 𝐶 , 𝑟 ⟩ ∧ ⟨ 𝐷 , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) )
69	30 68	syl	⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝐶 ≠ 𝐷 ) ) → ( TransportTo ‘ ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ ) = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐷 Btwn ⟨ 𝐶 , 𝑟 ⟩ ∧ ⟨ 𝐷 , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) )
70	1 69	eqtrid	⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝐶 ≠ 𝐷 ) ) → ( ⟨ 𝐴 , 𝐵 ⟩ TransportTo ⟨ 𝐶 , 𝐷 ⟩ ) = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐷 Btwn ⟨ 𝐶 , 𝑟 ⟩ ∧ ⟨ 𝐷 , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) )

Metamath Proof Explorer

Theorem fvtransport

Proof