df-transport

Description: Define the segment transport function. See fvtransport for an explanation of the function. (Contributed by Scott Fenton, 18-Oct-2013)

		Ref	Expression
	Assertion	df-transport	⊢ TransportTo = { ⟨ ⟨ 𝑝 , 𝑞 ⟩ , 𝑥 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑝 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ 𝑞 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ ( 1^st ‘ 𝑞 ) ≠ ( 2^nd ‘ 𝑞 ) ) ∧ 𝑥 = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑛 ) ( ( 2^nd ‘ 𝑞 ) Btwn ⟨ ( 1^st ‘ 𝑞 ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ 𝑞 ) , 𝑟 ⟩ Cgr 𝑝 ) ) ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ctransport	⊢ TransportTo
1		vp	⊢ 𝑝
2		vq	⊢ 𝑞
3		vx	⊢ 𝑥
4		vn	⊢ 𝑛
5		cn	⊢ ℕ
6	1	cv	⊢ 𝑝
7		cee	⊢ 𝔼
8	4	cv	⊢ 𝑛
9	8 7	cfv	⊢ ( 𝔼 ‘ 𝑛 )
10	9 9	cxp	⊢ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) )
11	6 10	wcel	⊢ 𝑝 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) )
12	2	cv	⊢ 𝑞
13	12 10	wcel	⊢ 𝑞 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) )
14		c1st	⊢ 1^st
15	12 14	cfv	⊢ ( 1^st ‘ 𝑞 )
16		c2nd	⊢ 2^nd
17	12 16	cfv	⊢ ( 2^nd ‘ 𝑞 )
18	15 17	wne	⊢ ( 1^st ‘ 𝑞 ) ≠ ( 2^nd ‘ 𝑞 )
19	11 13 18	w3a	⊢ ( 𝑝 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ 𝑞 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ ( 1^st ‘ 𝑞 ) ≠ ( 2^nd ‘ 𝑞 ) )
20	3	cv	⊢ 𝑥
21		vr	⊢ 𝑟
22		cbtwn	⊢ Btwn
23	21	cv	⊢ 𝑟
24	15 23	cop	⊢ ⟨ ( 1^st ‘ 𝑞 ) , 𝑟 ⟩
25	17 24 22	wbr	⊢ ( 2^nd ‘ 𝑞 ) Btwn ⟨ ( 1^st ‘ 𝑞 ) , 𝑟 ⟩
26	17 23	cop	⊢ ⟨ ( 2^nd ‘ 𝑞 ) , 𝑟 ⟩
27		ccgr	⊢ Cgr
28	26 6 27	wbr	⊢ ⟨ ( 2^nd ‘ 𝑞 ) , 𝑟 ⟩ Cgr 𝑝
29	25 28	wa	⊢ ( ( 2^nd ‘ 𝑞 ) Btwn ⟨ ( 1^st ‘ 𝑞 ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ 𝑞 ) , 𝑟 ⟩ Cgr 𝑝 )
30	29 21 9	crio	⊢ ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑛 ) ( ( 2^nd ‘ 𝑞 ) Btwn ⟨ ( 1^st ‘ 𝑞 ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ 𝑞 ) , 𝑟 ⟩ Cgr 𝑝 ) )
31	20 30	wceq	⊢ 𝑥 = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑛 ) ( ( 2^nd ‘ 𝑞 ) Btwn ⟨ ( 1^st ‘ 𝑞 ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ 𝑞 ) , 𝑟 ⟩ Cgr 𝑝 ) )
32	19 31	wa	⊢ ( ( 𝑝 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ 𝑞 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ ( 1^st ‘ 𝑞 ) ≠ ( 2^nd ‘ 𝑞 ) ) ∧ 𝑥 = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑛 ) ( ( 2^nd ‘ 𝑞 ) Btwn ⟨ ( 1^st ‘ 𝑞 ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ 𝑞 ) , 𝑟 ⟩ Cgr 𝑝 ) ) )
33	32 4 5	wrex	⊢ ∃ 𝑛 ∈ ℕ ( ( 𝑝 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ 𝑞 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ ( 1^st ‘ 𝑞 ) ≠ ( 2^nd ‘ 𝑞 ) ) ∧ 𝑥 = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑛 ) ( ( 2^nd ‘ 𝑞 ) Btwn ⟨ ( 1^st ‘ 𝑞 ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ 𝑞 ) , 𝑟 ⟩ Cgr 𝑝 ) ) )
34	33 1 2 3	coprab	⊢ { ⟨ ⟨ 𝑝 , 𝑞 ⟩ , 𝑥 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑝 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ 𝑞 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ ( 1^st ‘ 𝑞 ) ≠ ( 2^nd ‘ 𝑞 ) ) ∧ 𝑥 = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑛 ) ( ( 2^nd ‘ 𝑞 ) Btwn ⟨ ( 1^st ‘ 𝑞 ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ 𝑞 ) , 𝑟 ⟩ Cgr 𝑝 ) ) ) }
35	0 34	wceq	⊢ TransportTo = { ⟨ ⟨ 𝑝 , 𝑞 ⟩ , 𝑥 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑝 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ 𝑞 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ ( 1^st ‘ 𝑞 ) ≠ ( 2^nd ‘ 𝑞 ) ) ∧ 𝑥 = ( ℩ 𝑟 ∈ ( 𝔼 ‘ 𝑛 ) ( ( 2^nd ‘ 𝑞 ) Btwn ⟨ ( 1^st ‘ 𝑞 ) , 𝑟 ⟩ ∧ ⟨ ( 2^nd ‘ 𝑞 ) , 𝑟 ⟩ Cgr 𝑝 ) ) ) }

Metamath Proof Explorer

Definition df-transport

Detailed syntax breakdown