Theorem euor2 1435

Description: Introduce or eliminate a disjunct in a uniqueness quantifier.

Assertion

Ref	Expression
euor2	⊢ (¬ ∃xφ → (∃!x(φ ⋁ ψ) ↔ ∃!xψ))

Proof of Theorem euor2

Step	Hyp	Ref	Expression
1		euex 1392	. . . . . . 7 ⊢ (∃!x(φ ⋁ ψ) → ∃x(φ ⋁ ψ))
2		19.43 1086	. . . . . . 7 ⊢ (∃x(φ ⋁ ψ) ↔ (∃xφ ⋁ ∃xψ))
3	1, 2	sylib 198	. . . . . 6 ⊢ (∃!x(φ ⋁ ψ) → (∃xφ ⋁ ∃xψ))
4	3	ord 232	. . . . 5 ⊢ (∃!x(φ ⋁ ψ) → (¬ ∃xφ → ∃xψ))
5	4	com12 11	. . . 4 ⊢ (¬ ∃xφ → (∃!x(φ ⋁ ψ) → ∃xψ))
6		eumo 1409	. . . . . 6 ⊢ (∃!x(φ ⋁ ψ) → ∃*x(φ ⋁ ψ))
7		orcom 246	. . . . . . . 8 ⊢ ((φ ⋁ ψ) ↔ (ψ ⋁ φ))
8	7	mobii 1403	. . . . . . 7 ⊢ (∃*x(φ ⋁ ψ) ↔ ∃*x(ψ ⋁ φ))
9		moor 1422	. . . . . . 7 ⊢ (∃*x(ψ ⋁ φ) → ∃*xψ)
10	8, 9	sylbi 199	. . . . . 6 ⊢ (∃*x(φ ⋁ ψ) → ∃*xψ)
11	6, 10	syl 10	. . . . 5 ⊢ (∃!x(φ ⋁ ψ) → ∃*xψ)
12	11	a1i 8	. . . 4 ⊢ (¬ ∃xφ → (∃!x(φ ⋁ ψ) → ∃*xψ))
13	5, 12	jcad 599	. . 3 ⊢ (¬ ∃xφ → (∃!x(φ ⋁ ψ) → (∃xψ ⋀ ∃*xψ)))
14		eu5 1407	. . 3 ⊢ (∃!xψ ↔ (∃xψ ⋀ ∃*xψ))
15	13, 14	syl6ibr 213	. 2 ⊢ (¬ ∃xφ → (∃!x(φ ⋁ ψ) → ∃!xψ))
16		hbe1 1014	. . . . 5 ⊢ (∃xφ → ∀x∃xφ)
17	16	euor 1396	. . . 4 ⊢ ((¬ ∃xφ ⋀ ∃!xψ) → ∃!x(∃xφ ⋁ ψ))
18		euex 1392	. . . . . 6 ⊢ (∃!xψ → ∃xψ)
19		olc 268	. . . . . . 7 ⊢ (ψ → (φ ⋁ ψ))
20	19	19.22i 1038	. . . . . 6 ⊢ (∃xψ → ∃x(φ ⋁ ψ))
21		19.8a 1027	. . . . . . . . 9 ⊢ (φ → ∃xφ)
22	21	orim1i 337	. . . . . . . 8 ⊢ ((φ ⋁ ψ) → (∃xφ ⋁ ψ))
23	22	ax-gen 961	. . . . . . 7 ⊢ ∀x((φ ⋁ ψ) → (∃xφ ⋁ ψ))
24		euim 1419	. . . . . . 7 ⊢ ((∃x(φ ⋁ ψ) ⋀ ∀x((φ ⋁ ψ) → (∃xφ ⋁ ψ))) → (∃!x(∃xφ ⋁ ψ) → ∃!x(φ ⋁ ψ)))
25	23, 24	mpan2 695	. . . . . 6 ⊢ (∃x(φ ⋁ ψ) → (∃!x(∃xφ ⋁ ψ) → ∃!x(φ ⋁ ψ)))
26	18, 20, 25	3syl 20	. . . . 5 ⊢ (∃!xψ → (∃!x(∃xφ ⋁ ψ) → ∃!x(φ ⋁ ψ)))
27	26	adantl 388	. . . 4 ⊢ ((¬ ∃xφ ⋀ ∃!xψ) → (∃!x(∃xφ ⋁ ψ) → ∃!x(φ ⋁ ψ)))
28	17, 27	mpd 26	. . 3 ⊢ ((¬ ∃xφ ⋀ ∃!xψ) → ∃!x(φ ⋁ ψ))
29	28	ex 373	. 2 ⊢ (¬ ∃xφ → (∃!xψ → ∃!x(φ ⋁ ψ)))
30	15, 29	impbid 515	1 ⊢ (¬ ∃xφ → (∃!x(φ ⋁ ψ) ↔ ∃!xψ))

Syntax hints:  ¬ wn 2   → wi 3   ↔ wb 146   ⋁ wo 222   ⋀ wa 223  ∀wal 952  ∃wex 978  ∃!weu 1378  ∃*wmo 1379

This theorem is referenced by:  reuun2 2274

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-11 965  ax-12 966  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 979  df-sb 1170  df-eu 1380  df-mo 1381

Copyright terms: Public domain