Theorem wl-mo3t

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

	Ref	Expression
Assertion	wl-mo3t	⊢ ( ∀ 𝑥 Ⅎ 𝑦 𝜑 → ( ∃* 𝑥 𝜑 ↔ ∀ 𝑥 ∀ 𝑦 ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) ) )

Proof

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