Metamath Proof Explorer

Theorem negprop

Description: The negation of a sentence of propositional calculus is a sentence of propositional calculus. (Contributed by Thomas van Maaren, 21-Aug-2026)

Ref Expression
Assertion negprop 
|- ( x e. PROP -> ( prop-. ` x ) e. PROP )

Proof

Step Hyp Ref Expression
1 df-prop 
 |-  PROP = setrecs ( ( y e. _V |-> { u | ( E. z e. y ( u = ( prop-. ` z ) \/ E. w e. y u = ( w prop-> z ) ) \/ E. n e. NN u = ( propvar ` n ) ) } ) )
2 snexg 
 |-  ( x e. PROP -> { x } e. _V )
3 snssi 
 |-  ( x e. PROP -> { x } C_ PROP )
4 1 2 3 setrec1 
 |-  ( x e. PROP -> ( ( y e. _V |-> { u | ( E. z e. y ( u = ( prop-. ` z ) \/ E. w e. y u = ( w prop-> z ) ) \/ E. n e. NN u = ( propvar ` n ) ) } ) ` { x } ) C_ PROP )
5 velsn 
 |-  ( z e. { x } <-> z = x )
6 5 anbi1i 
 |-  ( ( z e. { x } /\ u = ( prop-. ` z ) ) <-> ( z = x /\ u = ( prop-. ` z ) ) )
7 6 exbii 
 |-  ( E. z ( z e. { x } /\ u = ( prop-. ` z ) ) <-> E. z ( z = x /\ u = ( prop-. ` z ) ) )
8 fveq2 
 |-  ( z = x -> ( prop-. ` z ) = ( prop-. ` x ) )
9 8 eqeq2d 
 |-  ( z = x -> ( u = ( prop-. ` z ) <-> u = ( prop-. ` x ) ) )
10 9 equsexvw 
 |-  ( E. z ( z = x /\ u = ( prop-. ` z ) ) <-> u = ( prop-. ` x ) )
11 7 10 bitri 
 |-  ( E. z ( z e. { x } /\ u = ( prop-. ` z ) ) <-> u = ( prop-. ` x ) )
12 11 bilanri 
 |-  ( ( x e. PROP /\ u = ( prop-. ` x ) ) -> E. z ( z e. { x } /\ u = ( prop-. ` z ) ) )
13 df-rex 
 |-  ( E. z e. { x } u = ( prop-. ` z ) <-> E. z ( z e. { x } /\ u = ( prop-. ` z ) ) )
14 13 biimpri 
 |-  ( E. z ( z e. { x } /\ u = ( prop-. ` z ) ) -> E. z e. { x } u = ( prop-. ` z ) )
15 orc 
 |-  ( u = ( prop-. ` z ) -> ( u = ( prop-. ` z ) \/ E. w e. { x } u = ( w prop-> z ) ) )
16 15 reximi 
 |-  ( E. z e. { x } u = ( prop-. ` z ) -> E. z e. { x } ( u = ( prop-. ` z ) \/ E. w e. { x } u = ( w prop-> z ) ) )
17 16 orcd 
 |-  ( E. z e. { x } u = ( prop-. ` z ) -> ( E. z e. { x } ( u = ( prop-. ` z ) \/ E. w e. { x } u = ( w prop-> z ) ) \/ E. n e. NN u = ( propvar ` n ) ) )
18 12 14 17 3syl 
 |-  ( ( x e. PROP /\ u = ( prop-. ` x ) ) -> ( E. z e. { x } ( u = ( prop-. ` z ) \/ E. w e. { x } u = ( w prop-> z ) ) \/ E. n e. NN u = ( propvar ` n ) ) )
19 18 ex 
 |-  ( x e. PROP -> ( u = ( prop-. ` x ) -> ( E. z e. { x } ( u = ( prop-. ` z ) \/ E. w e. { x } u = ( w prop-> z ) ) \/ E. n e. NN u = ( propvar ` n ) ) ) )
20 19 alrimiv 
 |-  ( x e. PROP -> A. u ( u = ( prop-. ` x ) -> ( E. z e. { x } ( u = ( prop-. ` z ) \/ E. w e. { x } u = ( w prop-> z ) ) \/ E. n e. NN u = ( propvar ` n ) ) ) )
21 fvex 
 |-  ( prop-. ` x ) e. _V
22 elab6g 
 |-  ( ( prop-. ` x ) e. _V -> ( ( prop-. ` x ) e. { u | ( E. z e. { x } ( u = ( prop-. ` z ) \/ E. w e. { x } u = ( w prop-> z ) ) \/ E. n e. NN u = ( propvar ` n ) ) } <-> A. u ( u = ( prop-. ` x ) -> ( E. z e. { x } ( u = ( prop-. ` z ) \/ E. w e. { x } u = ( w prop-> z ) ) \/ E. n e. NN u = ( propvar ` n ) ) ) ) )
