Metamath Proof Explorer

Theorem elmpst

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

Ref Expression
Hypotheses mpstval.v ⊢ V = mDV ⁡ T
mpstval.e ⊢ E = mEx ⁡ T
mpstval.p ⊢ P = mPreSt ⁡ T
Assertion elmpst ⊢ D H A ∈ P ↔ D ⊆ V ∧ D -1 = D ∧ H ⊆ E ∧ H ∈ Fin ∧ A ∈ E

Proof

Step Hyp Ref Expression
1 mpstval.v ⊢ V = mDV ⁡ T
2 mpstval.e ⊢ E = mEx ⁡ T
3 mpstval.p ⊢ P = mPreSt ⁡ T
4 opelxp ⊢ D H A ∈ d ∈ 𝒫 V | d -1 = d × 𝒫 E ∩ Fin × E ↔ D H ∈ d ∈ 𝒫 V | d -1 = d × 𝒫 E ∩ Fin ∧ A ∈ E
5 opelxp ⊢ D H ∈ d ∈ 𝒫 V | d -1 = d × 𝒫 E ∩ Fin ↔ D ∈ d ∈ 𝒫 V | d -1 = d ∧ H ∈ 𝒫 E ∩ Fin
6 cnveq ⊢ d = D → d -1 = D -1
7 id ⊢ d = D → d = D
8 6 7 eqeq12d ⊢ d = D → d -1 = d ↔ D -1 = D
9 8 elrab ⊢ D ∈ d ∈ 𝒫 V | d -1 = d ↔ D ∈ 𝒫 V ∧ D -1 = D
10 1 fvexi ⊢ V ∈ V
11 10 elpw2 ⊢ D ∈ 𝒫 V ↔ D ⊆ V
12 11 anbi1i ⊢ D ∈ 𝒫 V ∧ D -1 = D ↔ D ⊆ V ∧ D -1 = D
13 9 12 bitri ⊢ D ∈ d ∈ 𝒫 V | d -1 = d ↔ D ⊆ V ∧ D -1 = D
14 elfpw ⊢ H ∈ 𝒫 E ∩ Fin ↔ H ⊆ E ∧ H ∈ Fin
15 13 14 anbi12i ⊢ D ∈ d ∈ 𝒫 V | d -1 = d ∧ H ∈ 𝒫 E ∩ Fin ↔ D ⊆ V ∧ D -1 = D ∧ H ⊆ E ∧ H ∈ Fin
16 5 15 bitri ⊢ D H ∈ d ∈ 𝒫 V | d -1 = d × 𝒫 E ∩ Fin ↔ D ⊆ V ∧ D -1 = D ∧ H ⊆ E ∧ H ∈ Fin
17 16 anbi1i ⊢ D H ∈ d ∈ 𝒫 V | d -1 = d × 𝒫 E ∩ Fin ∧ A ∈ E ↔ D ⊆ V ∧ D -1 = D ∧ H ⊆ E ∧ H ∈ Fin ∧ A ∈ E
18 4 17 bitri ⊢ D H A ∈ d ∈ 𝒫 V | d -1 = d × 𝒫 E ∩ Fin × E ↔ D ⊆ V ∧ D -1 = D ∧ H ⊆ E ∧ H ∈ Fin ∧ A ∈ E
19 df-ot ⊢ D H A = D H A
20 1 2 3 mpstval ⊢ P = d ∈ 𝒫 V | d -1 = d × 𝒫 E ∩ Fin × E
21 19 20 eleq12i ⊢ D H A ∈ P ↔ D H A ∈ d ∈ 𝒫 V | d -1 = d × 𝒫 E ∩ Fin × E
22 df-3an ⊢ D ⊆ V ∧ D -1 = D ∧ H ⊆ E ∧ H ∈ Fin ∧ A ∈ E ↔ D ⊆ V ∧ D -1 = D ∧ H ⊆ E ∧ H ∈ Fin ∧ A ∈ E
23 18 21 22 3bitr4i ⊢ D H A ∈ P ↔ D ⊆ V ∧ D -1 = D ∧ H ⊆ E ∧ H ∈ Fin ∧ A ∈ E