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	⊢ 𝐴 ∈ V
Assertion	dfproplem	⊢ { 𝑥 ∣ ( ∃ 𝑧 ∈ 𝐴 ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ 𝐴 𝑥 = ( 𝑤 prop→ 𝑧 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑥 = ( propvar ‘ 𝑛 ) ) } ∈ V

Proof

Step	Hyp	Ref	Expression
1		dfproplem.a	⊢ 𝐴 ∈ V
2		df-iun	⊢ ∪ 𝑧 ∈ 𝐴 ( { ( prop¬ ‘ 𝑧 ) } ∪ ∪ 𝑤 ∈ 𝐴 { ( 𝑤 prop→ 𝑧 ) } ) = { 𝑥 ∣ ∃ 𝑧 ∈ 𝐴 𝑥 ∈ ( { ( prop¬ ‘ 𝑧 ) } ∪ ∪ 𝑤 ∈ 𝐴 { ( 𝑤 prop→ 𝑧 ) } ) }
3		df-sn	⊢ { ( prop¬ ‘ 𝑧 ) } = { 𝑥 ∣ 𝑥 = ( prop¬ ‘ 𝑧 ) }
4		iunsn	⊢ ∪ 𝑤 ∈ 𝐴 { ( 𝑤 prop→ 𝑧 ) } = { 𝑥 ∣ ∃ 𝑤 ∈ 𝐴 𝑥 = ( 𝑤 prop→ 𝑧 ) }
5	3 4	uneq12i	⊢ ( { ( prop¬ ‘ 𝑧 ) } ∪ ∪ 𝑤 ∈ 𝐴 { ( 𝑤 prop→ 𝑧 ) } ) = ( { 𝑥 ∣ 𝑥 = ( prop¬ ‘ 𝑧 ) } ∪ { 𝑥 ∣ ∃ 𝑤 ∈ 𝐴 𝑥 = ( 𝑤 prop→ 𝑧 ) } )
6		unab	⊢ ( { 𝑥 ∣ 𝑥 = ( prop¬ ‘ 𝑧 ) } ∪ { 𝑥 ∣ ∃ 𝑤 ∈ 𝐴 𝑥 = ( 𝑤 prop→ 𝑧 ) } ) = { 𝑥 ∣ ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ 𝐴 𝑥 = ( 𝑤 prop→ 𝑧 ) ) }
7	5 6	eqtri	⊢ ( { ( prop¬ ‘ 𝑧 ) } ∪ ∪ 𝑤 ∈ 𝐴 { ( 𝑤 prop→ 𝑧 ) } ) = { 𝑥 ∣ ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ 𝐴 𝑥 = ( 𝑤 prop→ 𝑧 ) ) }
8	7	eqabri	⊢ ( 𝑥 ∈ ( { ( prop¬ ‘ 𝑧 ) } ∪ ∪ 𝑤 ∈ 𝐴 { ( 𝑤 prop→ 𝑧 ) } ) ↔ ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ 𝐴 𝑥 = ( 𝑤 prop→ 𝑧 ) ) )
9	8	rexbii	⊢ ( ∃ 𝑧 ∈ 𝐴 𝑥 ∈ ( { ( prop¬ ‘ 𝑧 ) } ∪ ∪ 𝑤 ∈ 𝐴 { ( 𝑤 prop→ 𝑧 ) } ) ↔ ∃ 𝑧 ∈ 𝐴 ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ 𝐴 𝑥 = ( 𝑤 prop→ 𝑧 ) ) )
10	9	abbii	⊢ { 𝑥 ∣ ∃ 𝑧 ∈ 𝐴 𝑥 ∈ ( { ( prop¬ ‘ 𝑧 ) } ∪ ∪ 𝑤 ∈ 𝐴 { ( 𝑤 prop→ 𝑧 ) } ) } = { 𝑥 ∣ ∃ 𝑧 ∈ 𝐴 ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ 𝐴 𝑥 = ( 𝑤 prop→ 𝑧 ) ) }
11	2 10	eqtri	⊢ ∪ 𝑧 ∈ 𝐴 ( { ( prop¬ ‘ 𝑧 ) } ∪ ∪ 𝑤 ∈ 𝐴 { ( 𝑤 prop→ 𝑧 ) } ) = { 𝑥 ∣ ∃ 𝑧 ∈ 𝐴 ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ 𝐴 𝑥 = ( 𝑤 prop→ 𝑧 ) ) }
12		iunsn	⊢ ∪ 𝑛 ∈ ℕ { ( propvar ‘ 𝑛 ) } = { 𝑥 ∣ ∃ 𝑛 ∈ ℕ 𝑥 = ( propvar ‘ 𝑛 ) }
13	11 12	uneq12i	⊢ ( ∪ 𝑧 ∈ 𝐴 ( { ( prop¬ ‘ 𝑧 ) } ∪ ∪ 𝑤 ∈ 𝐴 { ( 𝑤 prop→ 𝑧 ) } ) ∪ ∪ 𝑛 ∈ ℕ { ( propvar ‘ 𝑛 ) } ) = ( { 𝑥 ∣ ∃ 𝑧 ∈ 𝐴 ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ 𝐴 𝑥 = ( 𝑤 prop→ 𝑧 ) ) } ∪ { 𝑥 ∣ ∃ 𝑛 ∈ ℕ 𝑥 = ( propvar ‘ 𝑛 ) } )
14		unab	⊢ ( { 𝑥 ∣ ∃ 𝑧 ∈ 𝐴 ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ 𝐴 𝑥 = ( 𝑤 prop→ 𝑧 ) ) } ∪ { 𝑥 ∣ ∃ 𝑛 ∈ ℕ 𝑥 = ( propvar ‘ 𝑛 ) } ) = { 𝑥 ∣ ( ∃ 𝑧 ∈ 𝐴 ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ 𝐴 𝑥 = ( 𝑤 prop→ 𝑧 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑥 = ( propvar ‘ 𝑛 ) ) }
15	13 14	eqtri	⊢ ( ∪ 𝑧 ∈ 𝐴 ( { ( prop¬ ‘ 𝑧 ) } ∪ ∪ 𝑤 ∈ 𝐴 { ( 𝑤 prop→ 𝑧 ) } ) ∪ ∪ 𝑛 ∈ ℕ { ( propvar ‘ 𝑛 ) } ) = { 𝑥 ∣ ( ∃ 𝑧 ∈ 𝐴 ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ 𝐴 𝑥 = ( 𝑤 prop→ 𝑧 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑥 = ( propvar ‘ 𝑛 ) ) }
16		snex	⊢ { ( prop¬ ‘ 𝑧 ) } ∈ V
17		snex	⊢ { ( 𝑤 prop→ 𝑧 ) } ∈ V
18	1 17	iunex	⊢ ∪ 𝑤 ∈ 𝐴 { ( 𝑤 prop→ 𝑧 ) } ∈ V
19	16 18	unex	⊢ ( { ( prop¬ ‘ 𝑧 ) } ∪ ∪ 𝑤 ∈ 𝐴 { ( 𝑤 prop→ 𝑧 ) } ) ∈ V
20	1 19	iunex	⊢ ∪ 𝑧 ∈ 𝐴 ( { ( prop¬ ‘ 𝑧 ) } ∪ ∪ 𝑤 ∈ 𝐴 { ( 𝑤 prop→ 𝑧 ) } ) ∈ V
21		nnex	⊢ ℕ ∈ V
22		snex	⊢ { ( propvar ‘ 𝑛 ) } ∈ V
23	21 22	iunex	⊢ ∪ 𝑛 ∈ ℕ { ( propvar ‘ 𝑛 ) } ∈ V
24	20 23	unex	⊢ ( ∪ 𝑧 ∈ 𝐴 ( { ( prop¬ ‘ 𝑧 ) } ∪ ∪ 𝑤 ∈ 𝐴 { ( 𝑤 prop→ 𝑧 ) } ) ∪ ∪ 𝑛 ∈ ℕ { ( propvar ‘ 𝑛 ) } ) ∈ V
25	15 24	eqeltrri	⊢ { 𝑥 ∣ ( ∃ 𝑧 ∈ 𝐴 ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ 𝐴 𝑥 = ( 𝑤 prop→ 𝑧 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑥 = ( propvar ‘ 𝑛 ) ) } ∈ V