Metamath Proof Explorer

Theorem dfprop2

Description: Every sentence of propositional calculus is either a variable encoded as a natural number, a negation of a sentence of propositional calculus, or an implication between two sentences of propositional calculus. (Contributed by Thomas van Maaren, 21-Aug-2026)

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

Proof

Step Hyp Ref Expression
1 df-prop 
 |-  PROP = setrecs ( ( y e. _V |-> { x | ( E. z e. y ( x = ( prop-. ` z ) \/ E. w e. y x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) } ) )
2 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
3 sstr2 
 |-  ( a C_ { x | ( E. z e. PROP ( x = ( prop-. ` z ) \/ E. w e. PROP x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) } -> ( { 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 -> a C_ PROP ) )
4 2 3 mpi 
 |-  ( a C_ { x | ( E. z e. PROP ( x = ( prop-. ` z ) \/ E. w e. PROP x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) } -> a C_ PROP )
5 rexeq 
 |-  ( y = a -> ( E. w e. y x = ( w prop-> z ) <-> E. w e. a x = ( w prop-> z ) ) )
6 5 orbi2d 
 |-  ( y = a -> ( ( x = ( prop-. ` z ) \/ E. w e. y x = ( w prop-> z ) ) <-> ( x = ( prop-. ` z ) \/ E. w e. a x = ( w prop-> z ) ) ) )
7 6 rexeqbi1dv 
 |-  ( y = a -> ( E. z e. y ( x = ( prop-. ` z ) \/ E. w e. y x = ( w prop-> z ) ) <-> E. z e. a ( x = ( prop-. ` z ) \/ E. w e. a x = ( w prop-> z ) ) ) )
8 7 orbi1d 
 |-  ( y = a -> ( ( E. z e. y ( x = ( prop-. ` z ) \/ E. w e. y x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) <-> ( E. z e. a ( x = ( prop-. ` z ) \/ E. w e. a x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) ) )
9 8 abbidv 
 |-  ( y = a -> { x | ( E. z e. y ( x = ( prop-. ` z ) \/ E. w e. y x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) } = { x | ( E. z e. a ( x = ( prop-. ` z ) \/ E. w e. a x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) } )
10 eqid 
 |-  ( y e. _V |-> { x | ( E. z e. y ( x = ( prop-. ` z ) \/ E. w e. y x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) } ) = ( y e. _V |-> { x | ( E. z e. y ( x = ( prop-. ` z ) \/ E. w e. y x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) } )
11 vex 
 |-  a e. _V
12 11 dfproplem 
 |-  { x | ( E. z e. a ( x = ( prop-. ` z ) \/ E. w e. a x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) } e. _V
13 9 10 12 fvmpt 
 |-  ( a e. _V -> ( ( y e. _V |-> { x | ( E. z e. y ( x = ( prop-. ` z ) \/ E. w e. y x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) } ) ` a ) = { x | ( E. z e. a ( x = ( prop-. ` z ) \/ E. w e. a x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) } )
14 13 elv 
 |-  ( ( y e. _V |-> { x | ( E. z e. y ( x = ( prop-. ` z ) \/ E. w e. y x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) } ) ` a ) = { x | ( E. z e. a ( x = ( prop-. ` z ) \/ E. w e. a x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) }
15 ssrexv 
 |-  ( a C_ PROP -> ( E. z e. a ( x = ( prop-. ` z ) \/ E. w e. a x = ( w prop-> z ) ) -> E. z e. PROP ( x = ( prop-. ` z ) \/ E. w e. a x = ( w prop-> z ) ) ) )
16 15 orim1d 
 |-  ( a C_ PROP -> ( ( E. z e. a ( x = ( prop-. ` z ) \/ E. w e. a x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) -> ( E. z e. PROP ( x = ( prop-. ` z ) \/ E. w e. a x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) ) )
17 ssrexv 
 |-  ( a C_ PROP -> ( E. w e. a x = ( w prop-> z ) -> E. w e. PROP x = ( w prop-> z ) ) )
18 17 orim2d 
 |-  ( a C_ PROP -> ( ( x = ( prop-. ` z ) \/ E. w e. a x = ( w prop-> z ) ) -> ( x = ( prop-. ` z ) \/ E. w e. PROP x = ( w prop-> z ) ) ) )
19 18 reximdv 
 |-  ( a C_ PROP -> ( E. z e. PROP ( x = ( prop-. ` z ) \/ E. w e. a x = ( w prop-> z ) ) -> E. z e. PROP ( x = ( prop-. ` z ) \/ E. w e. PROP x = ( w prop-> z ) ) ) )
20 19 orim1d 
 |-  ( a C_ PROP -> ( ( E. z e. PROP ( x = ( prop-. ` z ) \/ E. w e. a x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) -> ( E. z e. PROP ( x = ( prop-. ` z ) \/ E. w e. PROP x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) ) )
21 16 20 syld 
 |-  ( a C_ PROP -> ( ( E. z e. a ( x = ( prop-. ` z ) \/ E. w e. a x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) -> ( E. z e. PROP ( x = ( prop-. ` z ) \/ E. w e. PROP x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) ) )
22 21 ss2abdv 
 |-  ( a C_ PROP -> { x | ( E. z e. a ( x = ( prop-. ` z ) \/ E. w e. a x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) } C_ { x | ( E. z e. PROP ( x = ( prop-. ` z ) \/ E. w e. PROP x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) } )
23 14 22 eqsstrid 
 |-  ( a C_ PROP -> ( ( y e. _V |-> { x | ( E. z e. y ( x = ( prop-. ` z ) \/ E. w e. y x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) } ) ` a ) C_ { x | ( E. z e. PROP ( x = ( prop-. ` z ) \/ E. w e. PROP x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) } )
24 4 23 syl 
 |-  ( a C_ { x | ( E. z e. PROP ( x = ( prop-. ` z ) \/ E. w e. PROP x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) } -> ( ( y e. _V |-> { x | ( E. z e. y ( x = ( prop-. ` z ) \/ E. w e. y x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) } ) ` a ) C_ { x | ( E. z e. PROP ( x = ( prop-. ` z ) \/ E. w e. PROP x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) } )
25 24 ax-gen 
 |-  A. a ( a C_ { x | ( E. z e. PROP ( x = ( prop-. ` z ) \/ E. w e. PROP x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) } -> ( ( y e. _V |-> { x | ( E. z e. y ( x = ( prop-. ` z ) \/ E. w e. y x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) } ) ` a ) C_ { x | ( E. z e. PROP ( x = ( prop-. ` z ) \/ E. w e. PROP x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) } )
26 25 a1i 
 |-  ( T. -> A. a ( a C_ { x | ( E. z e. PROP ( x = ( prop-. ` z ) \/ E. w e. PROP x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) } -> ( ( y e. _V |-> { x | ( E. z e. y ( x = ( prop-. ` z ) \/ E. w e. y x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) } ) ` a ) C_ { x | ( E. z e. PROP ( x = ( prop-. ` z ) \/ E. w e. PROP x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) } ) )
27 1 26 setrec2v 
 |-  ( T. -> PROP C_ { x | ( E. z e. PROP ( x = ( prop-. ` z ) \/ E. w e. PROP x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) } )
28 27 mptru 
 |-  PROP C_ { x | ( E. z e. PROP ( x = ( prop-. ` z ) \/ E. w e. PROP x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) }