Metamath Proof Explorer

Theorem wl-df3maxtru1

Description: Assuming "(n+1)-maxtru1" <-> -. "(n+1)-mintru-2", we can deduce from the recursion formula given in wl-df-3mintru2 , that a similiar one

"(n+1)-maxtru1" <-> if- ( ph , -. "n-mintru-1" , "n-maxtru1" )

is valid for expressing 'at most one input is true'. This can also be rephrased as a mutual exclusivity of propositional expressions (no two of a sequence of inputs can simultaniously be true). Of course, this suggests that all inputs depend on variables et , ze ... Whatever wellformed expression we plugin for these variables, it will render at most one of the inputs true.

The here introduced mutual exclusivity is possibly useful for case studies, where we want the cases be sort of 'disjoint'. One can further imagine that a complete case scenario demands that the 'at most' is sharpened to 'exactly one'. This does not impose any difficulty here, as one of the inputs will then be the negation of all others be or'ed. As one input is determined, 'at most one' is sufficient to describe the general form here.

Since cadd is an alias for 'at least 2 out of three are true', its negation is under focus here. (Contributed by Wolf Lammen, 23-Jun-2024)

Ref Expression
Assertion wl-df3maxtru1 ⊢ ¬ cadd φ ψ χ ↔ if- φ ψ ⊽ χ ψ ⊼ χ

Proof

Step Hyp Ref Expression
1 cadnot ⊢ ¬ cadd φ ψ χ ↔ cadd ¬ φ ¬ ψ ¬ χ
2 wl-df-3mintru2 ⊢ cadd ¬ φ ¬ ψ ¬ χ ↔ if- ¬ φ ¬ ψ ∨ ¬ χ ¬ ψ ∧ ¬ χ
3 ifpn ⊢ if- φ ψ ⊽ χ ψ ⊼ χ ↔ if- ¬ φ ψ ⊼ χ ψ ⊽ χ
4 nanor ⊢ ψ ⊼ χ ↔ ¬ ψ ∨ ¬ χ
5 4 a1i ⊢ ⊤ → ψ ⊼ χ ↔ ¬ ψ ∨ ¬ χ
6 df-nor ⊢ ψ ⊽ χ ↔ ¬ ψ ∨ χ
7 ioran ⊢ ¬ ψ ∨ χ ↔ ¬ ψ ∧ ¬ χ
8 6 7 bitri ⊢ ψ ⊽ χ ↔ ¬ ψ ∧ ¬ χ
9 8 a1i ⊢ ⊤ → ψ ⊽ χ ↔ ¬ ψ ∧ ¬ χ
10 5 9 ifpbi23d ⊢ ⊤ → if- ¬ φ ψ ⊼ χ ψ ⊽ χ ↔ if- ¬ φ ¬ ψ ∨ ¬ χ ¬ ψ ∧ ¬ χ
11 10 mptru ⊢ if- ¬ φ ψ ⊼ χ ψ ⊽ χ ↔ if- ¬ φ ¬ ψ ∨ ¬ χ ¬ ψ ∧ ¬ χ
12 3 11 bitr2i ⊢ if- ¬ φ ¬ ψ ∨ ¬ χ ¬ ψ ∧ ¬ χ ↔ if- φ ψ ⊽ χ ψ ⊼ χ
13 1 2 12 3bitri ⊢ ¬ cadd φ ψ χ ↔ if- φ ψ ⊽ χ ψ ⊼ χ