Theorem om1elbas

Description: Elementhood in the base set of the loop space. (Contributed by Mario Carneiro, 10-Jul-2015)

	Ref	Expression
Hypotheses	om1bas.o	⊢ 𝑂 = ( 𝐽 Ω1 𝑌 )
	om1bas.j	⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
	om1bas.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑋 )
	om1bas.b	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑂 ) )
Assertion	om1elbas	⊢ ( 𝜑 → ( 𝐹 ∈ 𝐵 ↔ ( 𝐹 ∈ ( II Cn 𝐽 ) ∧ ( 𝐹 ‘ 0 ) = 𝑌 ∧ ( 𝐹 ‘ 1 ) = 𝑌 ) ) )

Proof

Step	Hyp	Ref	Expression
1		om1bas.o	⊢ 𝑂 = ( 𝐽 Ω1 𝑌 )
2		om1bas.j	⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
3		om1bas.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑋 )
4		om1bas.b	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑂 ) )
5	1 2 3 4	om1bas	⊢ ( 𝜑 → 𝐵 = { 𝑓 ∈ ( II Cn 𝐽 ) ∣ ( ( 𝑓 ‘ 0 ) = 𝑌 ∧ ( 𝑓 ‘ 1 ) = 𝑌 ) } )
6	5	eleq2d	⊢ ( 𝜑 → ( 𝐹 ∈ 𝐵 ↔ 𝐹 ∈ { 𝑓 ∈ ( II Cn 𝐽 ) ∣ ( ( 𝑓 ‘ 0 ) = 𝑌 ∧ ( 𝑓 ‘ 1 ) = 𝑌 ) } ) )
7		fveq1	⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ 0 ) = ( 𝐹 ‘ 0 ) )
8	7	eqeq1d	⊢ ( 𝑓 = 𝐹 → ( ( 𝑓 ‘ 0 ) = 𝑌 ↔ ( 𝐹 ‘ 0 ) = 𝑌 ) )
9		fveq1	⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ 1 ) = ( 𝐹 ‘ 1 ) )
10	9	eqeq1d	⊢ ( 𝑓 = 𝐹 → ( ( 𝑓 ‘ 1 ) = 𝑌 ↔ ( 𝐹 ‘ 1 ) = 𝑌 ) )
11	8 10	anbi12d	⊢ ( 𝑓 = 𝐹 → ( ( ( 𝑓 ‘ 0 ) = 𝑌 ∧ ( 𝑓 ‘ 1 ) = 𝑌 ) ↔ ( ( 𝐹 ‘ 0 ) = 𝑌 ∧ ( 𝐹 ‘ 1 ) = 𝑌 ) ) )
12	11	elrab	⊢ ( 𝐹 ∈ { 𝑓 ∈ ( II Cn 𝐽 ) ∣ ( ( 𝑓 ‘ 0 ) = 𝑌 ∧ ( 𝑓 ‘ 1 ) = 𝑌 ) } ↔ ( 𝐹 ∈ ( II Cn 𝐽 ) ∧ ( ( 𝐹 ‘ 0 ) = 𝑌 ∧ ( 𝐹 ‘ 1 ) = 𝑌 ) ) )
13		3anass	⊢ ( ( 𝐹 ∈ ( II Cn 𝐽 ) ∧ ( 𝐹 ‘ 0 ) = 𝑌 ∧ ( 𝐹 ‘ 1 ) = 𝑌 ) ↔ ( 𝐹 ∈ ( II Cn 𝐽 ) ∧ ( ( 𝐹 ‘ 0 ) = 𝑌 ∧ ( 𝐹 ‘ 1 ) = 𝑌 ) ) )
14	12 13	bitr4i	⊢ ( 𝐹 ∈ { 𝑓 ∈ ( II Cn 𝐽 ) ∣ ( ( 𝑓 ‘ 0 ) = 𝑌 ∧ ( 𝑓 ‘ 1 ) = 𝑌 ) } ↔ ( 𝐹 ∈ ( II Cn 𝐽 ) ∧ ( 𝐹 ‘ 0 ) = 𝑌 ∧ ( 𝐹 ‘ 1 ) = 𝑌 ) )
15	6 14	bitrdi	⊢ ( 𝜑 → ( 𝐹 ∈ 𝐵 ↔ ( 𝐹 ∈ ( II Cn 𝐽 ) ∧ ( 𝐹 ‘ 0 ) = 𝑌 ∧ ( 𝐹 ‘ 1 ) = 𝑌 ) ) )