ttgval - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > ttgval		Structured version Visualization version GIF version

Theorem ttgval 25555

Description: Define a function to augment a complex Hilbert space with betweenness and a line definition. (Contributed by Thierry Arnoux, 25-Mar-2019.)

**Hypotheses**
Ref	Expression
ttgval.n	⊢ 𝐺 = (toTG‘𝐻)
ttgval.b	⊢ 𝐵 = (Base‘𝐻)
ttgval.m	⊢ − = (-_g‘𝐻)
ttgval.s	⊢ · = ( ·_𝑠 ‘𝐻)
ttgval.i	⊢ 𝐼 = (Itv‘𝐺)

**Assertion**
Ref	Expression
ttgval	⊢ (𝐻 ∈ 𝑉 → (𝐺 = ((𝐻 sSet ⟨(Itv‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})⟩) sSet ⟨(LineG‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))})⟩) ∧ 𝐼 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})))

Distinct variable groups: 𝑥,𝑘,𝑦,𝑧 𝑥,𝐵,𝑦,𝑧 𝑘,𝐻,𝑥,𝑦,𝑧 𝑥,𝑉,𝑦,𝑧 𝑥, − ,𝑦,𝑧 𝑥, · ,𝑦,𝑧 Allowed substitution hints: 𝐵(𝑘) · (𝑘) 𝐺(𝑥,𝑦,𝑧,𝑘) 𝐼(𝑥,𝑦,𝑧,𝑘) − (𝑘) 𝑉(𝑘)

