Metamath Proof Explorer

Theorem mo3

Description: Alternate definition of the at-most-one quantifier. Definition of BellMachover p. 460, except that definition has the side condition that y not occur in ph in place of our hypothesis. (Contributed by NM, 8-Mar-1995) (Proof shortened by Wolf Lammen, 18-Aug-2019) Remove dependency on ax-13 . (Revised by BJ and WL, 29-Jan-2023)

Ref Expression
Hypothesis mo3.nf ⊢ Ⅎ 𝑦 𝜑
Assertion mo3 ( ∃* 𝑥 𝜑 ↔ ∀ 𝑥 ∀ 𝑦 ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) )

Proof

Step Hyp Ref Expression
1 mo3.nf ⊢ Ⅎ 𝑦 𝜑
2 nfmo1 ⊢ Ⅎ 𝑥 ∃* 𝑥 𝜑
3 1 nfmov ⊢ Ⅎ 𝑦 ∃* 𝑥 𝜑
4 df-mo ⊢ ( ∃* 𝑥 𝜑 ↔ ∃ 𝑧 ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑧 ) )
5 sp ⊢ ( ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑧 ) → ( 𝜑 → 𝑥 = 𝑧 ) )
6 spsbim ⊢ ( ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑧 ) → ( [ 𝑦 / 𝑥 ] 𝜑 → [ 𝑦 / 𝑥 ] 𝑥 = 𝑧 ) )
7 equsb3 ⊢ ( [ 𝑦 / 𝑥 ] 𝑥 = 𝑧 ↔ 𝑦 = 𝑧 )
8 6 7 imbitrdi ⊢ ( ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑧 ) → ( [ 𝑦 / 𝑥 ] 𝜑 → 𝑦 = 𝑧 ) )
9 5 8 anim12d ⊢ ( ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑧 ) → ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑧 ) ) )
10 equtr2 ⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑧 ) → 𝑥 = 𝑦 )
11 9 10 syl6 ⊢ ( ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑧 ) → ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) )
12 11 exlimiv ⊢ ( ∃ 𝑧 ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑧 ) → ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) )
13 4 12 sylbi ⊢ ( ∃* 𝑥 𝜑 → ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) )
14 3 13 alrimi ⊢ ( ∃* 𝑥 𝜑 → ∀ 𝑦 ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) )
15 2 14 alrimi ⊢ ( ∃* 𝑥 𝜑 → ∀ 𝑥 ∀ 𝑦 ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) )
16 nfs1v ⊢ Ⅎ 𝑥 [ 𝑦 / 𝑥 ] 𝜑
17 pm3.21 ⊢ ( [ 𝑦 / 𝑥 ] 𝜑 → ( 𝜑 → ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) ) )
18 17 imim1d ⊢ ( [ 𝑦 / 𝑥 ] 𝜑 → ( ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) → ( 𝜑 → 𝑥 = 𝑦 ) ) )
19 16 18 alimd ⊢ ( [ 𝑦 / 𝑥 ] 𝜑 → ( ∀ 𝑥 ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) → ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) ) )
20 19 com12 ⊢ ( ∀ 𝑥 ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) → ( [ 𝑦 / 𝑥 ] 𝜑 → ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) ) )
21 20 aleximi ⊢ ( ∀ 𝑦 ∀ 𝑥 ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) → ( ∃ 𝑦 [ 𝑦 / 𝑥 ] 𝜑 → ∃ 𝑦 ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) ) )
22 1 sb8ef ⊢ ( ∃ 𝑥 𝜑 ↔ ∃ 𝑦 [ 𝑦 / 𝑥 ] 𝜑 )
23 1 mof ⊢ ( ∃* 𝑥 𝜑 ↔ ∃ 𝑦 ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) )
24 21 22 23 3imtr4g ⊢ ( ∀ 𝑦 ∀ 𝑥 ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) → ( ∃ 𝑥 𝜑 → ∃* 𝑥 𝜑 ) )
25 moabs ⊢ ( ∃* 𝑥 𝜑 ↔ ( ∃ 𝑥 𝜑 → ∃* 𝑥 𝜑 ) )
26 24 25 sylibr ⊢ ( ∀ 𝑦 ∀ 𝑥 ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) → ∃* 𝑥 𝜑 )
27 26 alcoms ⊢ ( ∀ 𝑥 ∀ 𝑦 ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) → ∃* 𝑥 𝜑 )
28 15 27 impbii ⊢ ( ∃* 𝑥 𝜑 ↔ ∀ 𝑥 ∀ 𝑦 ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) )