Metamath Proof Explorer

Theorem varprop

Description: Variables encoded as natural numbers are sentences of propositional calculus. (Contributed by Thomas van Maaren, 21-Aug-2026)

Ref Expression
Assertion varprop 
|- ( n e. NN -> ( propvar ` n ) e. PROP )

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 0ex 
 |-  (/) e. _V
3 2 a1i 
 |-  ( n e. NN -> (/) e. _V )
4 0ss 
 |-  (/) C_ PROP
5 4 a1i 
 |-  ( n e. NN -> (/) C_ PROP )
6 1 3 5 setrec1 
 |-  ( n e. NN -> ( ( 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 ) ) } ) ` (/) ) C_ PROP )
7 rspe 
 |-  ( ( n e. NN /\ x = ( propvar ` n ) ) -> E. n e. NN x = ( propvar ` n ) )
8 7 olcd 
 |-  ( ( n e. NN /\ x = ( propvar ` n ) ) -> ( E. z e. (/) ( x = ( prop-. ` z ) \/ E. w e. (/) x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) )
9 8 ex 
 |-  ( n e. NN -> ( x = ( propvar ` n ) -> ( E. z e. (/) ( x = ( prop-. ` z ) \/ E. w e. (/) x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) ) )
10 9 alrimiv 
 |-  ( n e. NN -> A. x ( x = ( propvar ` n ) -> ( E. z e. (/) ( x = ( prop-. ` z ) \/ E. w e. (/) x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) ) )
11 fvex 
 |-  ( propvar ` n ) e. _V
12 elab6g 
 |-  ( ( propvar ` n ) e. _V -> ( ( propvar ` n ) e. { x | ( E. z e. (/) ( x = ( prop-. ` z ) \/ E. w e. (/) x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) } <-> A. x ( x = ( propvar ` n ) -> ( E. z e. (/) ( x = ( prop-. ` z ) \/ E. w e. (/) x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) ) ) )
13 11 12 ax-mp 
 |-  ( ( propvar ` n ) e. { x | ( E. z e. (/) ( x = ( prop-. ` z ) \/ E. w e. (/) x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) } <-> A. x ( x = ( propvar ` n ) -> ( E. z e. (/) ( x = ( prop-. ` z ) \/ E. w e. (/) x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) ) )
14 10 13 sylibr 
 |-  ( n e. NN -> ( propvar ` n ) e. { x | ( E. z e. (/) ( x = ( prop-. ` z ) \/ E. w e. (/) x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) } )
15 rexeq 
 |-  ( y = (/) -> ( E. w e. y x = ( w prop-> z ) <-> E. w e. (/) x = ( w prop-> z ) ) )
16 15 orbi2d 
 |-  ( y = (/) -> ( ( x = ( prop-. ` z ) \/ E. w e. y x = ( w prop-> z ) ) <-> ( x = ( prop-. ` z ) \/ E. w e. (/) x = ( w prop-> z ) ) ) )
17 16 rexeqbi1dv 
 |-  ( y = (/) -> ( E. z e. y ( x = ( prop-. ` z ) \/ E. w e. y x = ( w prop-> z ) ) <-> E. z e. (/) ( x = ( prop-. ` z ) \/ E. w e. (/) x = ( w prop-> z ) ) ) )
18 17 orbi1d 
 |-  ( y = (/) -> ( ( 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. (/) ( x = ( prop-. ` z ) \/ E. w e. (/) x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) ) )
19 18 abbidv 
 |-  ( y = (/) -> { 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. (/) ( x = ( prop-. ` z ) \/ E. w e. (/) x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) } )
20 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 ) ) } )
21 2 dfproplem 
 |-  { x | ( E. z e. (/) ( x = ( prop-. ` z ) \/ E. w e. (/) x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) } e. _V
22 19 20 21 fvmpt 
 |-  ( (/) 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 ) ) } ) ` (/) ) = { x | ( E. z e. (/) ( x = ( prop-. ` z ) \/ E. w e. (/) x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) } )
23 2 22 ax-mp 
 |-  ( ( 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 ) ) } ) ` (/) ) = { x | ( E. z e. (/) ( x = ( prop-. ` z ) \/ E. w e. (/) x = ( w prop-> z ) ) \/ E. n e. NN x = ( propvar ` n ) ) }
24 14 23 eleqtrrdi 
 |-  ( n e. NN -> ( propvar ` n ) e. ( ( 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 ) ) } ) ` (/) ) )
25 6 24 sseldd 
 |-  ( n e. NN -> ( propvar ` n ) e. PROP )