This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem euind

Description: Existential uniqueness via an indirect equality. (Contributed by NM, 11-Oct-2010)

Ref Expression
Hypotheses euind.1 ⊢ 𝐵 ∈ V
euind.2 ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
Assertion euind ( ( ∀ 𝑥 ∀ 𝑦 ( ( 𝜑 ∧ 𝜓 ) → 𝐴 = 𝐵 ) ∧ ∃ 𝑥 𝜑 ) → ∃! 𝑧 ∀ 𝑥 ( 𝜑 → 𝑧 = 𝐴 ) )

Proof

Step Hyp Ref Expression
1 euind.1 ⊢ 𝐵 ∈ V
2 euind.2 ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
3 2 cbvexvw ⊢ ( ∃ 𝑥 𝜑 ↔ ∃ 𝑦 𝜓 )
4 1 isseti ⊢ ∃ 𝑧 𝑧 = 𝐵
5 4 biantrur ⊢ ( 𝜓 ↔ ( ∃ 𝑧 𝑧 = 𝐵 ∧ 𝜓 ) )
6 5 exbii ⊢ ( ∃ 𝑦 𝜓 ↔ ∃ 𝑦 ( ∃ 𝑧 𝑧 = 𝐵 ∧ 𝜓 ) )
7 19.41v ⊢ ( ∃ 𝑧 ( 𝑧 = 𝐵 ∧ 𝜓 ) ↔ ( ∃ 𝑧 𝑧 = 𝐵 ∧ 𝜓 ) )
8 7 exbii ⊢ ( ∃ 𝑦 ∃ 𝑧 ( 𝑧 = 𝐵 ∧ 𝜓 ) ↔ ∃ 𝑦 ( ∃ 𝑧 𝑧 = 𝐵 ∧ 𝜓 ) )
9 excom ⊢ ( ∃ 𝑦 ∃ 𝑧 ( 𝑧 = 𝐵 ∧ 𝜓 ) ↔ ∃ 𝑧 ∃ 𝑦 ( 𝑧 = 𝐵 ∧ 𝜓 ) )
10 6 8 9 3bitr2i ⊢ ( ∃ 𝑦 𝜓 ↔ ∃ 𝑧 ∃ 𝑦 ( 𝑧 = 𝐵 ∧ 𝜓 ) )
11 3 10 bitri ⊢ ( ∃ 𝑥 𝜑 ↔ ∃ 𝑧 ∃ 𝑦 ( 𝑧 = 𝐵 ∧ 𝜓 ) )
12 eqeq2 ⊢ ( 𝐴 = 𝐵 → ( 𝑧 = 𝐴 ↔ 𝑧 = 𝐵 ) )
13 12 imim2i ⊢ ( ( ( 𝜑 ∧ 𝜓 ) → 𝐴 = 𝐵 ) → ( ( 𝜑 ∧ 𝜓 ) → ( 𝑧 = 𝐴 ↔ 𝑧 = 𝐵 ) ) )
14 biimpr ⊢ ( ( 𝑧 = 𝐴 ↔ 𝑧 = 𝐵 ) → ( 𝑧 = 𝐵 → 𝑧 = 𝐴 ) )
15 14 imim2i ⊢ ( ( ( 𝜑 ∧ 𝜓 ) → ( 𝑧 = 𝐴 ↔ 𝑧 = 𝐵 ) ) → ( ( 𝜑 ∧ 𝜓 ) → ( 𝑧 = 𝐵 → 𝑧 = 𝐴 ) ) )
16 an31 ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑧 = 𝐵 ) ↔ ( ( 𝑧 = 𝐵 ∧ 𝜓 ) ∧ 𝜑 ) )
17 16 imbi1i ⊢ ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑧 = 𝐵 ) → 𝑧 = 𝐴 ) ↔ ( ( ( 𝑧 = 𝐵 ∧ 𝜓 ) ∧ 𝜑 ) → 𝑧 = 𝐴 ) )
18 impexp ⊢ ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑧 = 𝐵 ) → 𝑧 = 𝐴 ) ↔ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑧 = 𝐵 → 𝑧 = 𝐴 ) ) )
19 impexp ⊢ ( ( ( ( 𝑧 = 𝐵 ∧ 𝜓 ) ∧ 𝜑 ) → 𝑧 = 𝐴 ) ↔ ( ( 𝑧 = 𝐵 ∧ 𝜓 ) → ( 𝜑 → 𝑧 = 𝐴 ) ) )
20 17 18 19 3bitr3i ⊢ ( ( ( 𝜑 ∧ 𝜓 ) → ( 𝑧 = 𝐵 → 𝑧 = 𝐴 ) ) ↔ ( ( 𝑧 = 𝐵 ∧ 𝜓 ) → ( 𝜑 → 𝑧 = 𝐴 ) ) )
21 15 20 sylib ⊢ ( ( ( 𝜑 ∧ 𝜓 ) → ( 𝑧 = 𝐴 ↔ 𝑧 = 𝐵 ) ) → ( ( 𝑧 = 𝐵 ∧ 𝜓 ) → ( 𝜑 → 𝑧 = 𝐴 ) ) )
22 13 21 syl ⊢ ( ( ( 𝜑 ∧ 𝜓 ) → 𝐴 = 𝐵 ) → ( ( 𝑧 = 𝐵 ∧ 𝜓 ) → ( 𝜑 → 𝑧 = 𝐴 ) ) )
23 22 2alimi ⊢ ( ∀ 𝑥 ∀ 𝑦 ( ( 𝜑 ∧ 𝜓 ) → 𝐴 = 𝐵 ) → ∀ 𝑥 ∀ 𝑦 ( ( 𝑧 = 𝐵 ∧ 𝜓 ) → ( 𝜑 → 𝑧 = 𝐴 ) ) )
24 19.23v ⊢ ( ∀ 𝑦 ( ( 𝑧 = 𝐵 ∧ 𝜓 ) → ( 𝜑 → 𝑧 = 𝐴 ) ) ↔ ( ∃ 𝑦 ( 𝑧 = 𝐵 ∧ 𝜓 ) → ( 𝜑 → 𝑧 = 𝐴 ) ) )
25 24 albii ⊢ ( ∀ 𝑥 ∀ 𝑦 ( ( 𝑧 = 𝐵 ∧ 𝜓 ) → ( 𝜑 → 𝑧 = 𝐴 ) ) ↔ ∀ 𝑥 ( ∃ 𝑦 ( 𝑧 = 𝐵 ∧ 𝜓 ) → ( 𝜑 → 𝑧 = 𝐴 ) ) )
26 19.21v ⊢ ( ∀ 𝑥 ( ∃ 𝑦 ( 𝑧 = 𝐵 ∧ 𝜓 ) → ( 𝜑 → 𝑧 = 𝐴 ) ) ↔ ( ∃ 𝑦 ( 𝑧 = 𝐵 ∧ 𝜓 ) → ∀ 𝑥 ( 𝜑 → 𝑧 = 𝐴 ) ) )
27 25 26 bitri ⊢ ( ∀ 𝑥 ∀ 𝑦 ( ( 𝑧 = 𝐵 ∧ 𝜓 ) → ( 𝜑 → 𝑧 = 𝐴 ) ) ↔ ( ∃ 𝑦 ( 𝑧 = 𝐵 ∧ 𝜓 ) → ∀ 𝑥 ( 𝜑 → 𝑧 = 𝐴 ) ) )
28 23 27 sylib ⊢ ( ∀ 𝑥 ∀ 𝑦 ( ( 𝜑 ∧ 𝜓 ) → 𝐴 = 𝐵 ) → ( ∃ 𝑦 ( 𝑧 = 𝐵 ∧ 𝜓 ) → ∀ 𝑥 ( 𝜑 → 𝑧 = 𝐴 ) ) )
29 28 eximdv ⊢ ( ∀ 𝑥 ∀ 𝑦 ( ( 𝜑 ∧ 𝜓 ) → 𝐴 = 𝐵 ) → ( ∃ 𝑧 ∃ 𝑦 ( 𝑧 = 𝐵 ∧ 𝜓 ) → ∃ 𝑧 ∀ 𝑥 ( 𝜑 → 𝑧 = 𝐴 ) ) )
30 11 29 biimtrid ⊢ ( ∀ 𝑥 ∀ 𝑦 ( ( 𝜑 ∧ 𝜓 ) → 𝐴 = 𝐵 ) → ( ∃ 𝑥 𝜑 → ∃ 𝑧 ∀ 𝑥 ( 𝜑 → 𝑧 = 𝐴 ) ) )
31 30 imp ⊢ ( ( ∀ 𝑥 ∀ 𝑦 ( ( 𝜑 ∧ 𝜓 ) → 𝐴 = 𝐵 ) ∧ ∃ 𝑥 𝜑 ) → ∃ 𝑧 ∀ 𝑥 ( 𝜑 → 𝑧 = 𝐴 ) )
32 pm4.24 ⊢ ( 𝜑 ↔ ( 𝜑 ∧ 𝜑 ) )
33 32 biimpi ⊢ ( 𝜑 → ( 𝜑 ∧ 𝜑 ) )
34 anim12 ⊢ ( ( ( 𝜑 → 𝑧 = 𝐴 ) ∧ ( 𝜑 → 𝑤 = 𝐴 ) ) → ( ( 𝜑 ∧ 𝜑 ) → ( 𝑧 = 𝐴 ∧ 𝑤 = 𝐴 ) ) )
35 eqtr3 ⊢ ( ( 𝑧 = 𝐴 ∧ 𝑤 = 𝐴 ) → 𝑧 = 𝑤 )
36 33 34 35 syl56 ⊢ ( ( ( 𝜑 → 𝑧 = 𝐴 ) ∧ ( 𝜑 → 𝑤 = 𝐴 ) ) → ( 𝜑 → 𝑧 = 𝑤 ) )
37 36 alanimi ⊢ ( ( ∀ 𝑥 ( 𝜑 → 𝑧 = 𝐴 ) ∧ ∀ 𝑥 ( 𝜑 → 𝑤 = 𝐴 ) ) → ∀ 𝑥 ( 𝜑 → 𝑧 = 𝑤 ) )
38 19.23v ⊢ ( ∀ 𝑥 ( 𝜑 → 𝑧 = 𝑤 ) ↔ ( ∃ 𝑥 𝜑 → 𝑧 = 𝑤 ) )
39 37 38 sylib ⊢ ( ( ∀ 𝑥 ( 𝜑 → 𝑧 = 𝐴 ) ∧ ∀ 𝑥 ( 𝜑 → 𝑤 = 𝐴 ) ) → ( ∃ 𝑥 𝜑 → 𝑧 = 𝑤 ) )
40 39 com12 ⊢ ( ∃ 𝑥 𝜑 → ( ( ∀ 𝑥 ( 𝜑 → 𝑧 = 𝐴 ) ∧ ∀ 𝑥 ( 𝜑 → 𝑤 = 𝐴 ) ) → 𝑧 = 𝑤 ) )
41 40 alrimivv ⊢ ( ∃ 𝑥 𝜑 → ∀ 𝑧 ∀ 𝑤 ( ( ∀ 𝑥 ( 𝜑 → 𝑧 = 𝐴 ) ∧ ∀ 𝑥 ( 𝜑 → 𝑤 = 𝐴 ) ) → 𝑧 = 𝑤 ) )
42 41 adantl ⊢ ( ( ∀ 𝑥 ∀ 𝑦 ( ( 𝜑 ∧ 𝜓 ) → 𝐴 = 𝐵 ) ∧ ∃ 𝑥 𝜑 ) → ∀ 𝑧 ∀ 𝑤 ( ( ∀ 𝑥 ( 𝜑 → 𝑧 = 𝐴 ) ∧ ∀ 𝑥 ( 𝜑 → 𝑤 = 𝐴 ) ) → 𝑧 = 𝑤 ) )
43 eqeq1 ⊢ ( 𝑧 = 𝑤 → ( 𝑧 = 𝐴 ↔ 𝑤 = 𝐴 ) )
44 43 imbi2d ⊢ ( 𝑧 = 𝑤 → ( ( 𝜑 → 𝑧 = 𝐴 ) ↔ ( 𝜑 → 𝑤 = 𝐴 ) ) )
45 44 albidv ⊢ ( 𝑧 = 𝑤 → ( ∀ 𝑥 ( 𝜑 → 𝑧 = 𝐴 ) ↔ ∀ 𝑥 ( 𝜑 → 𝑤 = 𝐴 ) ) )
46 45 eu4 ⊢ ( ∃! 𝑧 ∀ 𝑥 ( 𝜑 → 𝑧 = 𝐴 ) ↔ ( ∃ 𝑧 ∀ 𝑥 ( 𝜑 → 𝑧 = 𝐴 ) ∧ ∀ 𝑧 ∀ 𝑤 ( ( ∀ 𝑥 ( 𝜑 → 𝑧 = 𝐴 ) ∧ ∀ 𝑥 ( 𝜑 → 𝑤 = 𝐴 ) ) → 𝑧 = 𝑤 ) ) )
47 31 42 46 sylanbrc ⊢ ( ( ∀ 𝑥 ∀ 𝑦 ( ( 𝜑 ∧ 𝜓 ) → 𝐴 = 𝐵 ) ∧ ∃ 𝑥 𝜑 ) → ∃! 𝑧 ∀ 𝑥 ( 𝜑 → 𝑧 = 𝐴 ) )