This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 2reurex

Description: Double restricted quantification with existential uniqueness, analogous to 2euex . (Contributed by Alexander van der Vekens, 24-Jun-2017)

Ref Expression
Assertion 2reurex ( ∃! 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 → ∃ 𝑦 ∈ 𝐵 ∃! 𝑥 ∈ 𝐴 𝜑 )

Proof

Step Hyp Ref Expression
1 reu5 ⊢ ( ∃! 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ↔ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ∧ ∃* 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ) )
2 rexcom ⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ↔ ∃ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝜑 )
3 nfcv ⊢ Ⅎ 𝑦 𝐴
4 nfre1 ⊢ Ⅎ 𝑦 ∃ 𝑦 ∈ 𝐵 𝜑
5 3 4 nfrmow ⊢ Ⅎ 𝑦 ∃* 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑
6 rspe ⊢ ( ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) → ∃ 𝑦 ∈ 𝐵 𝜑 )
7 6 ex ⊢ ( 𝑦 ∈ 𝐵 → ( 𝜑 → ∃ 𝑦 ∈ 𝐵 𝜑 ) )
8 7 ralrimivw ⊢ ( 𝑦 ∈ 𝐵 → ∀ 𝑥 ∈ 𝐴 ( 𝜑 → ∃ 𝑦 ∈ 𝐵 𝜑 ) )
9 rmoim ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 → ∃ 𝑦 ∈ 𝐵 𝜑 ) → ( ∃* 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 → ∃* 𝑥 ∈ 𝐴 𝜑 ) )
10 8 9 syl ⊢ ( 𝑦 ∈ 𝐵 → ( ∃* 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 → ∃* 𝑥 ∈ 𝐴 𝜑 ) )
11 10 impcom ⊢ ( ( ∃* 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ∃* 𝑥 ∈ 𝐴 𝜑 )
12 rmo5 ⊢ ( ∃* 𝑥 ∈ 𝐴 𝜑 ↔ ( ∃ 𝑥 ∈ 𝐴 𝜑 → ∃! 𝑥 ∈ 𝐴 𝜑 ) )
13 11 12 sylib ⊢ ( ( ∃* 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( ∃ 𝑥 ∈ 𝐴 𝜑 → ∃! 𝑥 ∈ 𝐴 𝜑 ) )
14 13 ex ⊢ ( ∃* 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 → ( 𝑦 ∈ 𝐵 → ( ∃ 𝑥 ∈ 𝐴 𝜑 → ∃! 𝑥 ∈ 𝐴 𝜑 ) ) )
15 5 14 reximdai ⊢ ( ∃* 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 → ( ∃ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝜑 → ∃ 𝑦 ∈ 𝐵 ∃! 𝑥 ∈ 𝐴 𝜑 ) )
16 2 15 biimtrid ⊢ ( ∃* 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 → ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 → ∃ 𝑦 ∈ 𝐵 ∃! 𝑥 ∈ 𝐴 𝜑 ) )
17 16 impcom ⊢ ( ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ∧ ∃* 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ) → ∃ 𝑦 ∈ 𝐵 ∃! 𝑥 ∈ 𝐴 𝜑 )
18 1 17 sylbi ⊢ ( ∃! 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 → ∃ 𝑦 ∈ 𝐵 ∃! 𝑥 ∈ 𝐴 𝜑 )