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 ⊢∃!x∀y∈Ax=B→∃!x∃y∈Ax=B

Proof

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