Metamath Proof Explorer

Theorem 2reu5

Description: Double restricted existential uniqueness in terms of restricted existential quantification and restricted universal quantification, analogous to 2eu5 and reu3 . (Contributed by Alexander van der Vekens, 17-Jun-2017)

Ref Expression
Assertion 2reu5 ( ( ∃! 𝑥 ∈ 𝐴 ∃! 𝑦 ∈ 𝐵 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 ∃* 𝑦 ∈ 𝐵 𝜑 ) ↔ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ∧ ∃ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐵 ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ) )

Proof

Step Hyp Ref Expression
1 r19.29r ⊢ ( ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ) → ∃ 𝑥 ∈ 𝐴 ( ∃ 𝑦 ∈ 𝐵 𝜑 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ) )
2 r19.29r ⊢ ( ( ∃ 𝑦 ∈ 𝐵 𝜑 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ) → ∃ 𝑦 ∈ 𝐵 ( 𝜑 ∧ ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ) )
3 2 reximi ⊢ ( ∃ 𝑥 ∈ 𝐴 ( ∃ 𝑦 ∈ 𝐵 𝜑 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ) → ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝜑 ∧ ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ) )
4 pm3.35 ⊢ ( ( 𝜑 ∧ ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ) → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) )
5 4 reximi ⊢ ( ∃ 𝑦 ∈ 𝐵 ( 𝜑 ∧ ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ) → ∃ 𝑦 ∈ 𝐵 ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) )
6 5 reximi ⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝜑 ∧ ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ) → ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) )
7 eleq1w ⊢ ( 𝑥 = 𝑧 → ( 𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴 ) )
8 eleq1w ⊢ ( 𝑦 = 𝑤 → ( 𝑦 ∈ 𝐵 ↔ 𝑤 ∈ 𝐵 ) )
9 7 8 bi2anan9 ⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ↔ ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵 ) ) )
10 9 biimpac ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) → ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵 ) )
11 10 ancomd ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) → ( 𝑤 ∈ 𝐵 ∧ 𝑧 ∈ 𝐴 ) )
12 11 ex ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( 𝑤 ∈ 𝐵 ∧ 𝑧 ∈ 𝐴 ) ) )
13 12 rexlimivv ⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( 𝑤 ∈ 𝐵 ∧ 𝑧 ∈ 𝐴 ) )
14 1 3 6 13 4syl ⊢ ( ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ) → ( 𝑤 ∈ 𝐵 ∧ 𝑧 ∈ 𝐴 ) )
15 14 ex ⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) → ( 𝑤 ∈ 𝐵 ∧ 𝑧 ∈ 𝐴 ) ) )
16 15 pm4.71rd ⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ↔ ( ( 𝑤 ∈ 𝐵 ∧ 𝑧 ∈ 𝐴 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ) ) )
17 anass ⊢ ( ( ( 𝑤 ∈ 𝐵 ∧ 𝑧 ∈ 𝐴 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ) ↔ ( 𝑤 ∈ 𝐵 ∧ ( 𝑧 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ) ) )
18 16 17 bitrdi ⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ↔ ( 𝑤 ∈ 𝐵 ∧ ( 𝑧 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ) ) ) )
19 18 2exbidv ⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 → ( ∃ 𝑧 ∃ 𝑤 ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ↔ ∃ 𝑧 ∃ 𝑤 ( 𝑤 ∈ 𝐵 ∧ ( 𝑧 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ) ) ) )
20 19 pm5.32i ⊢ ( ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ∧ ∃ 𝑧 ∃ 𝑤 ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ) ↔ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ∧ ∃ 𝑧 ∃ 𝑤 ( 𝑤 ∈ 𝐵 ∧ ( 𝑧 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ) ) ) )
21 2reu5lem3 ⊢ ( ( ∃! 𝑥 ∈ 𝐴 ∃! 𝑦 ∈ 𝐵 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 ∃* 𝑦 ∈ 𝐵 𝜑 ) ↔ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ∧ ∃ 𝑧 ∃ 𝑤 ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ) )
22 df-rex ⊢ ( ∃ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐵 ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ↔ ∃ 𝑧 ( 𝑧 ∈ 𝐴 ∧ ∃ 𝑤 ∈ 𝐵 ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ) )
23 r19.42v ⊢ ( ∃ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ) ↔ ( 𝑧 ∈ 𝐴 ∧ ∃ 𝑤 ∈ 𝐵 ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ) )
24 df-rex ⊢ ( ∃ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ) ↔ ∃ 𝑤 ( 𝑤 ∈ 𝐵 ∧ ( 𝑧 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ) ) )
25 23 24 bitr3i ⊢ ( ( 𝑧 ∈ 𝐴 ∧ ∃ 𝑤 ∈ 𝐵 ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ) ↔ ∃ 𝑤 ( 𝑤 ∈ 𝐵 ∧ ( 𝑧 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ) ) )
26 25 exbii ⊢ ( ∃ 𝑧 ( 𝑧 ∈ 𝐴 ∧ ∃ 𝑤 ∈ 𝐵 ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ) ↔ ∃ 𝑧 ∃ 𝑤 ( 𝑤 ∈ 𝐵 ∧ ( 𝑧 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ) ) )
27 22 26 bitri ⊢ ( ∃ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐵 ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ↔ ∃ 𝑧 ∃ 𝑤 ( 𝑤 ∈ 𝐵 ∧ ( 𝑧 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ) ) )
28 27 anbi2i ⊢ ( ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ∧ ∃ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐵 ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ) ↔ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ∧ ∃ 𝑧 ∃ 𝑤 ( 𝑤 ∈ 𝐵 ∧ ( 𝑧 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ) ) ) )
29 20 21 28 3bitr4i ⊢ ( ( ∃! 𝑥 ∈ 𝐴 ∃! 𝑦 ∈ 𝐵 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 ∃* 𝑦 ∈ 𝐵 𝜑 ) ↔ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ∧ ∃ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐵 ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ) )