Metamath Proof Explorer


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 ) = 𝑌 ) ) )