Metamath Proof Explorer

Theorem dfprop1

Description: The set of variables encoded as a natural number, negations of sentences of propositional calculus, and implications between sentences of propositional calculus is a subset of PROP . (Contributed by Thomas van Maaren, 21-Aug-2026)

Ref Expression
Assertion dfprop1 
|- { x | ( E. z e. PROP ( x = ( prop-. ` z ) \/ E. w e. PROP x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) } C_ PROP

Proof

Step Hyp Ref Expression
1 simpr 
 |-  ( ( z e. PROP /\ x = ( prop-. ` z ) ) -> x = ( prop-. ` z ) )
2 negprop 
 |-  ( z e. PROP -> ( prop-. ` z ) e. PROP )
3 2 adantr 
 |-  ( ( z e. PROP /\ x = ( prop-. ` z ) ) -> ( prop-. ` z ) e. PROP )
4 1 3 eqeltrd 
 |-  ( ( z e. PROP /\ x = ( prop-. ` z ) ) -> x e. PROP )
5 df-rex 
 |-  ( E. w e. PROP x = ( w prop-> z ) <-> E. w ( w e. PROP /\ x = ( w prop-> z ) ) )
6 5 anbi2i 
 |-  ( ( z e. PROP /\ E. w e. PROP x = ( w prop-> z ) ) <-> ( z e. PROP /\ E. w ( w e. PROP /\ x = ( w prop-> z ) ) ) )
7 19.42v 
 |-  ( E. w ( z e. PROP /\ ( w e. PROP /\ x = ( w prop-> z ) ) ) <-> ( z e. PROP /\ E. w ( w e. PROP /\ x = ( w prop-> z ) ) ) )
8 6 7 bitr4i 
 |-  ( ( z e. PROP /\ E. w e. PROP x = ( w prop-> z ) ) <-> E. w ( z e. PROP /\ ( w e. PROP /\ x = ( w prop-> z ) ) ) )
9 simprr 
 |-  ( ( z e. PROP /\ ( w e. PROP /\ x = ( w prop-> z ) ) ) -> x = ( w prop-> z ) )
10 simpl 
 |-  ( ( w e. PROP /\ x = ( w prop-> z ) ) -> w e. PROP )
11 simpl 
 |-  ( ( z e. PROP /\ ( w e. PROP /\ x = ( w prop-> z ) ) ) -> z e. PROP )
12 impprop 
 |-  ( ( w e. PROP /\ z e. PROP ) -> ( w prop-> z ) e. PROP )
13 10 11 12 syl2an2 
 |-  ( ( z e. PROP /\ ( w e. PROP /\ x = ( w prop-> z ) ) ) -> ( w prop-> z ) e. PROP )
14 9 13 eqeltrd 
 |-  ( ( z e. PROP /\ ( w e. PROP /\ x = ( w prop-> z ) ) ) -> x e. PROP )
15 14 exlimiv 
 |-  ( E. w ( z e. PROP /\ ( w e. PROP /\ x = ( w prop-> z ) ) ) -> x e. PROP )
16 8 15 sylbi 
 |-  ( ( z e. PROP /\ E. w e. PROP x = ( w prop-> z ) ) -> x e. PROP )
17 4 16 jaodan 
 |-  ( ( z e. PROP /\ ( x = ( prop-. ` z ) \/ E. w e. PROP x = ( w prop-> z ) ) ) -> x e. PROP )
18 17 rexlimiva 
 |-  ( E. z e. PROP ( x = ( prop-. ` z ) \/ E. w e. PROP x = ( w prop-> z ) ) -> x e. PROP )
19 simpr 
 |-  ( ( n e. NN /\ x = ( propvar ` n ) ) -> x = ( propvar ` n ) )
20 varprop 
 |-  ( n e. NN -> ( propvar ` n ) e. PROP )
21 20 adantr 
 |-  ( ( n e. NN /\ x = ( propvar ` n ) ) -> ( propvar ` n ) e. PROP )
22 19 21 eqeltrd 
 |-  ( ( n e. NN /\ x = ( propvar ` n ) ) -> x e. PROP )
23 22 rexlimiva 
 |-  ( E. n e. NN x = ( propvar ` n ) -> x e. PROP )
24 18 23 jaoi 
 |-  ( ( E. z e. PROP ( x = ( prop-. ` z ) \/ E. w e. PROP x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) -> x e. PROP )
25 24 abssi 
 |-  { x | ( E. z e. PROP ( x = ( prop-. ` z ) \/ E. w e. PROP x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) } C_ PROP