Theorem wl-df3maxtru1 35357

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

"(n+1)-maxtru1" ↔ if-(𝜑,-. "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 𝜂, 𝜁... 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.)

Assertion

Ref	Expression
wl-df3maxtru1	⊢ (¬ cadd(𝜑, 𝜓, 𝜒) ↔ if-(𝜑, (𝜓 ⊽ 𝜒), (𝜓 ⊼ 𝜒)))

Proof of Theorem wl-df3maxtru1

Step	Hyp	Ref	Expression
1		cadnot 1622	. 2 ⊢ (¬ cadd(𝜑, 𝜓, 𝜒) ↔ cadd(¬ 𝜑, ¬ 𝜓, ¬ 𝜒))
2		wl-df-3mintru2 35349	. 2 ⊢ (cadd(¬ 𝜑, ¬ 𝜓, ¬ 𝜒) ↔ if-(¬ 𝜑, (¬ 𝜓 ∨ ¬ 𝜒), (¬ 𝜓 ∧ ¬ 𝜒)))
3		ifpn 1074	. . 3 ⊢ (if-(𝜑, (𝜓 ⊽ 𝜒), (𝜓 ⊼ 𝜒)) ↔ if-(¬ 𝜑, (𝜓 ⊼ 𝜒), (𝜓 ⊽ 𝜒)))
4		nanor 1491	. . . . . 6 ⊢ ((𝜓 ⊼ 𝜒) ↔ (¬ 𝜓 ∨ ¬ 𝜒))
5	4	a1i 11	. . . . 5 ⊢ (⊤ → ((𝜓 ⊼ 𝜒) ↔ (¬ 𝜓 ∨ ¬ 𝜒)))
6		df-nor 1527	. . . . . . 7 ⊢ ((𝜓 ⊽ 𝜒) ↔ ¬ (𝜓 ∨ 𝜒))
7		ioran 984	. . . . . . 7 ⊢ (¬ (𝜓 ∨ 𝜒) ↔ (¬ 𝜓 ∧ ¬ 𝜒))
8	6, 7	bitri 278	. . . . . 6 ⊢ ((𝜓 ⊽ 𝜒) ↔ (¬ 𝜓 ∧ ¬ 𝜒))
9	8	a1i 11	. . . . 5 ⊢ (⊤ → ((𝜓 ⊽ 𝜒) ↔ (¬ 𝜓 ∧ ¬ 𝜒)))
10	5, 9	ifpbi23d 1082	. . . 4 ⊢ (⊤ → (if-(¬ 𝜑, (𝜓 ⊼ 𝜒), (𝜓 ⊽ 𝜒)) ↔ if-(¬ 𝜑, (¬ 𝜓 ∨ ¬ 𝜒), (¬ 𝜓 ∧ ¬ 𝜒))))
11	10	mptru 1550	. . 3 ⊢ (if-(¬ 𝜑, (𝜓 ⊼ 𝜒), (𝜓 ⊽ 𝜒)) ↔ if-(¬ 𝜑, (¬ 𝜓 ∨ ¬ 𝜒), (¬ 𝜓 ∧ ¬ 𝜒)))
12	3, 11	bitr2i 279	. 2 ⊢ (if-(¬ 𝜑, (¬ 𝜓 ∨ ¬ 𝜒), (¬ 𝜓 ∧ ¬ 𝜒)) ↔ if-(𝜑, (𝜓 ⊽ 𝜒), (𝜓 ⊼ 𝜒)))
13	1, 2, 12	3bitri 300	1 ⊢ (¬ cadd(𝜑, 𝜓, 𝜒) ↔ if-(𝜑, (𝜓 ⊽ 𝜒), (𝜓 ⊼ 𝜒)))

Syntax hints:  ¬ wn 3   ↔ wb 209   ∧ wa 399   ∨ wo 847  if-wif 1063   ⊼ wnan 1487   ⊽ wnor 1526  ⊤wtru 1544  caddwcad 1613

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-ifp 1064  df-3or 1090  df-3an 1091  df-nan 1488  df-xor 1508  df-nor 1527  df-tru 1546  df-cad 1614

This theorem is referenced by: (None)