Theorem om1val

Description: The definition of the loop space. (Contributed by Mario Carneiro, 10-Jul-2015)

	Ref	Expression
Hypotheses	om1val.o	⊢ 𝑂 = ( 𝐽 Ω1 𝑌 )
	om1val.b	⊢ ( 𝜑 → 𝐵 = { 𝑓 ∈ ( II Cn 𝐽 ) ∣ ( ( 𝑓 ‘ 0 ) = 𝑌 ∧ ( 𝑓 ‘ 1 ) = 𝑌 ) } )
	om1val.p	⊢ ( 𝜑 → + = ( *𝑝 ‘ 𝐽 ) )
	om1val.k	⊢ ( 𝜑 → 𝐾 = ( 𝐽 ↑ko II ) )
	om1val.j	⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
	om1val.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑋 )
Assertion	om1val	⊢ ( 𝜑 → 𝑂 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐾 ⟩ } )

Proof

Step	Hyp	Ref	Expression
1		om1val.o	⊢ 𝑂 = ( 𝐽 Ω1 𝑌 )
2		om1val.b	⊢ ( 𝜑 → 𝐵 = { 𝑓 ∈ ( II Cn 𝐽 ) ∣ ( ( 𝑓 ‘ 0 ) = 𝑌 ∧ ( 𝑓 ‘ 1 ) = 𝑌 ) } )
3		om1val.p	⊢ ( 𝜑 → + = ( *𝑝 ‘ 𝐽 ) )
4		om1val.k	⊢ ( 𝜑 → 𝐾 = ( 𝐽 ↑ko II ) )
5		om1val.j	⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
6		om1val.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑋 )
7		df-om1	⊢ Ω1 = ( 𝑗 ∈ Top , 𝑦 ∈ ∪ 𝑗 ↦ { ⟨ ( Base ‘ ndx ) , { 𝑓 ∈ ( II Cn 𝑗 ) ∣ ( ( 𝑓 ‘ 0 ) = 𝑦 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) } ⟩ , ⟨ ( +g ‘ ndx ) , ( *𝑝 ‘ 𝑗 ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( 𝑗 ↑ko II ) ⟩ } )
8	7	a1i	⊢ ( 𝜑 → Ω1 = ( 𝑗 ∈ Top , 𝑦 ∈ ∪ 𝑗 ↦ { ⟨ ( Base ‘ ndx ) , { 𝑓 ∈ ( II Cn 𝑗 ) ∣ ( ( 𝑓 ‘ 0 ) = 𝑦 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) } ⟩ , ⟨ ( +g ‘ ndx ) , ( *𝑝 ‘ 𝑗 ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( 𝑗 ↑ko II ) ⟩ } ) )
9		simprl	⊢ ( ( 𝜑 ∧ ( 𝑗 = 𝐽 ∧ 𝑦 = 𝑌 ) ) → 𝑗 = 𝐽 )
10	9	oveq2d	⊢ ( ( 𝜑 ∧ ( 𝑗 = 𝐽 ∧ 𝑦 = 𝑌 ) ) → ( II Cn 𝑗 ) = ( II Cn 𝐽 ) )
11		simprr	⊢ ( ( 𝜑 ∧ ( 𝑗 = 𝐽 ∧ 𝑦 = 𝑌 ) ) → 𝑦 = 𝑌 )
12	11	eqeq2d	⊢ ( ( 𝜑 ∧ ( 𝑗 = 𝐽 ∧ 𝑦 = 𝑌 ) ) → ( ( 𝑓 ‘ 0 ) = 𝑦 ↔ ( 𝑓 ‘ 0 ) = 𝑌 ) )
13	11	eqeq2d	⊢ ( ( 𝜑 ∧ ( 𝑗 = 𝐽 ∧ 𝑦 = 𝑌 ) ) → ( ( 𝑓 ‘ 1 ) = 𝑦 ↔ ( 𝑓 ‘ 1 ) = 𝑌 ) )
14	12 13	anbi12d	⊢ ( ( 𝜑 ∧ ( 𝑗 = 𝐽 ∧ 𝑦 = 𝑌 ) ) → ( ( ( 𝑓 ‘ 0 ) = 𝑦 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) ↔ ( ( 𝑓 ‘ 0 ) = 𝑌 ∧ ( 𝑓 ‘ 1 ) = 𝑌 ) ) )
15	10 14	rabeqbidv	⊢ ( ( 𝜑 ∧ ( 𝑗 = 𝐽 ∧ 𝑦 = 𝑌 ) ) → { 𝑓 ∈ ( II Cn 𝑗 ) ∣ ( ( 𝑓 ‘ 0 ) = 𝑦 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) } = { 𝑓 ∈ ( II Cn 𝐽 ) ∣ ( ( 𝑓 ‘ 0 ) = 𝑌 ∧ ( 𝑓 ‘ 1 ) = 𝑌 ) } )
16	2	adantr	⊢ ( ( 𝜑 ∧ ( 𝑗 = 𝐽 ∧ 𝑦 = 𝑌 ) ) → 𝐵 = { 𝑓 ∈ ( II Cn 𝐽 ) ∣ ( ( 𝑓 ‘ 0 ) = 𝑌 ∧ ( 𝑓 ‘ 1 ) = 𝑌 ) } )
17	15 16	eqtr4d	⊢ ( ( 𝜑 ∧ ( 𝑗 = 𝐽 ∧ 𝑦 = 𝑌 ) ) → { 𝑓 ∈ ( II Cn 𝑗 ) ∣ ( ( 𝑓 ‘ 0 ) = 𝑦 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) } = 𝐵 )
18	17	opeq2d	⊢ ( ( 𝜑 ∧ ( 𝑗 = 𝐽 ∧ 𝑦 = 𝑌 ) ) → ⟨ ( Base ‘ ndx ) , { 𝑓 ∈ ( II Cn 𝑗 ) ∣ ( ( 𝑓 ‘ 0 ) = 𝑦 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) } ⟩ = ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ )
19	9	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝑗 = 𝐽 ∧ 𝑦 = 𝑌 ) ) → ( *𝑝 ‘ 𝑗 ) = ( *𝑝 ‘ 𝐽 ) )
20	3	adantr	⊢ ( ( 𝜑 ∧ ( 𝑗 = 𝐽 ∧ 𝑦 = 𝑌 ) ) → + = ( *𝑝 ‘ 𝐽 ) )
21	19 20	eqtr4d	⊢ ( ( 𝜑 ∧ ( 𝑗 = 𝐽 ∧ 𝑦 = 𝑌 ) ) → ( *𝑝 ‘ 𝑗 ) = + )
22	21	opeq2d	⊢ ( ( 𝜑 ∧ ( 𝑗 = 𝐽 ∧ 𝑦 = 𝑌 ) ) → ⟨ ( +g ‘ ndx ) , ( *𝑝 ‘ 𝑗 ) ⟩ = ⟨ ( +g ‘ ndx ) , + ⟩ )
23	9	oveq1d	⊢ ( ( 𝜑 ∧ ( 𝑗 = 𝐽 ∧ 𝑦 = 𝑌 ) ) → ( 𝑗 ↑ko II ) = ( 𝐽 ↑ko II ) )
24	4	adantr	⊢ ( ( 𝜑 ∧ ( 𝑗 = 𝐽 ∧ 𝑦 = 𝑌 ) ) → 𝐾 = ( 𝐽 ↑ko II ) )
25	23 24	eqtr4d	⊢ ( ( 𝜑 ∧ ( 𝑗 = 𝐽 ∧ 𝑦 = 𝑌 ) ) → ( 𝑗 ↑ko II ) = 𝐾 )
26	25	opeq2d	⊢ ( ( 𝜑 ∧ ( 𝑗 = 𝐽 ∧ 𝑦 = 𝑌 ) ) → ⟨ ( TopSet ‘ ndx ) , ( 𝑗 ↑ko II ) ⟩ = ⟨ ( TopSet ‘ ndx ) , 𝐾 ⟩ )
27	18 22 26	tpeq123d	⊢ ( ( 𝜑 ∧ ( 𝑗 = 𝐽 ∧ 𝑦 = 𝑌 ) ) → { ⟨ ( Base ‘ ndx ) , { 𝑓 ∈ ( II Cn 𝑗 ) ∣ ( ( 𝑓 ‘ 0 ) = 𝑦 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) } ⟩ , ⟨ ( +g ‘ ndx ) , ( *𝑝 ‘ 𝑗 ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( 𝑗 ↑ko II ) ⟩ } = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐾 ⟩ } )
28		unieq	⊢ ( 𝑗 = 𝐽 → ∪ 𝑗 = ∪ 𝐽 )
29	28	adantl	⊢ ( ( 𝜑 ∧ 𝑗 = 𝐽 ) → ∪ 𝑗 = ∪ 𝐽 )
30		toponuni	⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 )
31	5 30	syl	⊢ ( 𝜑 → 𝑋 = ∪ 𝐽 )
32	31	adantr	⊢ ( ( 𝜑 ∧ 𝑗 = 𝐽 ) → 𝑋 = ∪ 𝐽 )
33	29 32	eqtr4d	⊢ ( ( 𝜑 ∧ 𝑗 = 𝐽 ) → ∪ 𝑗 = 𝑋 )
34		topontop	⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐽 ∈ Top )
35	5 34	syl	⊢ ( 𝜑 → 𝐽 ∈ Top )
36		tpex	⊢ { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐾 ⟩ } ∈ V
37	36	a1i	⊢ ( 𝜑 → { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐾 ⟩ } ∈ V )
38	8 27 33 35 6 37	ovmpodx	⊢ ( 𝜑 → ( 𝐽 Ω1 𝑌 ) = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐾 ⟩ } )
39	1 38	syl5eq	⊢ ( 𝜑 → 𝑂 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐾 ⟩ } )