Metamath Proof Explorer

Definition df-prop

Description: Define the language of propositional calculus. This definition is noncircular. For a more usable and intuitive, but circular, definition see dfprop . (Contributed by Thomas van Maaren, 21-Aug-2026)

Ref Expression
Assertion 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 ) ) } ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cprop 
 |-  PROP
1 vy 
 |-  y
2 cvv 
 |-  _V
3 vx 
 |-  x
4 vz 
 |-  z
5 1 cv 
 |-  y
6 3 cv 
 |-  x
7 cpropneg 
 |-  prop-.
8 4 cv 
 |-  z
9 8 7 cfv 
 |-  ( prop-. ` z )
10 6 9 wceq 
 |-  x = ( prop-. ` z )
11 vw 
 |-  w
12 11 cv 
 |-  w
13 cpropimp 
 |-  prop->
14 12 8 13 co 
 |-  ( w prop-> z )
15 6 14 wceq 
 |-  x = ( w prop-> z )
16 15 11 5 wrex 
 |-  E. w e. y x = ( w prop-> z )
17 10 16 wo 
 |-  ( x = ( prop-. ` z ) \/ E. w e. y x = ( w prop-> z ) )
18 17 4 5 wrex 
 |-  E. z e. y ( x = ( prop-. ` z ) \/ E. w e. y x = ( w prop-> z ) )
19 vn 
 |-  n
20 cn 
 |-  NN
21 cpropvar 
 |-  propvar
22 19 cv 
 |-  n
23 22 21 cfv 
 |-  ( propvar ` n )
24 6 23 wceq 
 |-  x = ( propvar ` n )
25 24 19 20 wrex 
 |-  E. n e. NN x = ( propvar ` n )
26 18 25 wo 
 |-  ( E. z e. y ( x = ( prop-. ` z ) \/ E. w e. y x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) )
27 26 3 cab 
 |-  { x | ( E. z e. y ( x = ( prop-. ` z ) \/ E. w e. y x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) }
28 1 2 27 cmpt 
 |-  ( 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 ) ) } )
29 28 csetrecs 
 |-  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 ) ) } ) )
30 0 29 wceq 
 |-  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 ) ) } ) )