Metamath Proof Explorer

Theorem dfproplem

Description: Given a set A, the set of all variables encoded as natural numbers, negations of elements in A, and implications between elements of A forms a set. This lemma is used when using fvmptd on the defining function of PROP . (Contributed by Thomas van Maaren, 21-Aug-2026)

Ref Expression
Hypothesis dfproplem.a 
|- A e. _V
Assertion 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

Proof

Step Hyp Ref Expression
1 dfproplem.a 
 |-  A e. _V
2 df-iun 
 |-  U_ z e. A ( { ( prop-. ` z ) } u. U_ w e. A { ( w prop-> z ) } ) = { x | E. z e. A x e. ( { ( prop-. ` z ) } u. U_ w e. A { ( w prop-> z ) } ) }
3 df-sn 
 |-  { ( prop-. ` z ) } = { x | x = ( prop-. ` z ) }
4 iunsn 
 |-  U_ w e. A { ( w prop-> z ) } = { x | E. w e. A x = ( w prop-> z ) }
5 3 4 uneq12i 
 |-  ( { ( prop-. ` z ) } u. U_ w e. A { ( w prop-> z ) } ) = ( { x | x = ( prop-. ` z ) } u. { x | E. w e. A x = ( w prop-> z ) } )
6 unab 
 |-  ( { x | x = ( prop-. ` z ) } u. { x | E. w e. A x = ( w prop-> z ) } ) = { x | ( x = ( prop-. ` z ) \/ E. w e. A x = ( w prop-> z ) ) }
7 5 6 eqtri 
 |-  ( { ( prop-. ` z ) } u. U_ w e. A { ( w prop-> z ) } ) = { x | ( x = ( prop-. ` z ) \/ E. w e. A x = ( w prop-> z ) ) }
8 7 eqabri 
 |-  ( x e. ( { ( prop-. ` z ) } u. U_ w e. A { ( w prop-> z ) } ) <-> ( x = ( prop-. ` z ) \/ E. w e. A x = ( w prop-> z ) ) )
9 8 rexbii 
 |-  ( E. z e. A x e. ( { ( prop-. ` z ) } u. U_ w e. A { ( w prop-> z ) } ) <-> E. z e. A ( x = ( prop-. ` z ) \/ E. w e. A x = ( w prop-> z ) ) )
10 9 abbii 
 |-  { x | E. z e. A x e. ( { ( prop-. ` z ) } u. U_ w e. A { ( w prop-> z ) } ) } = { x | E. z e. A ( x = ( prop-. ` z ) \/ E. w e. A x = ( w prop-> z ) ) }
11 2 10 eqtri 
 |-  U_ z e. A ( { ( prop-. ` z ) } u. U_ w e. A { ( w prop-> z ) } ) = { x | E. z e. A ( x = ( prop-. ` z ) \/ E. w e. A x = ( w prop-> z ) ) }
12 iunsn 
 |-  U_ n e. NN { ( propvar ` n ) } = { x | E. n e. NN x = ( propvar ` n ) }
13 11 12 uneq12i 
 |-  ( U_ z e. A ( { ( prop-. ` z ) } u. U_ w e. A { ( w prop-> z ) } ) u. U_ n e. NN { ( propvar ` n ) } ) = ( { x | E. z e. A ( x = ( prop-. ` z ) \/ E. w e. A x = ( w prop-> z ) ) } u. { x | E. n e. NN x = ( propvar ` n ) } )
14 unab 
 |-  ( { x | E. z e. A ( x = ( prop-. ` z ) \/ E. w e. A x = ( w prop-> z ) ) } u. { x | 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 ) ) }
15 13 14 eqtri 
 |-  ( U_ z e. A ( { ( prop-. ` z ) } u. U_ w e. A { ( w prop-> z ) } ) u. U_ n e. NN { ( 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 ) ) }
16 snex 
 |-  { ( prop-. ` z ) } e. _V
17 snex 
 |-  { ( w prop-> z ) } e. _V
18 1 17 iunex 
 |-  U_ w e. A { ( w prop-> z ) } e. _V
19 16 18 unex 
 |-  ( { ( prop-. ` z ) } u. U_ w e. A { ( w prop-> z ) } ) e. _V
20 1 19 iunex 
 |-  U_ z e. A ( { ( prop-. ` z ) } u. U_ w e. A { ( w prop-> z ) } ) e. _V
21 nnex 
 |-  NN e. _V
22 snex 
 |-  { ( propvar ` n ) } e. _V
23 21 22 iunex 
 |-  U_ n e. NN { ( propvar ` n ) } e. _V
24 20 23 unex 
 |-  ( U_ z e. A ( { ( prop-. ` z ) } u. U_ w e. A { ( w prop-> z ) } ) u. U_ n e. NN { ( propvar ` n ) } ) e. _V
25 15 24 eqeltrri 
 |-  { 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