Metamath Proof Explorer

Theorem dfprop1

Description: The set of variables encoded as a natural number, negations of sentences of propositional calculus, and implications between sentences of propositional calculus is a subset of PROP . (Contributed by Thomas van Maaren, 21-Aug-2026)

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

Proof

Step Hyp Ref Expression
1 simpr ⊢ ( ( 𝑧 ∈ PROP ∧ 𝑥 = ( prop¬ ‘ 𝑧 ) ) → 𝑥 = ( prop¬ ‘ 𝑧 ) )
2 negprop ⊢ ( 𝑧 ∈ PROP → ( prop¬ ‘ 𝑧 ) ∈ PROP )
3 2 adantr ⊢ ( ( 𝑧 ∈ PROP ∧ 𝑥 = ( prop¬ ‘ 𝑧 ) ) → ( prop¬ ‘ 𝑧 ) ∈ PROP )
4 1 3 eqeltrd ⊢ ( ( 𝑧 ∈ PROP ∧ 𝑥 = ( prop¬ ‘ 𝑧 ) ) → 𝑥 ∈ PROP )
5 df-rex ⊢ ( ∃ 𝑤 ∈ PROP 𝑥 = ( 𝑤 prop→ 𝑧 ) ↔ ∃ 𝑤 ( 𝑤 ∈ PROP ∧ 𝑥 = ( 𝑤 prop→ 𝑧 ) ) )
6 5 anbi2i ⊢ ( ( 𝑧 ∈ PROP ∧ ∃ 𝑤 ∈ PROP 𝑥 = ( 𝑤 prop→ 𝑧 ) ) ↔ ( 𝑧 ∈ PROP ∧ ∃ 𝑤 ( 𝑤 ∈ PROP ∧ 𝑥 = ( 𝑤 prop→ 𝑧 ) ) ) )
7 19.42v ⊢ ( ∃ 𝑤 ( 𝑧 ∈ PROP ∧ ( 𝑤 ∈ PROP ∧ 𝑥 = ( 𝑤 prop→ 𝑧 ) ) ) ↔ ( 𝑧 ∈ PROP ∧ ∃ 𝑤 ( 𝑤 ∈ PROP ∧ 𝑥 = ( 𝑤 prop→ 𝑧 ) ) ) )
8 6 7 bitr4i ⊢ ( ( 𝑧 ∈ PROP ∧ ∃ 𝑤 ∈ PROP 𝑥 = ( 𝑤 prop→ 𝑧 ) ) ↔ ∃ 𝑤 ( 𝑧 ∈ PROP ∧ ( 𝑤 ∈ PROP ∧ 𝑥 = ( 𝑤 prop→ 𝑧 ) ) ) )
9 simprr ⊢ ( ( 𝑧 ∈ PROP ∧ ( 𝑤 ∈ PROP ∧ 𝑥 = ( 𝑤 prop→ 𝑧 ) ) ) → 𝑥 = ( 𝑤 prop→ 𝑧 ) )
10 simpl ⊢ ( ( 𝑤 ∈ PROP ∧ 𝑥 = ( 𝑤 prop→ 𝑧 ) ) → 𝑤 ∈ PROP )
11 simpl ⊢ ( ( 𝑧 ∈ PROP ∧ ( 𝑤 ∈ PROP ∧ 𝑥 = ( 𝑤 prop→ 𝑧 ) ) ) → 𝑧 ∈ PROP )
12 impprop ⊢ ( ( 𝑤 ∈ PROP ∧ 𝑧 ∈ PROP ) → ( 𝑤 prop→ 𝑧 ) ∈ PROP )
13 10 11 12 syl2an2 ⊢ ( ( 𝑧 ∈ PROP ∧ ( 𝑤 ∈ PROP ∧ 𝑥 = ( 𝑤 prop→ 𝑧 ) ) ) → ( 𝑤 prop→ 𝑧 ) ∈ PROP )
14 9 13 eqeltrd ⊢ ( ( 𝑧 ∈ PROP ∧ ( 𝑤 ∈ PROP ∧ 𝑥 = ( 𝑤 prop→ 𝑧 ) ) ) → 𝑥 ∈ PROP )
15 14 exlimiv ⊢ ( ∃ 𝑤 ( 𝑧 ∈ PROP ∧ ( 𝑤 ∈ PROP ∧ 𝑥 = ( 𝑤 prop→ 𝑧 ) ) ) → 𝑥 ∈ PROP )
16 8 15 sylbi ⊢ ( ( 𝑧 ∈ PROP ∧ ∃ 𝑤 ∈ PROP 𝑥 = ( 𝑤 prop→ 𝑧 ) ) → 𝑥 ∈ PROP )
17 4 16 jaodan ⊢ ( ( 𝑧 ∈ PROP ∧ ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ PROP 𝑥 = ( 𝑤 prop→ 𝑧 ) ) ) → 𝑥 ∈ PROP )
18 17 rexlimiva ⊢ ( ∃ 𝑧 ∈ PROP ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ PROP 𝑥 = ( 𝑤 prop→ 𝑧 ) ) → 𝑥 ∈ PROP )
19 simpr ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑥 = ( propvar ‘ 𝑛 ) ) → 𝑥 = ( propvar ‘ 𝑛 ) )
20 varprop ⊢ ( 𝑛 ∈ ℕ → ( propvar ‘ 𝑛 ) ∈ PROP )
21 20 adantr ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑥 = ( propvar ‘ 𝑛 ) ) → ( propvar ‘ 𝑛 ) ∈ PROP )
22 19 21 eqeltrd ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑥 = ( propvar ‘ 𝑛 ) ) → 𝑥 ∈ PROP )
23 22 rexlimiva ⊢ ( ∃ 𝑛 ∈ ℕ 𝑥 = ( propvar ‘ 𝑛 ) → 𝑥 ∈ PROP )
24 18 23 jaoi ⊢ ( ( ∃ 𝑧 ∈ PROP ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ PROP 𝑥 = ( 𝑤 prop→ 𝑧 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑥 = ( propvar ‘ 𝑛 ) ) → 𝑥 ∈ PROP )
25 24 abssi ⊢ { 𝑥 ∣ ( ∃ 𝑧 ∈ PROP ( 𝑥 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ PROP 𝑥 = ( 𝑤 prop→ 𝑧 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑥 = ( propvar ‘ 𝑛 ) ) } ⊆ PROP