Metamath Proof Explorer

Theorem reusv2lem5

Description: Lemma for reusv2 . (Contributed by NM, 4-Jan-2013) (Proof shortened by Mario Carneiro, 19-Nov-2016)

Ref Expression
Assertion reusv2lem5 ⊢∀y∈BC∈A∧B≠∅→∃!x∈A∃y∈Bx=C↔∃!x∈A∀y∈Bx=C

Proof

Step Hyp Ref Expression
1 tru ⊢⊤
2 biimt ⊢C∈A∧⊤→x=C↔C∈A∧⊤→x=C
3 1 2 mpan2 ⊢C∈A→x=C↔C∈A∧⊤→x=C
4 ibar ⊢C∈A→x=C↔C∈A∧x=C
5 3 4 bitr3d ⊢C∈A→C∈A∧⊤→x=C↔C∈A∧x=C
6 eleq1 ⊢x=C→x∈A↔C∈A
7 6 pm5.32ri ⊢x∈A∧x=C↔C∈A∧x=C
8 5 7 bitr4di ⊢C∈A→C∈A∧⊤→x=C↔x∈A∧x=C
9 8 ralimi ⊢∀y∈BC∈A→∀y∈BC∈A∧⊤→x=C↔x∈A∧x=C
10 ralbi ⊢∀y∈BC∈A∧⊤→x=C↔x∈A∧x=C→∀y∈BC∈A∧⊤→x=C↔∀y∈Bx∈A∧x=C
11 9 10 syl ⊢∀y∈BC∈A→∀y∈BC∈A∧⊤→x=C↔∀y∈Bx∈A∧x=C
12 11 eubidv ⊢∀y∈BC∈A→∃!x∀y∈BC∈A∧⊤→x=C↔∃!x∀y∈Bx∈A∧x=C
13 r19.28zv ⊢B≠∅→∀y∈Bx∈A∧x=C↔x∈A∧∀y∈Bx=C
14 13 eubidv ⊢B≠∅→∃!x∀y∈Bx∈A∧x=C↔∃!xx∈A∧∀y∈Bx=C
15 12 14 sylan9bb ⊢∀y∈BC∈A∧B≠∅→∃!x∀y∈BC∈A∧⊤→x=C↔∃!xx∈A∧∀y∈Bx=C
16 1 biantrur ⊢x=C↔⊤∧x=C
17 16 rexbii ⊢∃y∈Bx=C↔∃y∈B⊤∧x=C
18 17 reubii ⊢∃!x∈A∃y∈Bx=C↔∃!x∈A∃y∈B⊤∧x=C
19 reusv2lem4 ⊢∃!x∈A∃y∈B⊤∧x=C↔∃!x∀y∈BC∈A∧⊤→x=C
20 18 19 bitri ⊢∃!x∈A∃y∈Bx=C↔∃!x∀y∈BC∈A∧⊤→x=C
21 df-reu ⊢∃!x∈A∀y∈Bx=C↔∃!xx∈A∧∀y∈Bx=C
22 15 20 21 3bitr4g ⊢∀y∈BC∈A∧B≠∅→∃!x∈A∃y∈Bx=C↔∃!x∈A∀y∈Bx=C