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	⊢ ( 𝑛 ∈ ℕ → ( propvar ‘ 𝑛 ) ∈ PROP )

Proof

Step	Hyp	Ref	Expression
1		df-prop	⊢ PROP = setrecs ( ( 𝑦 ∈ V ↦ { 𝑥 ∣ ( ∃ 𝑧 ∈ 𝑦 ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ 𝑦 𝑥 = ( 𝑤 prop→ 𝑧 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑥 = ( propvar ‘ 𝑛 ) ) } ) )
2		0ex	⊢ ∅ ∈ V
3	2	a1i	⊢ ( 𝑛 ∈ ℕ → ∅ ∈ V )
4		0ss	⊢ ∅ ⊆ PROP
5	4	a1i	⊢ ( 𝑛 ∈ ℕ → ∅ ⊆ PROP )
6	1 3 5	setrec1	⊢ ( 𝑛 ∈ ℕ → ( ( 𝑦 ∈ V ↦ { 𝑥 ∣ ( ∃ 𝑧 ∈ 𝑦 ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ 𝑦 𝑥 = ( 𝑤 prop→ 𝑧 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑥 = ( propvar ‘ 𝑛 ) ) } ) ‘ ∅ ) ⊆ PROP )
7		rspe	⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑥 = ( propvar ‘ 𝑛 ) ) → ∃ 𝑛 ∈ ℕ 𝑥 = ( propvar ‘ 𝑛 ) )
8	7	olcd	⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑥 = ( propvar ‘ 𝑛 ) ) → ( ∃ 𝑧 ∈ ∅ ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ ∅ 𝑥 = ( 𝑤 prop→ 𝑧 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑥 = ( propvar ‘ 𝑛 ) ) )
9	8	ex	⊢ ( 𝑛 ∈ ℕ → ( 𝑥 = ( propvar ‘ 𝑛 ) → ( ∃ 𝑧 ∈ ∅ ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ ∅ 𝑥 = ( 𝑤 prop→ 𝑧 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑥 = ( propvar ‘ 𝑛 ) ) ) )
10	9	alrimiv	⊢ ( 𝑛 ∈ ℕ → ∀ 𝑥 ( 𝑥 = ( propvar ‘ 𝑛 ) → ( ∃ 𝑧 ∈ ∅ ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ ∅ 𝑥 = ( 𝑤 prop→ 𝑧 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑥 = ( propvar ‘ 𝑛 ) ) ) )
11		fvex	⊢ ( propvar ‘ 𝑛 ) ∈ V
12		elab6g	⊢ ( ( propvar ‘ 𝑛 ) ∈ V → ( ( propvar ‘ 𝑛 ) ∈ { 𝑥 ∣ ( ∃ 𝑧 ∈ ∅ ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ ∅ 𝑥 = ( 𝑤 prop→ 𝑧 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑥 = ( propvar ‘ 𝑛 ) ) } ↔ ∀ 𝑥 ( 𝑥 = ( propvar ‘ 𝑛 ) → ( ∃ 𝑧 ∈ ∅ ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ ∅ 𝑥 = ( 𝑤 prop→ 𝑧 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑥 = ( propvar ‘ 𝑛 ) ) ) ) )
13	11 12	ax-mp	⊢ ( ( propvar ‘ 𝑛 ) ∈ { 𝑥 ∣ ( ∃ 𝑧 ∈ ∅ ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ ∅ 𝑥 = ( 𝑤 prop→ 𝑧 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑥 = ( propvar ‘ 𝑛 ) ) } ↔ ∀ 𝑥 ( 𝑥 = ( propvar ‘ 𝑛 ) → ( ∃ 𝑧 ∈ ∅ ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ ∅ 𝑥 = ( 𝑤 prop→ 𝑧 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑥 = ( propvar ‘ 𝑛 ) ) ) )
14	10 13	sylibr	⊢ ( 𝑛 ∈ ℕ → ( propvar ‘ 𝑛 ) ∈ { 𝑥 ∣ ( ∃ 𝑧 ∈ ∅ ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ ∅ 𝑥 = ( 𝑤 prop→ 𝑧 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑥 = ( propvar ‘ 𝑛 ) ) } )
15		rexeq	⊢ ( 𝑦 = ∅ → ( ∃ 𝑤 ∈ 𝑦 𝑥 = ( 𝑤 prop→ 𝑧 ) ↔ ∃ 𝑤 ∈ ∅ 𝑥 = ( 𝑤 prop→ 𝑧 ) ) )
16	15	orbi2d	⊢ ( 𝑦 = ∅ → ( ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ 𝑦 𝑥 = ( 𝑤 prop→ 𝑧 ) ) ↔ ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ ∅ 𝑥 = ( 𝑤 prop→ 𝑧 ) ) ) )
17	16	rexeqbi1dv	⊢ ( 𝑦 = ∅ → ( ∃ 𝑧 ∈ 𝑦 ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ 𝑦 𝑥 = ( 𝑤 prop→ 𝑧 ) ) ↔ ∃ 𝑧 ∈ ∅ ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ ∅ 𝑥 = ( 𝑤 prop→ 𝑧 ) ) ) )
18	17	orbi1d	⊢ ( 𝑦 = ∅ → ( ( ∃ 𝑧 ∈ 𝑦 ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ 𝑦 𝑥 = ( 𝑤 prop→ 𝑧 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑥 = ( propvar ‘ 𝑛 ) ) ↔ ( ∃ 𝑧 ∈ ∅ ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ ∅ 𝑥 = ( 𝑤 prop→ 𝑧 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑥 = ( propvar ‘ 𝑛 ) ) ) )
19	18	abbidv	⊢ ( 𝑦 = ∅ → { 𝑥 ∣ ( ∃ 𝑧 ∈ 𝑦 ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ 𝑦 𝑥 = ( 𝑤 prop→ 𝑧 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑥 = ( propvar ‘ 𝑛 ) ) } = { 𝑥 ∣ ( ∃ 𝑧 ∈ ∅ ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ ∅ 𝑥 = ( 𝑤 prop→ 𝑧 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑥 = ( propvar ‘ 𝑛 ) ) } )
20		eqid	⊢ ( 𝑦 ∈ V ↦ { 𝑥 ∣ ( ∃ 𝑧 ∈ 𝑦 ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ 𝑦 𝑥 = ( 𝑤 prop→ 𝑧 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑥 = ( propvar ‘ 𝑛 ) ) } ) = ( 𝑦 ∈ V ↦ { 𝑥 ∣ ( ∃ 𝑧 ∈ 𝑦 ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ 𝑦 𝑥 = ( 𝑤 prop→ 𝑧 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑥 = ( propvar ‘ 𝑛 ) ) } )
21	2	dfproplem	⊢ { 𝑥 ∣ ( ∃ 𝑧 ∈ ∅ ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ ∅ 𝑥 = ( 𝑤 prop→ 𝑧 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑥 = ( propvar ‘ 𝑛 ) ) } ∈ V
22	19 20 21	fvmpt	⊢ ( ∅ ∈ V → ( ( 𝑦 ∈ V ↦ { 𝑥 ∣ ( ∃ 𝑧 ∈ 𝑦 ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ 𝑦 𝑥 = ( 𝑤 prop→ 𝑧 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑥 = ( propvar ‘ 𝑛 ) ) } ) ‘ ∅ ) = { 𝑥 ∣ ( ∃ 𝑧 ∈ ∅ ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ ∅ 𝑥 = ( 𝑤 prop→ 𝑧 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑥 = ( propvar ‘ 𝑛 ) ) } )
23	2 22	ax-mp	⊢ ( ( 𝑦 ∈ V ↦ { 𝑥 ∣ ( ∃ 𝑧 ∈ 𝑦 ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ 𝑦 𝑥 = ( 𝑤 prop→ 𝑧 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑥 = ( propvar ‘ 𝑛 ) ) } ) ‘ ∅ ) = { 𝑥 ∣ ( ∃ 𝑧 ∈ ∅ ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ ∅ 𝑥 = ( 𝑤 prop→ 𝑧 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑥 = ( propvar ‘ 𝑛 ) ) }
24	14 23	eleqtrrdi	⊢ ( 𝑛 ∈ ℕ → ( propvar ‘ 𝑛 ) ∈ ( ( 𝑦 ∈ V ↦ { 𝑥 ∣ ( ∃ 𝑧 ∈ 𝑦 ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ 𝑦 𝑥 = ( 𝑤 prop→ 𝑧 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑥 = ( propvar ‘ 𝑛 ) ) } ) ‘ ∅ ) )
25	6 24	sseldd	⊢ ( 𝑛 ∈ ℕ → ( propvar ‘ 𝑛 ) ∈ PROP )