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 ( ( ∀ 𝑦 ∈ 𝐵 𝐶 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) → ( ∃! 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 = 𝐶 ↔ ∃! 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 = 𝐶 ) )

Proof

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