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

Metamath Proof Explorer

Theorem reusv2lem3

Description: Lemma for reusv2 . (Contributed by NM, 14-Dec-2012) (Proof shortened by Mario Carneiro, 19-Nov-2016)

Ref Expression
Assertion reusv2lem3 ( ∀ 𝑦 ∈ 𝐴 𝐵 ∈ V → ( ∃! 𝑥 ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ↔ ∃! 𝑥 ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ) )

Proof

Step Hyp Ref Expression
1 simpr ⊢ ( ( ∀ 𝑦 ∈ 𝐴 𝐵 ∈ V ∧ ∃! 𝑥 ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ) → ∃! 𝑥 ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 )
2 nfv ⊢ Ⅎ 𝑥 ∀ 𝑦 ∈ 𝐴 𝐵 ∈ V
3 nfeu1 ⊢ Ⅎ 𝑥 ∃! 𝑥 ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵
4 2 3 nfan ⊢ Ⅎ 𝑥 ( ∀ 𝑦 ∈ 𝐴 𝐵 ∈ V ∧ ∃! 𝑥 ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 )
5 euex ⊢ ( ∃! 𝑥 ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 → ∃ 𝑥 ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 )
6 rexn0 ⊢ ( ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 → 𝐴 ≠ ∅ )
7 6 exlimiv ⊢ ( ∃ 𝑥 ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 → 𝐴 ≠ ∅ )
8 r19.2z ⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ) → ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 )
9 8 ex ⊢ ( 𝐴 ≠ ∅ → ( ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 → ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ) )
10 5 7 9 3syl ⊢ ( ∃! 𝑥 ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 → ( ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 → ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ) )
11 10 adantl ⊢ ( ( ∀ 𝑦 ∈ 𝐴 𝐵 ∈ V ∧ ∃! 𝑥 ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ) → ( ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 → ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ) )
12 nfra1 ⊢ Ⅎ 𝑦 ∀ 𝑦 ∈ 𝐴 𝐵 ∈ V
13 nfre1 ⊢ Ⅎ 𝑦 ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵
14 13 nfeuw ⊢ Ⅎ 𝑦 ∃! 𝑥 ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵
15 12 14 nfan ⊢ Ⅎ 𝑦 ( ∀ 𝑦 ∈ 𝐴 𝐵 ∈ V ∧ ∃! 𝑥 ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 )
16 rsp ⊢ ( ∀ 𝑦 ∈ 𝐴 𝐵 ∈ V → ( 𝑦 ∈ 𝐴 → 𝐵 ∈ V ) )
17 16 impcom ⊢ ( ( 𝑦 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 𝐵 ∈ V ) → 𝐵 ∈ V )
18 isset ⊢ ( 𝐵 ∈ V ↔ ∃ 𝑥 𝑥 = 𝐵 )
19 17 18 sylib ⊢ ( ( 𝑦 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 𝐵 ∈ V ) → ∃ 𝑥 𝑥 = 𝐵 )
20 19 adantrr ⊢ ( ( 𝑦 ∈ 𝐴 ∧ ( ∀ 𝑦 ∈ 𝐴 𝐵 ∈ V ∧ ∃! 𝑥 ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ) ) → ∃ 𝑥 𝑥 = 𝐵 )
21 rspe ⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑥 = 𝐵 ) → ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 )
22 21 ex ⊢ ( 𝑦 ∈ 𝐴 → ( 𝑥 = 𝐵 → ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ) )
23 22 ancrd ⊢ ( 𝑦 ∈ 𝐴 → ( 𝑥 = 𝐵 → ( ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ∧ 𝑥 = 𝐵 ) ) )
24 23 eximdv ⊢ ( 𝑦 ∈ 𝐴 → ( ∃ 𝑥 𝑥 = 𝐵 → ∃ 𝑥 ( ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ∧ 𝑥 = 𝐵 ) ) )
25 24 imp ⊢ ( ( 𝑦 ∈ 𝐴 ∧ ∃ 𝑥 𝑥 = 𝐵 ) → ∃ 𝑥 ( ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ∧ 𝑥 = 𝐵 ) )
26 20 25 syldan ⊢ ( ( 𝑦 ∈ 𝐴 ∧ ( ∀ 𝑦 ∈ 𝐴 𝐵 ∈ V ∧ ∃! 𝑥 ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ) ) → ∃ 𝑥 ( ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ∧ 𝑥 = 𝐵 ) )
27 eupick ⊢ ( ( ∃! 𝑥 ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ∧ ∃ 𝑥 ( ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ∧ 𝑥 = 𝐵 ) ) → ( ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 → 𝑥 = 𝐵 ) )
28 1 26 27 syl2an2 ⊢ ( ( 𝑦 ∈ 𝐴 ∧ ( ∀ 𝑦 ∈ 𝐴 𝐵 ∈ V ∧ ∃! 𝑥 ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ) ) → ( ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 → 𝑥 = 𝐵 ) )
29 28 ex ⊢ ( 𝑦 ∈ 𝐴 → ( ( ∀ 𝑦 ∈ 𝐴 𝐵 ∈ V ∧ ∃! 𝑥 ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ) → ( ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 → 𝑥 = 𝐵 ) ) )
30 29 com3l ⊢ ( ( ∀ 𝑦 ∈ 𝐴 𝐵 ∈ V ∧ ∃! 𝑥 ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ) → ( ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 → ( 𝑦 ∈ 𝐴 → 𝑥 = 𝐵 ) ) )
31 15 13 30 ralrimd ⊢ ( ( ∀ 𝑦 ∈ 𝐴 𝐵 ∈ V ∧ ∃! 𝑥 ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ) → ( ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 → ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ) )
32 11 31 impbid ⊢ ( ( ∀ 𝑦 ∈ 𝐴 𝐵 ∈ V ∧ ∃! 𝑥 ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ) → ( ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ↔ ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ) )
33 4 32 eubid ⊢ ( ( ∀ 𝑦 ∈ 𝐴 𝐵 ∈ V ∧ ∃! 𝑥 ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ) → ( ∃! 𝑥 ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ↔ ∃! 𝑥 ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ) )
34 1 33 mpbird ⊢ ( ( ∀ 𝑦 ∈ 𝐴 𝐵 ∈ V ∧ ∃! 𝑥 ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ) → ∃! 𝑥 ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 )
35 34 ex ⊢ ( ∀ 𝑦 ∈ 𝐴 𝐵 ∈ V → ( ∃! 𝑥 ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 → ∃! 𝑥 ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ) )
36 reusv2lem2 ⊢ ( ∃! 𝑥 ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 → ∃! 𝑥 ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 )
37 35 36 impbid1 ⊢ ( ∀ 𝑦 ∈ 𝐴 𝐵 ∈ V → ( ∃! 𝑥 ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ↔ ∃! 𝑥 ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ) )