Definition df-prop

Description: Define the language of propositional calculus. This definition is noncircular. For a more usable and intuitive, but circular, definition see dfprop . (Contributed by Thomas van Maaren, 21-Aug-2026)

	Ref	Expression
Assertion	df-prop	⊢ PROP = setrecs ( ( 𝑦 ∈ V ↦ { 𝑥 ∣ ( ∃ 𝑧 ∈ 𝑦 ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ 𝑦 𝑥 = ( 𝑤 prop→ 𝑧 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑥 = ( propvar ‘ 𝑛 ) ) } ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cprop	⊢ PROP
1		vy	⊢ 𝑦
2		cvv	⊢ V
3		vx	⊢ 𝑥
4		vz	⊢ 𝑧
5	1	cv	⊢ 𝑦
6	3	cv	⊢ 𝑥
7		cpropneg	⊢ prop¬
8	4	cv	⊢ 𝑧
9	8 7	cfv	⊢ ( prop¬ ‘ 𝑧 )
10	6 9	wceq	⊢ 𝑥 = ( prop¬ ‘ 𝑧 )
11		vw	⊢ 𝑤
12	11	cv	⊢ 𝑤
13		cpropimp	⊢ prop→
14	12 8 13	co	⊢ ( 𝑤 prop→ 𝑧 )
15	6 14	wceq	⊢ 𝑥 = ( 𝑤 prop→ 𝑧 )
16	15 11 5	wrex	⊢ ∃ 𝑤 ∈ 𝑦 𝑥 = ( 𝑤 prop→ 𝑧 )
17	10 16	wo	⊢ ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ 𝑦 𝑥 = ( 𝑤 prop→ 𝑧 ) )
18	17 4 5	wrex	⊢ ∃ 𝑧 ∈ 𝑦 ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ 𝑦 𝑥 = ( 𝑤 prop→ 𝑧 ) )
19		vn	⊢ 𝑛
20		cn	⊢ ℕ
21		cpropvar	⊢ propvar
22	19	cv	⊢ 𝑛
23	22 21	cfv	⊢ ( propvar ‘ 𝑛 )
24	6 23	wceq	⊢ 𝑥 = ( propvar ‘ 𝑛 )
25	24 19 20	wrex	⊢ ∃ 𝑛 ∈ ℕ 𝑥 = ( propvar ‘ 𝑛 )
26	18 25	wo	⊢ ( ∃ 𝑧 ∈ 𝑦 ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ 𝑦 𝑥 = ( 𝑤 prop→ 𝑧 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑥 = ( propvar ‘ 𝑛 ) )
27	26 3	cab	⊢ { 𝑥 ∣ ( ∃ 𝑧 ∈ 𝑦 ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ 𝑦 𝑥 = ( 𝑤 prop→ 𝑧 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑥 = ( propvar ‘ 𝑛 ) ) }
28	1 2 27	cmpt	⊢ ( 𝑦 ∈ V ↦ { 𝑥 ∣ ( ∃ 𝑧 ∈ 𝑦 ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ 𝑦 𝑥 = ( 𝑤 prop→ 𝑧 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑥 = ( propvar ‘ 𝑛 ) ) } )
29	28	csetrecs	⊢ setrecs ( ( 𝑦 ∈ V ↦ { 𝑥 ∣ ( ∃ 𝑧 ∈ 𝑦 ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ 𝑦 𝑥 = ( 𝑤 prop→ 𝑧 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑥 = ( propvar ‘ 𝑛 ) ) } ) )
30	0 29	wceq	⊢ PROP = setrecs ( ( 𝑦 ∈ V ↦ { 𝑥 ∣ ( ∃ 𝑧 ∈ 𝑦 ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ 𝑦 𝑥 = ( 𝑤 prop→ 𝑧 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑥 = ( propvar ‘ 𝑛 ) ) } ) )