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 ∈ B C ∈ A ∧ B ≠ ∅ → ∃! x ∈ A ∃ y ∈ B x = C ↔ ∃! x ∈ A ∀ y ∈ B x = 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 syl6bbr ⊢ C ∈ A → C ∈ A ∧ ⊤ → x = C ↔ x ∈ A ∧ x = C
9 8 ralimi ⊢ ∀ y ∈ B C ∈ A → ∀ y ∈ B C ∈ A ∧ ⊤ → x = C ↔ x ∈ A ∧ x = C
10 ralbi ⊢ ∀ y ∈ B C ∈ A ∧ ⊤ → x = C ↔ x ∈ A ∧ x = C → ∀ y ∈ B C ∈ A ∧ ⊤ → x = C ↔ ∀ y ∈ B x ∈ A ∧ x = C
11 9 10 syl ⊢ ∀ y ∈ B C ∈ A → ∀ y ∈ B C ∈ A ∧ ⊤ → x = C ↔ ∀ y ∈ B x ∈ A ∧ x = C
12 11 eubidv ⊢ ∀ y ∈ B C ∈ A → ∃! x ∀ y ∈ B C ∈ A ∧ ⊤ → x = C ↔ ∃! x ∀ y ∈ B x ∈ A ∧ x = C
13 r19.28zv ⊢ B ≠ ∅ → ∀ y ∈ B x ∈ A ∧ x = C ↔ x ∈ A ∧ ∀ y ∈ B x = C
14 13 eubidv ⊢ B ≠ ∅ → ∃! x ∀ y ∈ B x ∈ A ∧ x = C ↔ ∃! x x ∈ A ∧ ∀ y ∈ B x = C
15 12 14 sylan9bb ⊢ ∀ y ∈ B C ∈ A ∧ B ≠ ∅ → ∃! x ∀ y ∈ B C ∈ A ∧ ⊤ → x = C ↔ ∃! x x ∈ A ∧ ∀ y ∈ B x = C
16 1 biantrur ⊢ x = C ↔ ⊤ ∧ x = C
17 16 rexbii ⊢ ∃ y ∈ B x = C ↔ ∃ y ∈ B ⊤ ∧ x = C
18 17 reubii ⊢ ∃! x ∈ A ∃ y ∈ B x = C ↔ ∃! x ∈ A ∃ y ∈ B ⊤ ∧ x = C
19 reusv2lem4 ⊢ ∃! x ∈ A ∃ y ∈ B ⊤ ∧ x = C ↔ ∃! x ∀ y ∈ B C ∈ A ∧ ⊤ → x = C
20 18 19 bitri ⊢ ∃! x ∈ A ∃ y ∈ B x = C ↔ ∃! x ∀ y ∈ B C ∈ A ∧ ⊤ → x = C
21 df-reu ⊢ ∃! x ∈ A ∀ y ∈ B x = C ↔ ∃! x x ∈ A ∧ ∀ y ∈ B x = C
22 15 20 21 3bitr4g ⊢ ∀ y ∈ B C ∈ A ∧ B ≠ ∅ → ∃! x ∈ A ∃ y ∈ B x = C ↔ ∃! x ∈ A ∀ y ∈ B x = C