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\in \mathrm{V}$$
Assertion	dfproplem	Could not format assertion : No typesetting found for |- { 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 with typecode |-

Proof

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