Metamath Proof Explorer

Theorem wl-mo3t

Description: Closed form of mo3 . (Contributed by Wolf Lammen, 18-Aug-2019)

Ref Expression
Assertion wl-mo3t ⊢ ∀ x Ⅎ y φ → ∃* x φ ↔ ∀ x ∀ y φ ∧ y x φ → x = y

Proof

Step Hyp Ref Expression
1 nfa1 ⊢ Ⅎ x ∀ x Ⅎ y φ
2 nfmo1 ⊢ Ⅎ x ∃* x φ
3 nfnf1 ⊢ Ⅎ y Ⅎ y φ
4 3 nfal ⊢ Ⅎ y ∀ x Ⅎ y φ
5 sp ⊢ ∀ x Ⅎ y φ → Ⅎ y φ
6 1 5 nfmodv ⊢ ∀ x Ⅎ y φ → Ⅎ y ∃* x φ
7 4 6 nfan1 ⊢ Ⅎ y ∀ x Ⅎ y φ ∧ ∃* x φ
8 dfmo ⊢ ∃* x φ ↔ ∃ u ∀ x φ → x = u
9 sp ⊢ ∀ x φ → x = u → φ → x = u
10 spsbim ⊢ ∀ x φ → x = u → y x φ → y x x = u
11 equsb3 ⊢ y x x = u ↔ y = u
12 10 11 imbitrdi ⊢ ∀ x φ → x = u → y x φ → y = u
13 9 12 anim12d ⊢ ∀ x φ → x = u → φ ∧ y x φ → x = u ∧ y = u
14 equtr2 ⊢ x = u ∧ y = u → x = y
15 13 14 syl6 ⊢ ∀ x φ → x = u → φ ∧ y x φ → x = y
16 15 exlimiv ⊢ ∃ u ∀ x φ → x = u → φ ∧ y x φ → x = y
17 8 16 sylbi ⊢ ∃* x φ → φ ∧ y x φ → x = y
18 17 adantl ⊢ ∀ x Ⅎ y φ ∧ ∃* x φ → φ ∧ y x φ → x = y
19 7 18 alrimi ⊢ ∀ x Ⅎ y φ ∧ ∃* x φ → ∀ y φ ∧ y x φ → x = y
20 19 ex ⊢ ∀ x Ⅎ y φ → ∃* x φ → ∀ y φ ∧ y x φ → x = y
21 1 2 20 alrimd ⊢ ∀ x Ⅎ y φ → ∃* x φ → ∀ x ∀ y φ ∧ y x φ → x = y
22 nfa1 ⊢ Ⅎ x ∀ x φ ∧ y x φ → x = y
23 nfs1v ⊢ Ⅎ x y x φ
24 pm3.3 ⊢ φ ∧ y x φ → x = y → φ → y x φ → x = y
25 24 com23 ⊢ φ ∧ y x φ → x = y → y x φ → φ → x = y
26 25 sps ⊢ ∀ x φ ∧ y x φ → x = y → y x φ → φ → x = y
27 22 23 26 alrimd ⊢ ∀ x φ ∧ y x φ → x = y → y x φ → ∀ x φ → x = y
28 27 aleximi ⊢ ∀ y ∀ x φ ∧ y x φ → x = y → ∃ y y x φ → ∃ y ∀ x φ → x = y
29 28 alcoms ⊢ ∀ x ∀ y φ ∧ y x φ → x = y → ∃ y y x φ → ∃ y ∀ x φ → x = y
30 moabs ⊢ ∃* x φ ↔ ∃ x φ → ∃* x φ
31 wl-sb8eft ⊢ ∀ x Ⅎ y φ → ∃ x φ ↔ ∃ y y x φ
32 wl-mo2t ⊢ ∀ x Ⅎ y φ → ∃* x φ ↔ ∃ y ∀ x φ → x = y
33 31 32 imbi12d ⊢ ∀ x Ⅎ y φ → ∃ x φ → ∃* x φ ↔ ∃ y y x φ → ∃ y ∀ x φ → x = y
34 30 33 bitrid ⊢ ∀ x Ⅎ y φ → ∃* x φ ↔ ∃ y y x φ → ∃ y ∀ x φ → x = y
35 29 34 imbitrrid ⊢ ∀ x Ⅎ y φ → ∀ x ∀ y φ ∧ y x φ → x = y → ∃* x φ
36 21 35 impbid ⊢ ∀ x Ⅎ y φ → ∃* x φ ↔ ∀ x ∀ y φ ∧ y x φ → x = y