Proof of Theorem ttgval Dummy variables 𝑎 𝑏 𝑐 𝑖 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ttgval.n	. . . . 5 ⊢ 𝐺 = (toTG‘𝐻)
2	1	a1i 11	. . . 4 ⊢ (𝐻 ∈ 𝑉 → 𝐺 = (toTG‘𝐻))
3		elex 3185	. . . . 5 ⊢ (𝐻 ∈ 𝑉 → 𝐻 ∈ V)
4		fveq2 6103	. . . . . . . . . 10 ⊢ (𝑤 = 𝐻 → (Base‘𝑤) = (Base‘𝐻))
5		ttgval.b	. . . . . . . . . 10 ⊢ 𝐵 = (Base‘𝐻)
6	4, 5	syl6eqr 2662	. . . . . . . . 9 ⊢ (𝑤 = 𝐻 → (Base‘𝑤) = 𝐵)
7		fveq2 6103	. . . . . . . . . . . . . 14 ⊢ (𝑤 = 𝐻 → (-_g‘𝑤) = (-_g‘𝐻))
8		ttgval.m	. . . . . . . . . . . . . 14 ⊢ − = (-_g‘𝐻)
9	7, 8	syl6eqr 2662	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝐻 → (-_g‘𝑤) = − )
10	9	oveqd 6566	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝐻 → (𝑧(-_g‘𝑤)𝑥) = (𝑧 − 𝑥))
11		fveq2 6103	. . . . . . . . . . . . . 14 ⊢ (𝑤 = 𝐻 → ( ·_𝑠 ‘𝑤) = ( ·_𝑠 ‘𝐻))
12		ttgval.s	. . . . . . . . . . . . . 14 ⊢ · = ( ·_𝑠 ‘𝐻)
13	11, 12	syl6eqr 2662	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝐻 → ( ·_𝑠 ‘𝑤) = · )
14		eqidd 2611	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝐻 → 𝑘 = 𝑘)
15	9	oveqd 6566	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝐻 → (𝑦(-_g‘𝑤)𝑥) = (𝑦 − 𝑥))
16	13, 14, 15	oveq123d 6570	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝐻 → (𝑘( ·_𝑠 ‘𝑤)(𝑦(-_g‘𝑤)𝑥)) = (𝑘 · (𝑦 − 𝑥)))
17	10, 16	eqeq12d 2625	. . . . . . . . . . 11 ⊢ (𝑤 = 𝐻 → ((𝑧(-_g‘𝑤)𝑥) = (𝑘( ·_𝑠 ‘𝑤)(𝑦(-_g‘𝑤)𝑥)) ↔ (𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))))
18	17	rexbidv 3034	. . . . . . . . . 10 ⊢ (𝑤 = 𝐻 → (∃𝑘 ∈ (0[,]1)(𝑧(-_g‘𝑤)𝑥) = (𝑘( ·_𝑠 ‘𝑤)(𝑦(-_g‘𝑤)𝑥)) ↔ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))))
19	6, 18	rabeqbidv 3168	. . . . . . . . 9 ⊢ (𝑤 = 𝐻 → {𝑧 ∈ (Base‘𝑤) ∣ ∃𝑘 ∈ (0[,]1)(𝑧(-_g‘𝑤)𝑥) = (𝑘( ·_𝑠 ‘𝑤)(𝑦(-_g‘𝑤)𝑥))} = {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})
20	6, 6, 19	mpt2eq123dv 6615	. . . . . . . 8 ⊢ (𝑤 = 𝐻 → (𝑥 ∈ (Base‘𝑤), 𝑦 ∈ (Base‘𝑤) ↦ {𝑧 ∈ (Base‘𝑤) ∣ ∃𝑘 ∈ (0[,]1)(𝑧(-_g‘𝑤)𝑥) = (𝑘( ·_𝑠 ‘𝑤)(𝑦(-_g‘𝑤)𝑥))}) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))}))
21	20	csbeq1d 3506	. . . . . . 7 ⊢ (𝑤 = 𝐻 → ⦋(𝑥 ∈ (Base‘𝑤), 𝑦 ∈ (Base‘𝑤) ↦ {𝑧 ∈ (Base‘𝑤) ∣ ∃𝑘 ∈ (0[,]1)(𝑧(-_g‘𝑤)𝑥) = (𝑘( ·_𝑠 ‘𝑤)(𝑦(-_g‘𝑤)𝑥))}) / 𝑖⦌((𝑤 sSet ⟨(Itv‘ndx), 𝑖⟩) sSet ⟨(LineG‘ndx), (𝑥 ∈ (Base‘𝑤), 𝑦 ∈ (Base‘𝑤) ↦ {𝑧 ∈ (Base‘𝑤) ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})⟩) = ⦋(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))}) / 𝑖⦌((𝑤 sSet ⟨(Itv‘ndx), 𝑖⟩) sSet ⟨(LineG‘ndx), (𝑥 ∈ (Base‘𝑤), 𝑦 ∈ (Base‘𝑤) ↦ {𝑧 ∈ (Base‘𝑤) ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})⟩))
22		oveq1 6556	. . . . . . . . 9 ⊢ (𝑤 = 𝐻 → (𝑤 sSet ⟨(Itv‘ndx), 𝑖⟩) = (𝐻 sSet ⟨(Itv‘ndx), 𝑖⟩))
23		rabeq 3166	. . . . . . . . . . . 12 ⊢ ((Base‘𝑤) = 𝐵 → {𝑧 ∈ (Base‘𝑤) ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))} = {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})
24	6, 23	syl 17	. . . . . . . . . . 11 ⊢ (𝑤 = 𝐻 → {𝑧 ∈ (Base‘𝑤) ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))} = {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})
25	6, 6, 24	mpt2eq123dv 6615	. . . . . . . . . 10 ⊢ (𝑤 = 𝐻 → (𝑥 ∈ (Base‘𝑤), 𝑦 ∈ (Base‘𝑤) ↦ {𝑧 ∈ (Base‘𝑤) ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))}) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))}))
26	25	opeq2d 4347	. . . . . . . . 9 ⊢ (𝑤 = 𝐻 → ⟨(LineG‘ndx), (𝑥 ∈ (Base‘𝑤), 𝑦 ∈ (Base‘𝑤) ↦ {𝑧 ∈ (Base‘𝑤) ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})⟩ = ⟨(LineG‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})⟩)
27	22, 26	oveq12d 6567	. . . . . . . 8 ⊢ (𝑤 = 𝐻 → ((𝑤 sSet ⟨(Itv‘ndx), 𝑖⟩) sSet ⟨(LineG‘ndx), (𝑥 ∈ (Base‘𝑤), 𝑦 ∈ (Base‘𝑤) ↦ {𝑧 ∈ (Base‘𝑤) ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})⟩) = ((𝐻 sSet ⟨(Itv‘ndx), 𝑖⟩) sSet ⟨(LineG‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})⟩))
28	27	csbeq2dv 3944	. . . . . . 7 ⊢ (𝑤 = 𝐻 → ⦋(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))}) / 𝑖⦌((𝑤 sSet ⟨(Itv‘ndx), 𝑖⟩) sSet ⟨(LineG‘ndx), (𝑥 ∈ (Base‘𝑤), 𝑦 ∈ (Base‘𝑤) ↦ {𝑧 ∈ (Base‘𝑤) ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})⟩) = ⦋(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))}) / 𝑖⦌((𝐻 sSet ⟨(Itv‘ndx), 𝑖⟩) sSet ⟨(LineG‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})⟩))
29	21, 28	eqtrd 2644	. . . . . 6 ⊢ (𝑤 = 𝐻 → ⦋(𝑥 ∈ (Base‘𝑤), 𝑦 ∈ (Base‘𝑤) ↦ {𝑧 ∈ (Base‘𝑤) ∣ ∃𝑘 ∈ (0[,]1)(𝑧(-_g‘𝑤)𝑥) = (𝑘( ·_𝑠 ‘𝑤)(𝑦(-_g‘𝑤)𝑥))}) / 𝑖⦌((𝑤 sSet ⟨(Itv‘ndx), 𝑖⟩) sSet ⟨(LineG‘ndx), (𝑥 ∈ (Base‘𝑤), 𝑦 ∈ (Base‘𝑤) ↦ {𝑧 ∈ (Base‘𝑤) ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})⟩) = ⦋(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))}) / 𝑖⦌((𝐻 sSet ⟨(Itv‘ndx), 𝑖⟩) sSet ⟨(LineG‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})⟩))
30		df-ttg 25554	. . . . . 6 ⊢ toTG = (𝑤 ∈ V ↦ ⦋(𝑥 ∈ (Base‘𝑤), 𝑦 ∈ (Base‘𝑤) ↦ {𝑧 ∈ (Base‘𝑤) ∣ ∃𝑘 ∈ (0[,]1)(𝑧(-_g‘𝑤)𝑥) = (𝑘( ·_𝑠 ‘𝑤)(𝑦(-_g‘𝑤)𝑥))}) / 𝑖⦌((𝑤 sSet ⟨(Itv‘ndx), 𝑖⟩) sSet ⟨(LineG‘ndx), (𝑥 ∈ (Base‘𝑤), 𝑦 ∈ (Base‘𝑤) ↦ {𝑧 ∈ (Base‘𝑤) ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})⟩))
31		ovex 6577	. . . . . . 7 ⊢ ((𝐻 sSet ⟨(Itv‘ndx), 𝑖⟩) sSet ⟨(LineG‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})⟩) ∈ V
32	31	csbex 4721	. . . . . 6 ⊢ ⦋(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))}) / 𝑖⦌((𝐻 sSet ⟨(Itv‘ndx), 𝑖⟩) sSet ⟨(LineG‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})⟩) ∈ V
33	29, 30, 32	fvmpt 6191	. . . . 5 ⊢ (𝐻 ∈ V → (toTG‘𝐻) = ⦋(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))}) / 𝑖⦌((𝐻 sSet ⟨(Itv‘ndx), 𝑖⟩) sSet ⟨(LineG‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})⟩))
34	3, 33	syl 17	. . . 4 ⊢ (𝐻 ∈ 𝑉 → (toTG‘𝐻) = ⦋(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))}) / 𝑖⦌((𝐻 sSet ⟨(Itv‘ndx), 𝑖⟩) sSet ⟨(LineG‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})⟩))
35		fvex 6113	. . . . . . . 8 ⊢ (Base‘𝐻) ∈ V
36	5, 35	eqeltri 2684	. . . . . . 7 ⊢ 𝐵 ∈ V
37	36, 36	mpt2ex 7136	. . . . . 6 ⊢ (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))}) ∈ V
38	37	a1i 11	. . . . 5 ⊢ (𝐻 ∈ 𝑉 → (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))}) ∈ V)
39		simpr 476	. . . . . . 7 ⊢ ((𝐻 ∈ 𝑉 ∧ 𝑖 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})) → 𝑖 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))}))
40		oveq2 6557	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑥 → (𝑐 − 𝑎) = (𝑐 − 𝑥))
41		oveq2 6557	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑥 → (𝑏 − 𝑎) = (𝑏 − 𝑥))
42	41	oveq2d 6565	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑥 → (𝑘 · (𝑏 − 𝑎)) = (𝑘 · (𝑏 − 𝑥)))
43	40, 42	eqeq12d 2625	. . . . . . . . . 10 ⊢ (𝑎 = 𝑥 → ((𝑐 − 𝑎) = (𝑘 · (𝑏 − 𝑎)) ↔ (𝑐 − 𝑥) = (𝑘 · (𝑏 − 𝑥))))
44	43	rexbidv 3034	. . . . . . . . 9 ⊢ (𝑎 = 𝑥 → (∃𝑘 ∈ (0[,]1)(𝑐 − 𝑎) = (𝑘 · (𝑏 − 𝑎)) ↔ ∃𝑘 ∈ (0[,]1)(𝑐 − 𝑥) = (𝑘 · (𝑏 − 𝑥))))
45	44	rabbidv 3164	. . . . . . . 8 ⊢ (𝑎 = 𝑥 → {𝑐 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑐 − 𝑎) = (𝑘 · (𝑏 − 𝑎))} = {𝑐 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑐 − 𝑥) = (𝑘 · (𝑏 − 𝑥))})
46		oveq1 6556	. . . . . . . . . . . . 13 ⊢ (𝑏 = 𝑦 → (𝑏 − 𝑥) = (𝑦 − 𝑥))
47	46	oveq2d 6565	. . . . . . . . . . . 12 ⊢ (𝑏 = 𝑦 → (𝑘 · (𝑏 − 𝑥)) = (𝑘 · (𝑦 − 𝑥)))
48	47	eqeq2d 2620	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑦 → ((𝑐 − 𝑥) = (𝑘 · (𝑏 − 𝑥)) ↔ (𝑐 − 𝑥) = (𝑘 · (𝑦 − 𝑥))))
49	48	rexbidv 3034	. . . . . . . . . 10 ⊢ (𝑏 = 𝑦 → (∃𝑘 ∈ (0[,]1)(𝑐 − 𝑥) = (𝑘 · (𝑏 − 𝑥)) ↔ ∃𝑘 ∈ (0[,]1)(𝑐 − 𝑥) = (𝑘 · (𝑦 − 𝑥))))
50	49	rabbidv 3164	. . . . . . . . 9 ⊢ (𝑏 = 𝑦 → {𝑐 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑐 − 𝑥) = (𝑘 · (𝑏 − 𝑥))} = {𝑐 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑐 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})
51		oveq1 6556	. . . . . . . . . . . 12 ⊢ (𝑐 = 𝑧 → (𝑐 − 𝑥) = (𝑧 − 𝑥))
52	51	eqeq1d 2612	. . . . . . . . . . 11 ⊢ (𝑐 = 𝑧 → ((𝑐 − 𝑥) = (𝑘 · (𝑦 − 𝑥)) ↔ (𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))))
53	52	rexbidv 3034	. . . . . . . . . 10 ⊢ (𝑐 = 𝑧 → (∃𝑘 ∈ (0[,]1)(𝑐 − 𝑥) = (𝑘 · (𝑦 − 𝑥)) ↔ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))))
54	53	cbvrabv 3172	. . . . . . . . 9 ⊢ {𝑐 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑐 − 𝑥) = (𝑘 · (𝑦 − 𝑥))} = {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))}
55	50, 54	syl6eq 2660	. . . . . . . 8 ⊢ (𝑏 = 𝑦 → {𝑐 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑐 − 𝑥) = (𝑘 · (𝑏 − 𝑥))} = {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})
56	45, 55	cbvmpt2v 6633	. . . . . . 7 ⊢ (𝑎 ∈ 𝐵, 𝑏 ∈ 𝐵 ↦ {𝑐 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑐 − 𝑎) = (𝑘 · (𝑏 − 𝑎))}) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})
57	39, 56	syl6eqr 2662	. . . . . 6 ⊢ ((𝐻 ∈ 𝑉 ∧ 𝑖 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})) → 𝑖 = (𝑎 ∈ 𝐵, 𝑏 ∈ 𝐵 ↦ {𝑐 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑐 − 𝑎) = (𝑘 · (𝑏 − 𝑎))}))
58		simpr 476	. . . . . . . . . 10 ⊢ ((𝐻 ∈ 𝑉 ∧ 𝑖 = (𝑎 ∈ 𝐵, 𝑏 ∈ 𝐵 ↦ {𝑐 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑐 − 𝑎) = (𝑘 · (𝑏 − 𝑎))})) → 𝑖 = (𝑎 ∈ 𝐵, 𝑏 ∈ 𝐵 ↦ {𝑐 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑐 − 𝑎) = (𝑘 · (𝑏 − 𝑎))}))
59	58, 56	syl6eq 2660	. . . . . . . . 9 ⊢ ((𝐻 ∈ 𝑉 ∧ 𝑖 = (𝑎 ∈ 𝐵, 𝑏 ∈ 𝐵 ↦ {𝑐 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑐 − 𝑎) = (𝑘 · (𝑏 − 𝑎))})) → 𝑖 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))}))
60	59	opeq2d 4347	. . . . . . . 8 ⊢ ((𝐻 ∈ 𝑉 ∧ 𝑖 = (𝑎 ∈ 𝐵, 𝑏 ∈ 𝐵 ↦ {𝑐 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑐 − 𝑎) = (𝑘 · (𝑏 − 𝑎))})) → ⟨(Itv‘ndx), 𝑖⟩ = ⟨(Itv‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})⟩)
61	60	oveq2d 6565	. . . . . . 7 ⊢ ((𝐻 ∈ 𝑉 ∧ 𝑖 = (𝑎 ∈ 𝐵, 𝑏 ∈ 𝐵 ↦ {𝑐 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑐 − 𝑎) = (𝑘 · (𝑏 − 𝑎))})) → (𝐻 sSet ⟨(Itv‘ndx), 𝑖⟩) = (𝐻 sSet ⟨(Itv‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})⟩))
62	59	oveqd 6566	. . . . . . . . . . . 12 ⊢ ((𝐻 ∈ 𝑉 ∧ 𝑖 = (𝑎 ∈ 𝐵, 𝑏 ∈ 𝐵 ↦ {𝑐 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑐 − 𝑎) = (𝑘 · (𝑏 − 𝑎))})) → (𝑥𝑖𝑦) = (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦))
63	62	eleq2d 2673	. . . . . . . . . . 11 ⊢ ((𝐻 ∈ 𝑉 ∧ 𝑖 = (𝑎 ∈ 𝐵, 𝑏 ∈ 𝐵 ↦ {𝑐 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑐 − 𝑎) = (𝑘 · (𝑏 − 𝑎))})) → (𝑧 ∈ (𝑥𝑖𝑦) ↔ 𝑧 ∈ (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦)))
64	59	oveqd 6566	. . . . . . . . . . . 12 ⊢ ((𝐻 ∈ 𝑉 ∧ 𝑖 = (𝑎 ∈ 𝐵, 𝑏 ∈ 𝐵 ↦ {𝑐 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑐 − 𝑎) = (𝑘 · (𝑏 − 𝑎))})) → (𝑧𝑖𝑦) = (𝑧(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦))
65	64	eleq2d 2673	. . . . . . . . . . 11 ⊢ ((𝐻 ∈ 𝑉 ∧ 𝑖 = (𝑎 ∈ 𝐵, 𝑏 ∈ 𝐵 ↦ {𝑐 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑐 − 𝑎) = (𝑘 · (𝑏 − 𝑎))})) → (𝑥 ∈ (𝑧𝑖𝑦) ↔ 𝑥 ∈ (𝑧(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦)))
66	59	oveqd 6566	. . . . . . . . . . . 12 ⊢ ((𝐻 ∈ 𝑉 ∧ 𝑖 = (𝑎 ∈ 𝐵, 𝑏 ∈ 𝐵 ↦ {𝑐 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑐 − 𝑎) = (𝑘 · (𝑏 − 𝑎))})) → (𝑥𝑖𝑧) = (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑧))
67	66	eleq2d 2673	. . . . . . . . . . 11 ⊢ ((𝐻 ∈ 𝑉 ∧ 𝑖 = (𝑎 ∈ 𝐵, 𝑏 ∈ 𝐵 ↦ {𝑐 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑐 − 𝑎) = (𝑘 · (𝑏 − 𝑎))})) → (𝑦 ∈ (𝑥𝑖𝑧) ↔ 𝑦 ∈ (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑧)))
68	63, 65, 67	3orbi123d 1390	. . . . . . . . . 10 ⊢ ((𝐻 ∈ 𝑉 ∧ 𝑖 = (𝑎 ∈ 𝐵, 𝑏 ∈ 𝐵 ↦ {𝑐 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑐 − 𝑎) = (𝑘 · (𝑏 − 𝑎))})) → ((𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧)) ↔ (𝑧 ∈ (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦) ∨ 𝑥 ∈ (𝑧(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦) ∨ 𝑦 ∈ (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑧))))
69	68	rabbidv 3164	. . . . . . . . 9 ⊢ ((𝐻 ∈ 𝑉 ∧ 𝑖 = (𝑎 ∈ 𝐵, 𝑏 ∈ 𝐵 ↦ {𝑐 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑐 − 𝑎) = (𝑘 · (𝑏 − 𝑎))})) → {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))} = {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦) ∨ 𝑥 ∈ (𝑧(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦) ∨ 𝑦 ∈ (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑧))})
70	69	mpt2eq3dv 6619	. . . . . . . 8 ⊢ ((𝐻 ∈ 𝑉 ∧ 𝑖 = (𝑎 ∈ 𝐵, 𝑏 ∈ 𝐵 ↦ {𝑐 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑐 − 𝑎) = (𝑘 · (𝑏 − 𝑎))})) → (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))}) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦) ∨ 𝑥 ∈ (𝑧(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦) ∨ 𝑦 ∈ (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑧))}))
71	70	opeq2d 4347	. . . . . . 7 ⊢ ((𝐻 ∈ 𝑉 ∧ 𝑖 = (𝑎 ∈ 𝐵, 𝑏 ∈ 𝐵 ↦ {𝑐 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑐 − 𝑎) = (𝑘 · (𝑏 − 𝑎))})) → ⟨(LineG‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})⟩ = ⟨(LineG‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦) ∨ 𝑥 ∈ (𝑧(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦) ∨ 𝑦 ∈ (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑧))})⟩)
72	61, 71	oveq12d 6567	. . . . . 6 ⊢ ((𝐻 ∈ 𝑉 ∧ 𝑖 = (𝑎 ∈ 𝐵, 𝑏 ∈ 𝐵 ↦ {𝑐 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑐 − 𝑎) = (𝑘 · (𝑏 − 𝑎))})) → ((𝐻 sSet ⟨(Itv‘ndx), 𝑖⟩) sSet ⟨(LineG‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})⟩) = ((𝐻 sSet ⟨(Itv‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})⟩) sSet ⟨(LineG‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦) ∨ 𝑥 ∈ (𝑧(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦) ∨ 𝑦 ∈ (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑧))})⟩))
73	57, 72	syldan 486	. . . . 5 ⊢ ((𝐻 ∈ 𝑉 ∧ 𝑖 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})) → ((𝐻 sSet ⟨(Itv‘ndx), 𝑖⟩) sSet ⟨(LineG‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})⟩) = ((𝐻 sSet ⟨(Itv‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})⟩) sSet ⟨(LineG‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦) ∨ 𝑥 ∈ (𝑧(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦) ∨ 𝑦 ∈ (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑧))})⟩))
74	38, 73	csbied 3526	. . . 4 ⊢ (𝐻 ∈ 𝑉 → ⦋(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))}) / 𝑖⦌((𝐻 sSet ⟨(Itv‘ndx), 𝑖⟩) sSet ⟨(LineG‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})⟩) = ((𝐻 sSet ⟨(Itv‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})⟩) sSet ⟨(LineG‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦) ∨ 𝑥 ∈ (𝑧(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦) ∨ 𝑦 ∈ (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑧))})⟩))
75	2, 34, 74	3eqtrd 2648	. . 3 ⊢ (𝐻 ∈ 𝑉 → 𝐺 = ((𝐻 sSet ⟨(Itv‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})⟩) sSet ⟨(LineG‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦) ∨ 𝑥 ∈ (𝑧(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦) ∨ 𝑦 ∈ (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑧))})⟩))
76	75	fveq2d 6107	. . . . . . . . . . . 12 ⊢ (𝐻 ∈ 𝑉 → (Itv‘𝐺) = (Itv‘((𝐻 sSet ⟨(Itv‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})⟩) sSet ⟨(LineG‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦) ∨ 𝑥 ∈ (𝑧(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦) ∨ 𝑦 ∈ (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑧))})⟩)))
77		itvid 25141	. . . . . . . . . . . . 13 ⊢ Itv = Slot (Itv‘ndx)
78		1nn0 11185	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ ℕ₀
79		6nn 11066	. . . . . . . . . . . . . . . . 17 ⊢ 6 ∈ ℕ
80	78, 79	decnncl 11394	. . . . . . . . . . . . . . . 16 ⊢ ;16 ∈ ℕ
81	80	nnrei 10906	. . . . . . . . . . . . . . 15 ⊢ ;16 ∈ ℝ
82		6nn0 11190	. . . . . . . . . . . . . . . 16 ⊢ 6 ∈ ℕ₀
83		7nn 11067	. . . . . . . . . . . . . . . 16 ⊢ 7 ∈ ℕ
84		6lt7 11086	. . . . . . . . . . . . . . . 16 ⊢ 6 < 7
85	78, 82, 83, 84	declt 11406	. . . . . . . . . . . . . . 15 ⊢ ;16 < ;17
86	81, 85	ltneii 10029	. . . . . . . . . . . . . 14 ⊢ ;16 ≠ ;17
87		itvndx 25139	. . . . . . . . . . . . . . 15 ⊢ (Itv‘ndx) = ;16
88		lngndx 25140	. . . . . . . . . . . . . . 15 ⊢ (LineG‘ndx) = ;17
89	87, 88	neeq12i 2848	. . . . . . . . . . . . . 14 ⊢ ((Itv‘ndx) ≠ (LineG‘ndx) ↔ ;16 ≠ ;17)
90	86, 89	mpbir 220	. . . . . . . . . . . . 13 ⊢ (Itv‘ndx) ≠ (LineG‘ndx)
91	77, 90	setsnid 15743	. . . . . . . . . . . 12 ⊢ (Itv‘(𝐻 sSet ⟨(Itv‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})⟩)) = (Itv‘((𝐻 sSet ⟨(Itv‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})⟩) sSet ⟨(LineG‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦) ∨ 𝑥 ∈ (𝑧(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦) ∨ 𝑦 ∈ (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑧))})⟩))
92	76, 91	syl6eqr 2662	. . . . . . . . . . 11 ⊢ (𝐻 ∈ 𝑉 → (Itv‘𝐺) = (Itv‘(𝐻 sSet ⟨(Itv‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})⟩)))
93		ttgval.i	. . . . . . . . . . . 12 ⊢ 𝐼 = (Itv‘𝐺)
94	93	a1i 11	. . . . . . . . . . 11 ⊢ (𝐻 ∈ 𝑉 → 𝐼 = (Itv‘𝐺))
95	77	setsid 15742	. . . . . . . . . . . 12 ⊢ ((𝐻 ∈ 𝑉 ∧ (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))}) ∈ V) → (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))}) = (Itv‘(𝐻 sSet ⟨(Itv‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})⟩)))
96	37, 95	mpan2 703	. . . . . . . . . . 11 ⊢ (𝐻 ∈ 𝑉 → (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))}) = (Itv‘(𝐻 sSet ⟨(Itv‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})⟩)))
97	92, 94, 96	3eqtr4d 2654	. . . . . . . . . 10 ⊢ (𝐻 ∈ 𝑉 → 𝐼 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))}))
98	97	oveqd 6566	. . . . . . . . 9 ⊢ (𝐻 ∈ 𝑉 → (𝑥𝐼𝑦) = (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦))
99	98	eleq2d 2673	. . . . . . . 8 ⊢ (𝐻 ∈ 𝑉 → (𝑧 ∈ (𝑥𝐼𝑦) ↔ 𝑧 ∈ (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦)))
100	97	oveqd 6566	. . . . . . . . 9 ⊢ (𝐻 ∈ 𝑉 → (𝑧𝐼𝑦) = (𝑧(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦))
101	100	eleq2d 2673	. . . . . . . 8 ⊢ (𝐻 ∈ 𝑉 → (𝑥 ∈ (𝑧𝐼𝑦) ↔ 𝑥 ∈ (𝑧(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦)))
102	97	oveqd 6566	. . . . . . . . 9 ⊢ (𝐻 ∈ 𝑉 → (𝑥𝐼𝑧) = (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑧))
103	102	eleq2d 2673	. . . . . . . 8 ⊢ (𝐻 ∈ 𝑉 → (𝑦 ∈ (𝑥𝐼𝑧) ↔ 𝑦 ∈ (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑧)))
104	99, 101, 103	3orbi123d 1390	. . . . . . 7 ⊢ (𝐻 ∈ 𝑉 → ((𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)) ↔ (𝑧 ∈ (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦) ∨ 𝑥 ∈ (𝑧(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦) ∨ 𝑦 ∈ (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑧))))
105	104	rabbidv 3164	. . . . . 6 ⊢ (𝐻 ∈ 𝑉 → {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))} = {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦) ∨ 𝑥 ∈ (𝑧(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦) ∨ 𝑦 ∈ (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑧))})
106	105	mpt2eq3dv 6619	. . . . 5 ⊢ (𝐻 ∈ 𝑉 → (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))}) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦) ∨ 𝑥 ∈ (𝑧(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦) ∨ 𝑦 ∈ (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑧))}))
107	106	opeq2d 4347	. . . 4 ⊢ (𝐻 ∈ 𝑉 → ⟨(LineG‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))})⟩ = ⟨(LineG‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦) ∨ 𝑥 ∈ (𝑧(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦) ∨ 𝑦 ∈ (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑧))})⟩)
108	107	oveq2d 6565	. . 3 ⊢ (𝐻 ∈ 𝑉 → ((𝐻 sSet ⟨(Itv‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})⟩) sSet ⟨(LineG‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))})⟩) = ((𝐻 sSet ⟨(Itv‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})⟩) sSet ⟨(LineG‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦) ∨ 𝑥 ∈ (𝑧(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑦) ∨ 𝑦 ∈ (𝑥(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})𝑧))})⟩))
109	75, 108	eqtr4d 2647	. 2 ⊢ (𝐻 ∈ 𝑉 → 𝐺 = ((𝐻 sSet ⟨(Itv‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})⟩) sSet ⟨(LineG‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))})⟩))
110	109, 97	jca 553	1 ⊢ (𝐻 ∈ 𝑉 → (𝐺 = ((𝐻 sSet ⟨(Itv‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})⟩) sSet ⟨(LineG‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))})⟩) ∧ 𝐼 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ {𝑧 ∈ 𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 − 𝑥) = (𝑘 · (𝑦 − 𝑥))})))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 383 ∨ w3o 1030 = wceq 1475 ∈ wcel 1977 ≠ wne 2780 ∃wrex 2897 {crab 2900 Vcvv 3173 ⦋csb 3499 ⟨cop 4131 ‘cfv 5804 (class class class)co 6549 ↦ cmpt2 6551 0cc0 9815 1c1 9816 6c6 10951 7c7 10952 cdc 11369 [,]cicc 12049 ndxcnx 15692 sSet csts 15693 Basecbs 15695 ·_𝑠 cvsca 15772 -_gcsg 17247 Itvcitv 25135 LineGclng 25136 toTGcttg 25553

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-8 1979 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-rep 4699 ax-sep 4709 ax-nul 4717 ax-pow 4769 ax-pr 4833 ax-un 6847 ax-cnex 9871 ax-resscn 9872 ax-1cn 9873 ax-icn 9874 ax-addcl 9875 ax-addrcl 9876 ax-mulcl 9877 ax-mulrcl 9878 ax-mulcom 9879 ax-addass 9880 ax-mulass 9881 ax-distr 9882 ax-i2m1 9883 ax-1ne0 9884 ax-1rid 9885 ax-rnegex 9886 ax-rrecex 9887 ax-cnre 9888 ax-pre-lttri 9889 ax-pre-lttrn 9890 ax-pre-ltadd 9891 ax-pre-mulgt0 9892

This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3or 1032 df-3an 1033 df-tru 1478 df-fal 1481 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ne 2782 df-nel 2783 df-ral 2901 df-rex 2902 df-reu 2903 df-rab 2905 df-v 3175 df-sbc 3403 df-csb 3500 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-pss 3556 df-nul 3875 df-if 4037 df-pw 4110 df-sn 4126 df-pr 4128 df-tp 4130 df-op 4132 df-uni 4373 df-iun 4457 df-br 4584 df-opab 4644 df-mpt 4645 df-tr 4681 df-eprel 4949 df-id 4953 df-po 4959 df-so 4960 df-fr 4997 df-we 4999 df-xp 5044 df-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-rn 5049 df-res 5050 df-ima 5051 df-pred 5597 df-ord 5643 df-on 5644 df-lim 5645 df-suc 5646 df-iota 5768 df-fun 5806 df-fn 5807 df-f 5808 df-f1 5809 df-fo 5810 df-f1o 5811 df-fv 5812 df-riota 6511 df-ov 6552 df-oprab 6553 df-mpt2 6554 df-om 6958 df-1st 7059 df-2nd 7060 df-wrecs 7294 df-recs 7355 df-rdg 7393 df-er 7629 df-en 7842 df-dom 7843 df-sdom 7844 df-pnf 9955 df-mnf 9956 df-xr 9957 df-ltxr 9958 df-le 9959 df-sub 10147 df-neg 10148 df-nn 10898 df-2 10956 df-3 10957 df-4 10958 df-5 10959 df-6 10960 df-7 10961 df-8 10962 df-9 10963 df-n0 11170 df-dec 11370 df-ndx 15698 df-slot 15699 df-sets 15701 df-itv 25137 df-lng 25138 df-ttg 25554

This theorem is referenced by: ttglem 25556 ttgitvval 25562

W3C validator