Metamath Proof Explorer

Theorem 2reu5lem3

Description: Lemma for 2reu5 . This lemma is interesting in its own right, showing that existential restriction in the last conjunct (the "at most one" part) is optional; compare rmo2 . (Contributed by Alexander van der Vekens, 17-Jun-2017)

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

Proof

Step Hyp Ref Expression
1 2reu5lem1 ⊢ ( ∃! 𝑥 ∈ 𝐴 ∃! 𝑦 ∈ 𝐵 𝜑 ↔ ∃! 𝑥 ∃! 𝑦 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝜑 ) )
2 2reu5lem2 ⊢ ( ∀ 𝑥 ∈ 𝐴 ∃* 𝑦 ∈ 𝐵 𝜑 ↔ ∀ 𝑥 ∃* 𝑦 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝜑 ) )
3 1 2 anbi12i ⊢ ( ( ∃! 𝑥 ∈ 𝐴 ∃! 𝑦 ∈ 𝐵 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 ∃* 𝑦 ∈ 𝐵 𝜑 ) ↔ ( ∃! 𝑥 ∃! 𝑦 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝜑 ) ∧ ∀ 𝑥 ∃* 𝑦 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝜑 ) ) )
4 2eu5 ⊢ ( ( ∃! 𝑥 ∃! 𝑦 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝜑 ) ∧ ∀ 𝑥 ∃* 𝑦 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝜑 ) ) ↔ ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝜑 ) ∧ ∃ 𝑧 ∃ 𝑤 ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝜑 ) → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ) )
5 3anass ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝜑 ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ) )
6 5 exbii ⊢ ( ∃ 𝑦 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝜑 ) ↔ ∃ 𝑦 ( 𝑥 ∈ 𝐴 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ) )
7 19.42v ⊢ ( ∃ 𝑦 ( 𝑥 ∈ 𝐴 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ∃ 𝑦 ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ) )
8 df-rex ⊢ ( ∃ 𝑦 ∈ 𝐵 𝜑 ↔ ∃ 𝑦 ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) )
9 8 bicomi ⊢ ( ∃ 𝑦 ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ↔ ∃ 𝑦 ∈ 𝐵 𝜑 )
10 9 anbi2i ⊢ ( ( 𝑥 ∈ 𝐴 ∧ ∃ 𝑦 ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ∃ 𝑦 ∈ 𝐵 𝜑 ) )
11 6 7 10 3bitri ⊢ ( ∃ 𝑦 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝜑 ) ↔ ( 𝑥 ∈ 𝐴 ∧ ∃ 𝑦 ∈ 𝐵 𝜑 ) )
12 11 exbii ⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝜑 ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ ∃ 𝑦 ∈ 𝐵 𝜑 ) )
13 df-rex ⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ ∃ 𝑦 ∈ 𝐵 𝜑 ) )
14 12 13 bitr4i ⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝜑 ) ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 )
15 3anan12 ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝜑 ) ↔ ( 𝑦 ∈ 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) )
16 15 imbi1i ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝜑 ) → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ↔ ( ( 𝑦 ∈ 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) )
17 impexp ⊢ ( ( ( 𝑦 ∈ 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ↔ ( 𝑦 ∈ 𝐵 → ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ) )
18 impexp ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ↔ ( 𝑥 ∈ 𝐴 → ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ) )
19 18 imbi2i ⊢ ( ( 𝑦 ∈ 𝐵 → ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ) ↔ ( 𝑦 ∈ 𝐵 → ( 𝑥 ∈ 𝐴 → ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ) ) )
20 16 17 19 3bitri ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝜑 ) → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ↔ ( 𝑦 ∈ 𝐵 → ( 𝑥 ∈ 𝐴 → ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ) ) )
21 20 albii ⊢ ( ∀ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝜑 ) → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ↔ ∀ 𝑦 ( 𝑦 ∈ 𝐵 → ( 𝑥 ∈ 𝐴 → ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ) ) )
22 df-ral ⊢ ( ∀ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝐴 → ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ) ↔ ∀ 𝑦 ( 𝑦 ∈ 𝐵 → ( 𝑥 ∈ 𝐴 → ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ) ) )
23 r19.21v ⊢ ( ∀ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝐴 → ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ) ↔ ( 𝑥 ∈ 𝐴 → ∀ 𝑦 ∈ 𝐵 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ) )
24 21 22 23 3bitr2i ⊢ ( ∀ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝜑 ) → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ↔ ( 𝑥 ∈ 𝐴 → ∀ 𝑦 ∈ 𝐵 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ) )
25 24 albii ⊢ ( ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝜑 ) → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ∀ 𝑦 ∈ 𝐵 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ) )
26 df-ral ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ∀ 𝑦 ∈ 𝐵 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ) )
27 25 26 bitr4i ⊢ ( ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝜑 ) → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) )
28 27 exbii ⊢ ( ∃ 𝑤 ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝜑 ) → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ↔ ∃ 𝑤 ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) )
29 28 exbii ⊢ ( ∃ 𝑧 ∃ 𝑤 ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝜑 ) → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ↔ ∃ 𝑧 ∃ 𝑤 ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) )
30 14 29 anbi12i ⊢ ( ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝜑 ) ∧ ∃ 𝑧 ∃ 𝑤 ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝜑 ) → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ) ↔ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ∧ ∃ 𝑧 ∃ 𝑤 ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ) )
31 3 4 30 3bitri ⊢ ( ( ∃! 𝑥 ∈ 𝐴 ∃! 𝑦 ∈ 𝐵 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 ∃* 𝑦 ∈ 𝐵 𝜑 ) ↔ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ∧ ∃ 𝑧 ∃ 𝑤 ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ) )