23 21 22 ax-mp 
 |-  ( ( prop-. ` x ) e. { u | ( E. z e. { x } ( u = ( prop-. ` z ) \/ E. w e. { x } u = ( w prop-> z ) ) \/ E. n e. NN u = ( propvar ` n ) ) } <-> A. u ( u = ( prop-. ` x ) -> ( E. z e. { x } ( u = ( prop-. ` z ) \/ E. w e. { x } u = ( w prop-> z ) ) \/ E. n e. NN u = ( propvar ` n ) ) ) )
24 20 23 sylibr 
 |-  ( x e. PROP -> ( prop-. ` x ) e. { u | ( E. z e. { x } ( u = ( prop-. ` z ) \/ E. w e. { x } u = ( w prop-> z ) ) \/ E. n e. NN u = ( propvar ` n ) ) } )
25 vsnex 
 |-  { x } e. _V
26 rexeq 
 |-  ( y = { x } -> ( E. w e. y u = ( w prop-> z ) <-> E. w e. { x } u = ( w prop-> z ) ) )
27 26 orbi2d 
 |-  ( y = { x } -> ( ( u = ( prop-. ` z ) \/ E. w e. y u = ( w prop-> z ) ) <-> ( u = ( prop-. ` z ) \/ E. w e. { x } u = ( w prop-> z ) ) ) )
28 27 rexeqbi1dv 
 |-  ( y = { x } -> ( E. z e. y ( u = ( prop-. ` z ) \/ E. w e. y u = ( w prop-> z ) ) <-> E. z e. { x } ( u = ( prop-. ` z ) \/ E. w e. { x } u = ( w prop-> z ) ) ) )
29 28 orbi1d 
 |-  ( y = { x } -> ( ( E. z e. y ( u = ( prop-. ` z ) \/ E. w e. y u = ( w prop-> z ) ) \/ E. n e. NN u = ( propvar ` n ) ) <-> ( E. z e. { x } ( u = ( prop-. ` z ) \/ E. w e. { x } u = ( w prop-> z ) ) \/ E. n e. NN u = ( propvar ` n ) ) ) )
30 29 abbidv 
 |-  ( y = { x } -> { u | ( E. z e. y ( u = ( prop-. ` z ) \/ E. w e. y u = ( w prop-> z ) ) \/ E. n e. NN u = ( propvar ` n ) ) } = { u | ( E. z e. { x } ( u = ( prop-. ` z ) \/ E. w e. { x } u = ( w prop-> z ) ) \/ E. n e. NN u = ( propvar ` n ) ) } )
31 eqid 
 |-  ( y e. _V |-> { u | ( E. z e. y ( u = ( prop-. ` z ) \/ E. w e. y u = ( w prop-> z ) ) \/ E. n e. NN u = ( propvar ` n ) ) } ) = ( y e. _V |-> { u | ( E. z e. y ( u = ( prop-. ` z ) \/ E. w e. y u = ( w prop-> z ) ) \/ E. n e. NN u = ( propvar ` n ) ) } )
32 25 dfproplem 
 |-  { u | ( E. z e. { x } ( u = ( prop-. ` z ) \/ E. w e. { x } u = ( w prop-> z ) ) \/ E. n e. NN u = ( propvar ` n ) ) } e. _V
33 30 31 32 fvmpt 
 |-  ( { x } e. _V -> ( ( y e. _V |-> { u | ( E. z e. y ( u = ( prop-. ` z ) \/ E. w e. y u = ( w prop-> z ) ) \/ E. n e. NN u = ( propvar ` n ) ) } ) ` { x } ) = { u | ( E. z e. { x } ( u = ( prop-. ` z ) \/ E. w e. { x } u = ( w prop-> z ) ) \/ E. n e. NN u = ( propvar ` n ) ) } )
34 25 33 ax-mp 
 |-  ( ( y e. _V |-> { u | ( E. z e. y ( u = ( prop-. ` z ) \/ E. w e. y u = ( w prop-> z ) ) \/ E. n e. NN u = ( propvar ` n ) ) } ) ` { x } ) = { u | ( E. z e. { x } ( u = ( prop-. ` z ) \/ E. w e. { x } u = ( w prop-> z ) ) \/ E. n e. NN u = ( propvar ` n ) ) }
35 24 34 eleqtrrdi 
 |-  ( x e. PROP -> ( prop-. ` x ) e. ( ( y e. _V |-> { u | ( E. z e. y ( u = ( prop-. ` z ) \/ E. w e. y u = ( w prop-> z ) ) \/ E. n e. NN u = ( propvar ` n ) ) } ) ` { x } ) )
36 4 35 sseldd 
 |-  ( x e. PROP -> ( prop-. ` x ) e. PROP )