Metamath Proof Explorer

Theorem elmpst

Description: Property of being a pre-statement. (Contributed by Mario Carneiro, 18-Jul-2016)

Ref Expression
Hypotheses mpstval.v ⊢ 𝑉 = ( mDV ‘ 𝑇 )
mpstval.e ⊢ 𝐸 = ( mEx ‘ 𝑇 )
mpstval.p ⊢ 𝑃 = ( mPreSt ‘ 𝑇 )
Assertion elmpst ( ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝑃 ↔ ( ( 𝐷 ⊆ 𝑉 ∧ ◡ 𝐷 = 𝐷 ) ∧ ( 𝐻 ⊆ 𝐸 ∧ 𝐻 ∈ Fin ) ∧ 𝐴 ∈ 𝐸 ) )

Proof

Step Hyp Ref Expression
1 mpstval.v ⊢ 𝑉 = ( mDV ‘ 𝑇 )
2 mpstval.e ⊢ 𝐸 = ( mEx ‘ 𝑇 )
3 mpstval.p ⊢ 𝑃 = ( mPreSt ‘ 𝑇 )
4 opelxp ⊢ ( ⟨ ⟨ 𝐷 , 𝐻 ⟩ , 𝐴 ⟩ ∈ ( ( { 𝑑 ∈ 𝒫 𝑉 ∣ ◡ 𝑑 = 𝑑 } × ( 𝒫 𝐸 ∩ Fin ) ) × 𝐸 ) ↔ ( ⟨ 𝐷 , 𝐻 ⟩ ∈ ( { 𝑑 ∈ 𝒫 𝑉 ∣ ◡ 𝑑 = 𝑑 } × ( 𝒫 𝐸 ∩ Fin ) ) ∧ 𝐴 ∈ 𝐸 ) )
5 opelxp ⊢ ( ⟨ 𝐷 , 𝐻 ⟩ ∈ ( { 𝑑 ∈ 𝒫 𝑉 ∣ ◡ 𝑑 = 𝑑 } × ( 𝒫 𝐸 ∩ Fin ) ) ↔ ( 𝐷 ∈ { 𝑑 ∈ 𝒫 𝑉 ∣ ◡ 𝑑 = 𝑑 } ∧ 𝐻 ∈ ( 𝒫 𝐸 ∩ Fin ) ) )
6 cnveq ⊢ ( 𝑑 = 𝐷 → ◡ 𝑑 = ◡ 𝐷 )
7 id ⊢ ( 𝑑 = 𝐷 → 𝑑 = 𝐷 )
8 6 7 eqeq12d ⊢ ( 𝑑 = 𝐷 → ( ◡ 𝑑 = 𝑑 ↔ ◡ 𝐷 = 𝐷 ) )
9 8 elrab ⊢ ( 𝐷 ∈ { 𝑑 ∈ 𝒫 𝑉 ∣ ◡ 𝑑 = 𝑑 } ↔ ( 𝐷 ∈ 𝒫 𝑉 ∧ ◡ 𝐷 = 𝐷 ) )
10 1 fvexi ⊢ 𝑉 ∈ V
11 10 elpw2 ⊢ ( 𝐷 ∈ 𝒫 𝑉 ↔ 𝐷 ⊆ 𝑉 )
12 11 anbi1i ⊢ ( ( 𝐷 ∈ 𝒫 𝑉 ∧ ◡ 𝐷 = 𝐷 ) ↔ ( 𝐷 ⊆ 𝑉 ∧ ◡ 𝐷 = 𝐷 ) )
13 9 12 bitri ⊢ ( 𝐷 ∈ { 𝑑 ∈ 𝒫 𝑉 ∣ ◡ 𝑑 = 𝑑 } ↔ ( 𝐷 ⊆ 𝑉 ∧ ◡ 𝐷 = 𝐷 ) )
14 elfpw ⊢ ( 𝐻 ∈ ( 𝒫 𝐸 ∩ Fin ) ↔ ( 𝐻 ⊆ 𝐸 ∧ 𝐻 ∈ Fin ) )
15 13 14 anbi12i ⊢ ( ( 𝐷 ∈ { 𝑑 ∈ 𝒫 𝑉 ∣ ◡ 𝑑 = 𝑑 } ∧ 𝐻 ∈ ( 𝒫 𝐸 ∩ Fin ) ) ↔ ( ( 𝐷 ⊆ 𝑉 ∧ ◡ 𝐷 = 𝐷 ) ∧ ( 𝐻 ⊆ 𝐸 ∧ 𝐻 ∈ Fin ) ) )
16 5 15 bitri ⊢ ( ⟨ 𝐷 , 𝐻 ⟩ ∈ ( { 𝑑 ∈ 𝒫 𝑉 ∣ ◡ 𝑑 = 𝑑 } × ( 𝒫 𝐸 ∩ Fin ) ) ↔ ( ( 𝐷 ⊆ 𝑉 ∧ ◡ 𝐷 = 𝐷 ) ∧ ( 𝐻 ⊆ 𝐸 ∧ 𝐻 ∈ Fin ) ) )
17 16 anbi1i ⊢ ( ( ⟨ 𝐷 , 𝐻 ⟩ ∈ ( { 𝑑 ∈ 𝒫 𝑉 ∣ ◡ 𝑑 = 𝑑 } × ( 𝒫 𝐸 ∩ Fin ) ) ∧ 𝐴 ∈ 𝐸 ) ↔ ( ( ( 𝐷 ⊆ 𝑉 ∧ ◡ 𝐷 = 𝐷 ) ∧ ( 𝐻 ⊆ 𝐸 ∧ 𝐻 ∈ Fin ) ) ∧ 𝐴 ∈ 𝐸 ) )
18 4 17 bitri ⊢ ( ⟨ ⟨ 𝐷 , 𝐻 ⟩ , 𝐴 ⟩ ∈ ( ( { 𝑑 ∈ 𝒫 𝑉 ∣ ◡ 𝑑 = 𝑑 } × ( 𝒫 𝐸 ∩ Fin ) ) × 𝐸 ) ↔ ( ( ( 𝐷 ⊆ 𝑉 ∧ ◡ 𝐷 = 𝐷 ) ∧ ( 𝐻 ⊆ 𝐸 ∧ 𝐻 ∈ Fin ) ) ∧ 𝐴 ∈ 𝐸 ) )
19 df-ot ⊢ ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ = ⟨ ⟨ 𝐷 , 𝐻 ⟩ , 𝐴 ⟩
20 1 2 3 mpstval ⊢ 𝑃 = ( ( { 𝑑 ∈ 𝒫 𝑉 ∣ ◡ 𝑑 = 𝑑 } × ( 𝒫 𝐸 ∩ Fin ) ) × 𝐸 )
21 19 20 eleq12i ⊢ ( ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝑃 ↔ ⟨ ⟨ 𝐷 , 𝐻 ⟩ , 𝐴 ⟩ ∈ ( ( { 𝑑 ∈ 𝒫 𝑉 ∣ ◡ 𝑑 = 𝑑 } × ( 𝒫 𝐸 ∩ Fin ) ) × 𝐸 ) )
22 df-3an ⊢ ( ( ( 𝐷 ⊆ 𝑉 ∧ ◡ 𝐷 = 𝐷 ) ∧ ( 𝐻 ⊆ 𝐸 ∧ 𝐻 ∈ Fin ) ∧ 𝐴 ∈ 𝐸 ) ↔ ( ( ( 𝐷 ⊆ 𝑉 ∧ ◡ 𝐷 = 𝐷 ) ∧ ( 𝐻 ⊆ 𝐸 ∧ 𝐻 ∈ Fin ) ) ∧ 𝐴 ∈ 𝐸 ) )
23 18 21 22 3bitr4i ⊢ ( ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝑃 ↔ ( ( 𝐷 ⊆ 𝑉 ∧ ◡ 𝐷 = 𝐷 ) ∧ ( 𝐻 ⊆ 𝐸 ∧ 𝐻 ∈ Fin ) ∧ 𝐴 ∈ 𝐸 ) )