Metamath Proof Explorer

Theorem wl-mo3t

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

Ref Expression
Assertion wl-mo3t 
|- ( A. x F/ y ph -> ( E* x ph <-> A. x A. y ( ( ph /\ [ y / x ] ph ) -> x = y ) ) )

Proof

Step Hyp Ref Expression
1 nfa1 
 |-  F/ x A. x F/ y ph
2 nfmo1 
 |-  F/ x E* x ph
3 nfnf1 
 |-  F/ y F/ y ph
4 3 nfal 
 |-  F/ y A. x F/ y ph
5 sp 
 |-  ( A. x F/ y ph -> F/ y ph )
6 1 5 nfmod 
 |-  ( A. x F/ y ph -> F/ y E* x ph )
7 4 6 nfan1 
 |-  F/ y ( A. x F/ y ph /\ E* x ph )
8 df-mo 
 |-  ( E* x ph <-> E. u A. x ( ph -> x = u ) )
9 sp 
 |-  ( A. x ( ph -> x = u ) -> ( ph -> x = u ) )
10 spsbim 
 |-  ( A. x ( ph -> x = u ) -> ( [ y / x ] ph -> [ y / x ] x = u ) )
11 equsb3 
 |-  ( [ y / x ] x = u <-> y = u )
12 10 11 syl6ib 
 |-  ( A. x ( ph -> x = u ) -> ( [ y / x ] ph -> y = u ) )
13 9 12 anim12d 
 |-  ( A. x ( ph -> x = u ) -> ( ( ph /\ [ y / x ] ph ) -> ( x = u /\ y = u ) ) )
14 equtr2 
 |-  ( ( x = u /\ y = u ) -> x = y )
15 13 14 syl6 
 |-  ( A. x ( ph -> x = u ) -> ( ( ph /\ [ y / x ] ph ) -> x = y ) )
16 15 exlimiv 
 |-  ( E. u A. x ( ph -> x = u ) -> ( ( ph /\ [ y / x ] ph ) -> x = y ) )
17 8 16 sylbi 
 |-  ( E* x ph -> ( ( ph /\ [ y / x ] ph ) -> x = y ) )
18 17 adantl 
 |-  ( ( A. x F/ y ph /\ E* x ph ) -> ( ( ph /\ [ y / x ] ph ) -> x = y ) )
19 7 18 alrimi 
 |-  ( ( A. x F/ y ph /\ E* x ph ) -> A. y ( ( ph /\ [ y / x ] ph ) -> x = y ) )
20 19 ex 
 |-  ( A. x F/ y ph -> ( E* x ph -> A. y ( ( ph /\ [ y / x ] ph ) -> x = y ) ) )
21 1 2 20 alrimd 
 |-  ( A. x F/ y ph -> ( E* x ph -> A. x A. y ( ( ph /\ [ y / x ] ph ) -> x = y ) ) )
22 nfa1 
 |-  F/ x A. x ( ( ph /\ [ y / x ] ph ) -> x = y )
23 nfs1v 
 |-  F/ x [ y / x ] ph
24 pm3.3 
 |-  ( ( ( ph /\ [ y / x ] ph ) -> x = y ) -> ( ph -> ( [ y / x ] ph -> x = y ) ) )
25 24 com23 
 |-  ( ( ( ph /\ [ y / x ] ph ) -> x = y ) -> ( [ y / x ] ph -> ( ph -> x = y ) ) )
26 25 sps 
 |-  ( A. x ( ( ph /\ [ y / x ] ph ) -> x = y ) -> ( [ y / x ] ph -> ( ph -> x = y ) ) )
27 22 23 26 alrimd 
 |-  ( A. x ( ( ph /\ [ y / x ] ph ) -> x = y ) -> ( [ y / x ] ph -> A. x ( ph -> x = y ) ) )
28 27 aleximi 
 |-  ( A. y A. x ( ( ph /\ [ y / x ] ph ) -> x = y ) -> ( E. y [ y / x ] ph -> E. y A. x ( ph -> x = y ) ) )
29 28 alcoms 
 |-  ( A. x A. y ( ( ph /\ [ y / x ] ph ) -> x = y ) -> ( E. y [ y / x ] ph -> E. y A. x ( ph -> x = y ) ) )
30 moabs 
 |-  ( E* x ph <-> ( E. x ph -> E* x ph ) )
31 wl-sb8et 
 |-  ( A. x F/ y ph -> ( E. x ph <-> E. y [ y / x ] ph ) )
32 wl-mo2t 
 |-  ( A. x F/ y ph -> ( E* x ph <-> E. y A. x ( ph -> x = y ) ) )
33 31 32 imbi12d 
 |-  ( A. x F/ y ph -> ( ( E. x ph -> E* x ph ) <-> ( E. y [ y / x ] ph -> E. y A. x ( ph -> x = y ) ) ) )
34 30 33 syl5bb 
 |-  ( A. x F/ y ph -> ( E* x ph <-> ( E. y [ y / x ] ph -> E. y A. x ( ph -> x = y ) ) ) )
35 29 34 syl5ibr 
 |-  ( A. x F/ y ph -> ( A. x A. y ( ( ph /\ [ y / x ] ph ) -> x = y ) -> E* x ph ) )
36 21 35 impbid 
 |-  ( A. x F/ y ph -> ( E* x ph <-> A. x A. y ( ( ph /\ [ y / x ] ph ) -> x = y ) ) )