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

Metamath Proof Explorer

Theorem reusv2lem2

Description: Lemma for reusv2 . (Contributed by NM, 27-Oct-2010) (Proof shortened by Mario Carneiro, 19-Nov-2016) (Proof shortened by JJ, 7-Aug-2021)

Ref Expression
Assertion reusv2lem2 ( ∃! 𝑥 ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 → ∃! 𝑥 ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 )

Proof

Step Hyp Ref Expression
1 eunex ⊢ ( ∃! 𝑥 ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 → ∃ 𝑥 ¬ ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 )
2 exnal ⊢ ( ∃ 𝑥 ¬ ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ↔ ¬ ∀ 𝑥 ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 )
3 1 2 sylib ⊢ ( ∃! 𝑥 ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 → ¬ ∀ 𝑥 ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 )
4 rzal ⊢ ( 𝐴 = ∅ → ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 )
5 4 alrimiv ⊢ ( 𝐴 = ∅ → ∀ 𝑥 ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 )
6 3 5 nsyl3 ⊢ ( 𝐴 = ∅ → ¬ ∃! 𝑥 ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 )
7 6 pm2.21d ⊢ ( 𝐴 = ∅ → ( ∃! 𝑥 ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 → ∃! 𝑥 ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ) )
8 simpr ⊢ ( ( 𝐴 ≠ ∅ ∧ ∃! 𝑥 ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ) → ∃! 𝑥 ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 )
9 nfra1 ⊢ Ⅎ 𝑦 ∀ 𝑦 ∈ 𝐴 𝑧 = 𝐵
10 nfra1 ⊢ Ⅎ 𝑦 ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵
11 simpr ⊢ ( ( ( ∀ 𝑦 ∈ 𝐴 𝑧 = 𝐵 ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑥 = 𝐵 ) → 𝑥 = 𝐵 )
12 rspa ⊢ ( ( ∀ 𝑦 ∈ 𝐴 𝑧 = 𝐵 ∧ 𝑦 ∈ 𝐴 ) → 𝑧 = 𝐵 )
13 12 adantr ⊢ ( ( ( ∀ 𝑦 ∈ 𝐴 𝑧 = 𝐵 ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑥 = 𝐵 ) → 𝑧 = 𝐵 )
14 11 13 eqtr4d ⊢ ( ( ( ∀ 𝑦 ∈ 𝐴 𝑧 = 𝐵 ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑥 = 𝐵 ) → 𝑥 = 𝑧 )
15 eqeq1 ⊢ ( 𝑥 = 𝑧 → ( 𝑥 = 𝐵 ↔ 𝑧 = 𝐵 ) )
16 15 ralbidv ⊢ ( 𝑥 = 𝑧 → ( ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ↔ ∀ 𝑦 ∈ 𝐴 𝑧 = 𝐵 ) )
17 16 biimprcd ⊢ ( ∀ 𝑦 ∈ 𝐴 𝑧 = 𝐵 → ( 𝑥 = 𝑧 → ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ) )
18 17 ad2antrr ⊢ ( ( ( ∀ 𝑦 ∈ 𝐴 𝑧 = 𝐵 ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑥 = 𝐵 ) → ( 𝑥 = 𝑧 → ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ) )
19 14 18 mpd ⊢ ( ( ( ∀ 𝑦 ∈ 𝐴 𝑧 = 𝐵 ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑥 = 𝐵 ) → ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 )
20 19 exp31 ⊢ ( ∀ 𝑦 ∈ 𝐴 𝑧 = 𝐵 → ( 𝑦 ∈ 𝐴 → ( 𝑥 = 𝐵 → ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ) ) )
21 9 10 20 rexlimd ⊢ ( ∀ 𝑦 ∈ 𝐴 𝑧 = 𝐵 → ( ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 → ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ) )
22 21 adantl ⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑦 ∈ 𝐴 𝑧 = 𝐵 ) → ( ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 → ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ) )
23 r19.2z ⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ) → ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 )
24 23 ex ⊢ ( 𝐴 ≠ ∅ → ( ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 → ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ) )
25 24 adantr ⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑦 ∈ 𝐴 𝑧 = 𝐵 ) → ( ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 → ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ) )
26 22 25 impbid ⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑦 ∈ 𝐴 𝑧 = 𝐵 ) → ( ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ↔ ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ) )
27 26 eubidv ⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑦 ∈ 𝐴 𝑧 = 𝐵 ) → ( ∃! 𝑥 ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ↔ ∃! 𝑥 ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ) )
28 27 ex ⊢ ( 𝐴 ≠ ∅ → ( ∀ 𝑦 ∈ 𝐴 𝑧 = 𝐵 → ( ∃! 𝑥 ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ↔ ∃! 𝑥 ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ) ) )
29 28 exlimdv ⊢ ( 𝐴 ≠ ∅ → ( ∃ 𝑧 ∀ 𝑦 ∈ 𝐴 𝑧 = 𝐵 → ( ∃! 𝑥 ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ↔ ∃! 𝑥 ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ) ) )
30 euex ⊢ ( ∃! 𝑥 ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 → ∃ 𝑥 ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 )
31 16 cbvexvw ⊢ ( ∃ 𝑥 ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ↔ ∃ 𝑧 ∀ 𝑦 ∈ 𝐴 𝑧 = 𝐵 )
32 30 31 sylib ⊢ ( ∃! 𝑥 ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 → ∃ 𝑧 ∀ 𝑦 ∈ 𝐴 𝑧 = 𝐵 )
33 29 32 impel ⊢ ( ( 𝐴 ≠ ∅ ∧ ∃! 𝑥 ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ) → ( ∃! 𝑥 ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ↔ ∃! 𝑥 ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ) )
34 8 33 mpbird ⊢ ( ( 𝐴 ≠ ∅ ∧ ∃! 𝑥 ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ) → ∃! 𝑥 ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 )
35 34 ex ⊢ ( 𝐴 ≠ ∅ → ( ∃! 𝑥 ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 → ∃! 𝑥 ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ) )
36 7 35 pm2.61ine ⊢ ( ∃! 𝑥 ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 → ∃! 𝑥 ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 )