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 ⊢DHA∈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 ⊢DHA∈d∈𝒫V|d-1=d×𝒫E∩Fin×E↔DH∈d∈𝒫V|d-1=d×𝒫E∩Fin∧A∈E
5 opelxp ⊢DH∈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 ⊢DH∈d∈𝒫V|d-1=d×𝒫E∩Fin↔D⊆V∧D-1=D∧H⊆E∧H∈Fin
17 16 anbi1i ⊢DH∈d∈𝒫V|d-1=d×𝒫E∩Fin∧A∈E↔D⊆V∧D-1=D∧H⊆E∧H∈Fin∧A∈E
18 4 17 bitri ⊢DHA∈d∈𝒫V|d-1=d×𝒫E∩Fin×E↔D⊆V∧D-1=D∧H⊆E∧H∈Fin∧A∈E
19 df-ot ⊢DHA=DHA
20 1 2 3 mpstval ⊢P=d∈𝒫V|d-1=d×𝒫E∩Fin×E
21 19 20 eleq12i ⊢DHA∈P↔DHA∈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 ⊢DHA∈P↔D⊆V∧D-1=D∧H⊆E∧H∈Fin∧A∈E