Metamath Proof Explorer

Theorem negprop

Description: The negation of a sentence of propositional calculus is a sentence of propositional calculus. (Contributed by Thomas van Maaren, 21-Aug-2026)

Ref Expression
Assertion negprop ( 𝑥 ∈ PROP → ( prop¬ ‘ 𝑥 ) ∈ PROP )

Proof

Step Hyp Ref Expression
1 df-prop ⊢ PROP = setrecs ( ( 𝑦 ∈ V ↦ { 𝑢 ∣ ( ∃ 𝑧 ∈ 𝑦 ( 𝑢 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ 𝑦 𝑢 = ( 𝑤 prop→ 𝑧 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑢 = ( propvar ‘ 𝑛 ) ) } ) )
2 snexg ⊢ ( 𝑥 ∈ PROP → { 𝑥 } ∈ V )
3 snssi ⊢ ( 𝑥 ∈ PROP → { 𝑥 } ⊆ PROP )
4 1 2 3 setrec1 ⊢ ( 𝑥 ∈ PROP → ( ( 𝑦 ∈ V ↦ { 𝑢 ∣ ( ∃ 𝑧 ∈ 𝑦 ( 𝑢 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ 𝑦 𝑢 = ( 𝑤 prop→ 𝑧 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑢 = ( propvar ‘ 𝑛 ) ) } ) ‘ { 𝑥 } ) ⊆ PROP )
5 velsn ⊢ ( 𝑧 ∈ { 𝑥 } ↔ 𝑧 = 𝑥 )
6 5 anbi1i ⊢ ( ( 𝑧 ∈ { 𝑥 } ∧ 𝑢 = ( prop¬ ‘ 𝑧 ) ) ↔ ( 𝑧 = 𝑥 ∧ 𝑢 = ( prop¬ ‘ 𝑧 ) ) )
7 6 exbii ⊢ ( ∃ 𝑧 ( 𝑧 ∈ { 𝑥 } ∧ 𝑢 = ( prop¬ ‘ 𝑧 ) ) ↔ ∃ 𝑧 ( 𝑧 = 𝑥 ∧ 𝑢 = ( prop¬ ‘ 𝑧 ) ) )
8 fveq2 ⊢ ( 𝑧 = 𝑥 → ( prop¬ ‘ 𝑧 ) = ( prop¬ ‘ 𝑥 ) )
9 8 eqeq2d ⊢ ( 𝑧 = 𝑥 → ( 𝑢 = ( prop¬ ‘ 𝑧 ) ↔ 𝑢 = ( prop¬ ‘ 𝑥 ) ) )
10 9 equsexvw ⊢ ( ∃ 𝑧 ( 𝑧 = 𝑥 ∧ 𝑢 = ( prop¬ ‘ 𝑧 ) ) ↔ 𝑢 = ( prop¬ ‘ 𝑥 ) )
11 7 10 bitri ⊢ ( ∃ 𝑧 ( 𝑧 ∈ { 𝑥 } ∧ 𝑢 = ( prop¬ ‘ 𝑧 ) ) ↔ 𝑢 = ( prop¬ ‘ 𝑥 ) )
12 11 bilanri ⊢ ( ( 𝑥 ∈ PROP ∧ 𝑢 = ( prop¬ ‘ 𝑥 ) ) → ∃ 𝑧 ( 𝑧 ∈ { 𝑥 } ∧ 𝑢 = ( prop¬ ‘ 𝑧 ) ) )
13 df-rex ⊢ ( ∃ 𝑧 ∈ { 𝑥 } 𝑢 = ( prop¬ ‘ 𝑧 ) ↔ ∃ 𝑧 ( 𝑧 ∈ { 𝑥 } ∧ 𝑢 = ( prop¬ ‘ 𝑧 ) ) )
14 13 biimpri ⊢ ( ∃ 𝑧 ( 𝑧 ∈ { 𝑥 } ∧ 𝑢 = ( prop¬ ‘ 𝑧 ) ) → ∃ 𝑧 ∈ { 𝑥 } 𝑢 = ( prop¬ ‘ 𝑧 ) )
15 orc ⊢ ( 𝑢 = ( prop¬ ‘ 𝑧 ) → ( 𝑢 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ { 𝑥 } 𝑢 = ( 𝑤 prop→ 𝑧 ) ) )
16 15 reximi ⊢ ( ∃ 𝑧 ∈ { 𝑥 } 𝑢 = ( prop¬ ‘ 𝑧 ) → ∃ 𝑧 ∈ { 𝑥 } ( 𝑢 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ { 𝑥 } 𝑢 = ( 𝑤 prop→ 𝑧 ) ) )
17 16 orcd ⊢ ( ∃ 𝑧 ∈ { 𝑥 } 𝑢 = ( prop¬ ‘ 𝑧 ) → ( ∃ 𝑧 ∈ { 𝑥 } ( 𝑢 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ { 𝑥 } 𝑢 = ( 𝑤 prop→ 𝑧 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑢 = ( propvar ‘ 𝑛 ) ) )
18 12 14 17 3syl ⊢ ( ( 𝑥 ∈ PROP ∧ 𝑢 = ( prop¬ ‘ 𝑥 ) ) → ( ∃ 𝑧 ∈ { 𝑥 } ( 𝑢 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ { 𝑥 } 𝑢 = ( 𝑤 prop→ 𝑧 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑢 = ( propvar ‘ 𝑛 ) ) )
19 18 ex ⊢ ( 𝑥 ∈ PROP → ( 𝑢 = ( prop¬ ‘ 𝑥 ) → ( ∃ 𝑧 ∈ { 𝑥 } ( 𝑢 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ { 𝑥 } 𝑢 = ( 𝑤 prop→ 𝑧 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑢 = ( propvar ‘ 𝑛 ) ) ) )
20 19 alrimiv ⊢ ( 𝑥 ∈ PROP → ∀ 𝑢 ( 𝑢 = ( prop¬ ‘ 𝑥 ) → ( ∃ 𝑧 ∈ { 𝑥 } ( 𝑢 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ { 𝑥 } 𝑢 = ( 𝑤 prop→ 𝑧 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑢 = ( propvar ‘ 𝑛 ) ) ) )
21 fvex ⊢ ( prop¬ ‘ 𝑥 ) ∈ V
22 elab6g ⊢ ( ( prop¬ ‘ 𝑥 ) ∈ V → ( ( prop¬ ‘ 𝑥 ) ∈ { 𝑢 ∣ ( ∃ 𝑧 ∈ { 𝑥 } ( 𝑢 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ { 𝑥 } 𝑢 = ( 𝑤 prop→ 𝑧 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑢 = ( propvar ‘ 𝑛 ) ) } ↔ ∀ 𝑢 ( 𝑢 = ( prop¬ ‘ 𝑥 ) → ( ∃ 𝑧 ∈ { 𝑥 } ( 𝑢 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ { 𝑥 } 𝑢 = ( 𝑤 prop→ 𝑧 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑢 = ( propvar ‘ 𝑛 ) ) ) ) )
23 21 22 ax-mp ⊢ ( ( prop¬ ‘ 𝑥 ) ∈ { 𝑢 ∣ ( ∃ 𝑧 ∈ { 𝑥 } ( 𝑢 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ { 𝑥 } 𝑢 = ( 𝑤 prop→ 𝑧 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑢 = ( propvar ‘ 𝑛 ) ) } ↔ ∀ 𝑢 ( 𝑢 = ( prop¬ ‘ 𝑥 ) → ( ∃ 𝑧 ∈ { 𝑥 } ( 𝑢 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ { 𝑥 } 𝑢 = ( 𝑤 prop→ 𝑧 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑢 = ( propvar ‘ 𝑛 ) ) ) )
24 20 23 sylibr ⊢ ( 𝑥 ∈ PROP → ( prop¬ ‘ 𝑥 ) ∈ { 𝑢 ∣ ( ∃ 𝑧 ∈ { 𝑥 } ( 𝑢 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ { 𝑥 } 𝑢 = ( 𝑤 prop→ 𝑧 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑢 = ( propvar ‘ 𝑛 ) ) } )
25 vsnex ⊢ { 𝑥 } ∈ V
26 rexeq ⊢ ( 𝑦 = { 𝑥 } → ( ∃ 𝑤 ∈ 𝑦 𝑢 = ( 𝑤 prop→ 𝑧 ) ↔ ∃ 𝑤 ∈ { 𝑥 } 𝑢 = ( 𝑤 prop→ 𝑧 ) ) )
27 26 orbi2d ⊢ ( 𝑦 = { 𝑥 } → ( ( 𝑢 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ 𝑦 𝑢 = ( 𝑤 prop→ 𝑧 ) ) ↔ ( 𝑢 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ { 𝑥 } 𝑢 = ( 𝑤 prop→ 𝑧 ) ) ) )
28 27 rexeqbi1dv ⊢ ( 𝑦 = { 𝑥 } → ( ∃ 𝑧 ∈ 𝑦 ( 𝑢 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ 𝑦 𝑢 = ( 𝑤 prop→ 𝑧 ) ) ↔ ∃ 𝑧 ∈ { 𝑥 } ( 𝑢 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ { 𝑥 } 𝑢 = ( 𝑤 prop→ 𝑧 ) ) ) )
29 28 orbi1d ⊢ ( 𝑦 = { 𝑥 } → ( ( ∃ 𝑧 ∈ 𝑦 ( 𝑢 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ 𝑦 𝑢 = ( 𝑤 prop→ 𝑧 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑢 = ( propvar ‘ 𝑛 ) ) ↔ ( ∃ 𝑧 ∈ { 𝑥 } ( 𝑢 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ { 𝑥 } 𝑢 = ( 𝑤 prop→ 𝑧 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑢 = ( propvar ‘ 𝑛 ) ) ) )
30 29 abbidv ⊢ ( 𝑦 = { 𝑥 } → { 𝑢 ∣ ( ∃ 𝑧 ∈ 𝑦 ( 𝑢 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ 𝑦 𝑢 = ( 𝑤 prop→ 𝑧 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑢 = ( propvar ‘ 𝑛 ) ) } = { 𝑢 ∣ ( ∃ 𝑧 ∈ { 𝑥 } ( 𝑢 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ { 𝑥 } 𝑢 = ( 𝑤 prop→ 𝑧 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑢 = ( propvar ‘ 𝑛 ) ) } )
31 eqid ⊢ ( 𝑦 ∈ V ↦ { 𝑢 ∣ ( ∃ 𝑧 ∈ 𝑦 ( 𝑢 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ 𝑦 𝑢 = ( 𝑤 prop→ 𝑧 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑢 = ( propvar ‘ 𝑛 ) ) } ) = ( 𝑦 ∈ V ↦ { 𝑢 ∣ ( ∃ 𝑧 ∈ 𝑦 ( 𝑢 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ 𝑦 𝑢 = ( 𝑤 prop→ 𝑧 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑢 = ( propvar ‘ 𝑛 ) ) } )
32 25 dfproplem ⊢ { 𝑢 ∣ ( ∃ 𝑧 ∈ { 𝑥 } ( 𝑢 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ { 𝑥 } 𝑢 = ( 𝑤 prop→ 𝑧 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑢 = ( propvar ‘ 𝑛 ) ) } ∈ V
33 30 31 32 fvmpt ⊢ ( { 𝑥 } ∈ V → ( ( 𝑦 ∈ V ↦ { 𝑢 ∣ ( ∃ 𝑧 ∈ 𝑦 ( 𝑢 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ 𝑦 𝑢 = ( 𝑤 prop→ 𝑧 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑢 = ( propvar ‘ 𝑛 ) ) } ) ‘ { 𝑥 } ) = { 𝑢 ∣ ( ∃ 𝑧 ∈ { 𝑥 } ( 𝑢 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ { 𝑥 } 𝑢 = ( 𝑤 prop→ 𝑧 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑢 = ( propvar ‘ 𝑛 ) ) } )
34 25 33 ax-mp ⊢ ( ( 𝑦 ∈ V ↦ { 𝑢 ∣ ( ∃ 𝑧 ∈ 𝑦 ( 𝑢 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ 𝑦 𝑢 = ( 𝑤 prop→ 𝑧 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑢 = ( propvar ‘ 𝑛 ) ) } ) ‘ { 𝑥 } ) = { 𝑢 ∣ ( ∃ 𝑧 ∈ { 𝑥 } ( 𝑢 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ { 𝑥 } 𝑢 = ( 𝑤 prop→ 𝑧 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑢 = ( propvar ‘ 𝑛 ) ) }
35 24 34 eleqtrrdi ⊢ ( 𝑥 ∈ PROP → ( prop¬ ‘ 𝑥 ) ∈ ( ( 𝑦 ∈ V ↦ { 𝑢 ∣ ( ∃ 𝑧 ∈ 𝑦 ( 𝑢 = ( prop¬ ‘ 𝑧 ) ∨ ∃ 𝑤 ∈ 𝑦 𝑢 = ( 𝑤 prop→ 𝑧 ) ) ∨ ∃ 𝑛 ∈ ℕ 𝑢 = ( propvar ‘ 𝑛 ) ) } ) ‘ { 𝑥 } ) )
36 4 35 sseldd ⊢ ( 𝑥 ∈ PROP → ( prop¬ ‘ 𝑥 ) ∈ PROP )