Theorem dfprop2

Description: Every sentence of propositional calculus is either a variable encoded as a natural number, a negation of a sentence of propositional calculus, or an implication between two sentences of propositional calculus. (Contributed by Thomas van Maaren, 21-Aug-2026)

	Ref	Expression
Assertion	dfprop2	⊢ PROP ⊆ { 𝑥 ∣ ( ∃ 𝑧 ∈ PROP ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ PROP 𝑥 = ( 𝑤 prop→ 𝑧 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑥 = ( propvar ‘ 𝑛 ) ) }

Proof

Step	Hyp	Ref	Expression
1		df-prop	⊢ PROP = setrecs ( ( 𝑦 ∈ V ↦ { 𝑥 ∣ ( ∃ 𝑧 ∈ 𝑦 ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ 𝑦 𝑥 = ( 𝑤 prop→ 𝑧 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑥 = ( propvar ‘ 𝑛 ) ) } ) )
2		dfprop1	⊢ { 𝑥 ∣ ( ∃ 𝑧 ∈ PROP ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ PROP 𝑥 = ( 𝑤 prop→ 𝑧 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑥 = ( propvar ‘ 𝑛 ) ) } ⊆ PROP
3		sstr2	⊢ ( 𝑎 ⊆ { 𝑥 ∣ ( ∃ 𝑧 ∈ PROP ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ PROP 𝑥 = ( 𝑤 prop→ 𝑧 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑥 = ( propvar ‘ 𝑛 ) ) } → ( { 𝑥 ∣ ( ∃ 𝑧 ∈ PROP ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ PROP 𝑥 = ( 𝑤 prop→ 𝑧 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑥 = ( propvar ‘ 𝑛 ) ) } ⊆ PROP → 𝑎 ⊆ PROP ) )
4	2 3	mpi	⊢ ( 𝑎 ⊆ { 𝑥 ∣ ( ∃ 𝑧 ∈ PROP ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ PROP 𝑥 = ( 𝑤 prop→ 𝑧 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑥 = ( propvar ‘ 𝑛 ) ) } → 𝑎 ⊆ PROP )
5		rexeq	⊢ ( 𝑦 = 𝑎 → ( ∃ 𝑤 ∈ 𝑦 𝑥 = ( 𝑤 prop→ 𝑧 ) ↔ ∃ 𝑤 ∈ 𝑎 𝑥 = ( 𝑤 prop→ 𝑧 ) ) )
6	5	orbi2d	⊢ ( 𝑦 = 𝑎 → ( ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ 𝑦 𝑥 = ( 𝑤 prop→ 𝑧 ) ) ↔ ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ 𝑎 𝑥 = ( 𝑤 prop→ 𝑧 ) ) ) )
7	6	rexeqbi1dv	⊢ ( 𝑦 = 𝑎 → ( ∃ 𝑧 ∈ 𝑦 ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ 𝑦 𝑥 = ( 𝑤 prop→ 𝑧 ) ) ↔ ∃ 𝑧 ∈ 𝑎 ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ 𝑎 𝑥 = ( 𝑤 prop→ 𝑧 ) ) ) )
8	7	orbi1d	⊢ ( 𝑦 = 𝑎 → ( ( ∃ 𝑧 ∈ 𝑦 ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ 𝑦 𝑥 = ( 𝑤 prop→ 𝑧 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑥 = ( propvar ‘ 𝑛 ) ) ↔ ( ∃ 𝑧 ∈ 𝑎 ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ 𝑎 𝑥 = ( 𝑤 prop→ 𝑧 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑥 = ( propvar ‘ 𝑛 ) ) ) )
9	8	abbidv	⊢ ( 𝑦 = 𝑎 → { 𝑥 ∣ ( ∃ 𝑧 ∈ 𝑦 ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ 𝑦 𝑥 = ( 𝑤 prop→ 𝑧 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑥 = ( propvar ‘ 𝑛 ) ) } = { 𝑥 ∣ ( ∃ 𝑧 ∈ 𝑎 ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ 𝑎 𝑥 = ( 𝑤 prop→ 𝑧 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑥 = ( propvar ‘ 𝑛 ) ) } )
10		eqid	⊢ ( 𝑦 ∈ V ↦ { 𝑥 ∣ ( ∃ 𝑧 ∈ 𝑦 ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ 𝑦 𝑥 = ( 𝑤 prop→ 𝑧 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑥 = ( propvar ‘ 𝑛 ) ) } ) = ( 𝑦 ∈ V ↦ { 𝑥 ∣ ( ∃ 𝑧 ∈ 𝑦 ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ 𝑦 𝑥 = ( 𝑤 prop→ 𝑧 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑥 = ( propvar ‘ 𝑛 ) ) } )
11		vex	⊢ 𝑎 ∈ V
12	11	dfproplem	⊢ { 𝑥 ∣ ( ∃ 𝑧 ∈ 𝑎 ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ 𝑎 𝑥 = ( 𝑤 prop→ 𝑧 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑥 = ( propvar ‘ 𝑛 ) ) } ∈ V
13	9 10 12	fvmpt	⊢ ( 𝑎 ∈ V → ( ( 𝑦 ∈ V ↦ { 𝑥 ∣ ( ∃ 𝑧 ∈ 𝑦 ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ 𝑦 𝑥 = ( 𝑤 prop→ 𝑧 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑥 = ( propvar ‘ 𝑛 ) ) } ) ‘ 𝑎 ) = { 𝑥 ∣ ( ∃ 𝑧 ∈ 𝑎 ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ 𝑎 𝑥 = ( 𝑤 prop→ 𝑧 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑥 = ( propvar ‘ 𝑛 ) ) } )
14	13	elv	⊢ ( ( 𝑦 ∈ V ↦ { 𝑥 ∣ ( ∃ 𝑧 ∈ 𝑦 ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ 𝑦 𝑥 = ( 𝑤 prop→ 𝑧 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑥 = ( propvar ‘ 𝑛 ) ) } ) ‘ 𝑎 ) = { 𝑥 ∣ ( ∃ 𝑧 ∈ 𝑎 ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ 𝑎 𝑥 = ( 𝑤 prop→ 𝑧 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑥 = ( propvar ‘ 𝑛 ) ) }
15		ssrexv	⊢ ( 𝑎 ⊆ PROP → ( ∃ 𝑧 ∈ 𝑎 ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ 𝑎 𝑥 = ( 𝑤 prop→ 𝑧 ) ) → ∃ 𝑧 ∈ PROP ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ 𝑎 𝑥 = ( 𝑤 prop→ 𝑧 ) ) ) )
16	15	orim1d	⊢ ( 𝑎 ⊆ PROP → ( ( ∃ 𝑧 ∈ 𝑎 ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ 𝑎 𝑥 = ( 𝑤 prop→ 𝑧 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑥 = ( propvar ‘ 𝑛 ) ) → ( ∃ 𝑧 ∈ PROP ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ 𝑎 𝑥 = ( 𝑤 prop→ 𝑧 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑥 = ( propvar ‘ 𝑛 ) ) ) )
17		ssrexv	⊢ ( 𝑎 ⊆ PROP → ( ∃ 𝑤 ∈ 𝑎 𝑥 = ( 𝑤 prop→ 𝑧 ) → ∃ 𝑤 ∈ PROP 𝑥 = ( 𝑤 prop→ 𝑧 ) ) )
18	17	orim2d	⊢ ( 𝑎 ⊆ PROP → ( ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ 𝑎 𝑥 = ( 𝑤 prop→ 𝑧 ) ) → ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ PROP 𝑥 = ( 𝑤 prop→ 𝑧 ) ) ) )
19	18	reximdv	⊢ ( 𝑎 ⊆ PROP → ( ∃ 𝑧 ∈ PROP ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ 𝑎 𝑥 = ( 𝑤 prop→ 𝑧 ) ) → ∃ 𝑧 ∈ PROP ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ PROP 𝑥 = ( 𝑤 prop→ 𝑧 ) ) ) )
20	19	orim1d	⊢ ( 𝑎 ⊆ PROP → ( ( ∃ 𝑧 ∈ PROP ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ 𝑎 𝑥 = ( 𝑤 prop→ 𝑧 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑥 = ( propvar ‘ 𝑛 ) ) → ( ∃ 𝑧 ∈ PROP ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ PROP 𝑥 = ( 𝑤 prop→ 𝑧 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑥 = ( propvar ‘ 𝑛 ) ) ) )
21	16 20	syld	⊢ ( 𝑎 ⊆ PROP → ( ( ∃ 𝑧 ∈ 𝑎 ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ 𝑎 𝑥 = ( 𝑤 prop→ 𝑧 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑥 = ( propvar ‘ 𝑛 ) ) → ( ∃ 𝑧 ∈ PROP ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ PROP 𝑥 = ( 𝑤 prop→ 𝑧 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑥 = ( propvar ‘ 𝑛 ) ) ) )
22	21	ss2abdv	⊢ ( 𝑎 ⊆ PROP → { 𝑥 ∣ ( ∃ 𝑧 ∈ 𝑎 ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ 𝑎 𝑥 = ( 𝑤 prop→ 𝑧 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑥 = ( propvar ‘ 𝑛 ) ) } ⊆ { 𝑥 ∣ ( ∃ 𝑧 ∈ PROP ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ PROP 𝑥 = ( 𝑤 prop→ 𝑧 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑥 = ( propvar ‘ 𝑛 ) ) } )
23	14 22	eqsstrid	⊢ ( 𝑎 ⊆ PROP → ( ( 𝑦 ∈ V ↦ { 𝑥 ∣ ( ∃ 𝑧 ∈ 𝑦 ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ 𝑦 𝑥 = ( 𝑤 prop→ 𝑧 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑥 = ( propvar ‘ 𝑛 ) ) } ) ‘ 𝑎 ) ⊆ { 𝑥 ∣ ( ∃ 𝑧 ∈ PROP ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ PROP 𝑥 = ( 𝑤 prop→ 𝑧 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑥 = ( propvar ‘ 𝑛 ) ) } )
24	4 23	syl	⊢ ( 𝑎 ⊆ { 𝑥 ∣ ( ∃ 𝑧 ∈ PROP ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ PROP 𝑥 = ( 𝑤 prop→ 𝑧 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑥 = ( propvar ‘ 𝑛 ) ) } → ( ( 𝑦 ∈ V ↦ { 𝑥 ∣ ( ∃ 𝑧 ∈ 𝑦 ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ 𝑦 𝑥 = ( 𝑤 prop→ 𝑧 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑥 = ( propvar ‘ 𝑛 ) ) } ) ‘ 𝑎 ) ⊆ { 𝑥 ∣ ( ∃ 𝑧 ∈ PROP ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ PROP 𝑥 = ( 𝑤 prop→ 𝑧 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑥 = ( propvar ‘ 𝑛 ) ) } )
25	24	ax-gen	⊢ ∀ 𝑎 ( 𝑎 ⊆ { 𝑥 ∣ ( ∃ 𝑧 ∈ PROP ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ PROP 𝑥 = ( 𝑤 prop→ 𝑧 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑥 = ( propvar ‘ 𝑛 ) ) } → ( ( 𝑦 ∈ V ↦ { 𝑥 ∣ ( ∃ 𝑧 ∈ 𝑦 ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ 𝑦 𝑥 = ( 𝑤 prop→ 𝑧 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑥 = ( propvar ‘ 𝑛 ) ) } ) ‘ 𝑎 ) ⊆ { 𝑥 ∣ ( ∃ 𝑧 ∈ PROP ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ PROP 𝑥 = ( 𝑤 prop→ 𝑧 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑥 = ( propvar ‘ 𝑛 ) ) } )
26	25	a1i	⊢ ( ⊤ → ∀ 𝑎 ( 𝑎 ⊆ { 𝑥 ∣ ( ∃ 𝑧 ∈ PROP ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ PROP 𝑥 = ( 𝑤 prop→ 𝑧 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑥 = ( propvar ‘ 𝑛 ) ) } → ( ( 𝑦 ∈ V ↦ { 𝑥 ∣ ( ∃ 𝑧 ∈ 𝑦 ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ 𝑦 𝑥 = ( 𝑤 prop→ 𝑧 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑥 = ( propvar ‘ 𝑛 ) ) } ) ‘ 𝑎 ) ⊆ { 𝑥 ∣ ( ∃ 𝑧 ∈ PROP ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ PROP 𝑥 = ( 𝑤 prop→ 𝑧 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑥 = ( propvar ‘ 𝑛 ) ) } ) )
27	1 26	setrec2v	⊢ ( ⊤ → PROP ⊆ { 𝑥 ∣ ( ∃ 𝑧 ∈ PROP ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ PROP 𝑥 = ( 𝑤 prop→ 𝑧 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑥 = ( propvar ‘ 𝑛 ) ) } )
28	27	mptru	⊢ PROP ⊆ { 𝑥 ∣ ( ∃ 𝑧 ∈ PROP ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ PROP 𝑥 = ( 𝑤 prop→ 𝑧 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑥 = ( propvar ‘ 𝑛 ) ) }