Metamath Proof Explorer

Theorem 2reu3

Description: Double restricted existential uniqueness, analogous to 2eu3 . (Contributed by Alexander van der Vekens, 29-Jun-2017)

Ref Expression
Assertion 2reu3 ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( ∃* 𝑥 ∈ 𝐴 𝜑 ∨ ∃* 𝑦 ∈ 𝐵 𝜑 ) → ( ( ∃! 𝑥 ∈ 𝐴 ∃! 𝑦 ∈ 𝐵 𝜑 ∧ ∃! 𝑦 ∈ 𝐵 ∃! 𝑥 ∈ 𝐴 𝜑 ) ↔ ( ∃! 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ∧ ∃! 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝜑 ) ) )

Proof

Step Hyp Ref Expression
1 orcom ⊢ ( ( ∃* 𝑥 ∈ 𝐴 𝜑 ∨ ∃* 𝑦 ∈ 𝐵 𝜑 ) ↔ ( ∃* 𝑦 ∈ 𝐵 𝜑 ∨ ∃* 𝑥 ∈ 𝐴 𝜑 ) )
2 1 ralbii ⊢ ( ∀ 𝑦 ∈ 𝐵 ( ∃* 𝑥 ∈ 𝐴 𝜑 ∨ ∃* 𝑦 ∈ 𝐵 𝜑 ) ↔ ∀ 𝑦 ∈ 𝐵 ( ∃* 𝑦 ∈ 𝐵 𝜑 ∨ ∃* 𝑥 ∈ 𝐴 𝜑 ) )
3 nfrmo1 ⊢ Ⅎ 𝑦 ∃* 𝑦 ∈ 𝐵 𝜑
4 3 r19.32 ⊢ ( ∀ 𝑦 ∈ 𝐵 ( ∃* 𝑦 ∈ 𝐵 𝜑 ∨ ∃* 𝑥 ∈ 𝐴 𝜑 ) ↔ ( ∃* 𝑦 ∈ 𝐵 𝜑 ∨ ∀ 𝑦 ∈ 𝐵 ∃* 𝑥 ∈ 𝐴 𝜑 ) )
5 2 4 bitri ⊢ ( ∀ 𝑦 ∈ 𝐵 ( ∃* 𝑥 ∈ 𝐴 𝜑 ∨ ∃* 𝑦 ∈ 𝐵 𝜑 ) ↔ ( ∃* 𝑦 ∈ 𝐵 𝜑 ∨ ∀ 𝑦 ∈ 𝐵 ∃* 𝑥 ∈ 𝐴 𝜑 ) )
6 orcom ⊢ ( ( ∃* 𝑦 ∈ 𝐵 𝜑 ∨ ∀ 𝑦 ∈ 𝐵 ∃* 𝑥 ∈ 𝐴 𝜑 ) ↔ ( ∀ 𝑦 ∈ 𝐵 ∃* 𝑥 ∈ 𝐴 𝜑 ∨ ∃* 𝑦 ∈ 𝐵 𝜑 ) )
7 5 6 bitri ⊢ ( ∀ 𝑦 ∈ 𝐵 ( ∃* 𝑥 ∈ 𝐴 𝜑 ∨ ∃* 𝑦 ∈ 𝐵 𝜑 ) ↔ ( ∀ 𝑦 ∈ 𝐵 ∃* 𝑥 ∈ 𝐴 𝜑 ∨ ∃* 𝑦 ∈ 𝐵 𝜑 ) )
8 7 ralbii ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( ∃* 𝑥 ∈ 𝐴 𝜑 ∨ ∃* 𝑦 ∈ 𝐵 𝜑 ) ↔ ∀ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐵 ∃* 𝑥 ∈ 𝐴 𝜑 ∨ ∃* 𝑦 ∈ 𝐵 𝜑 ) )
9 nfcv ⊢ Ⅎ 𝑥 𝐵
10 nfrmo1 ⊢ Ⅎ 𝑥 ∃* 𝑥 ∈ 𝐴 𝜑
11 9 10 nfralw ⊢ Ⅎ 𝑥 ∀ 𝑦 ∈ 𝐵 ∃* 𝑥 ∈ 𝐴 𝜑
12 11 r19.32 ⊢ ( ∀ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐵 ∃* 𝑥 ∈ 𝐴 𝜑 ∨ ∃* 𝑦 ∈ 𝐵 𝜑 ) ↔ ( ∀ 𝑦 ∈ 𝐵 ∃* 𝑥 ∈ 𝐴 𝜑 ∨ ∀ 𝑥 ∈ 𝐴 ∃* 𝑦 ∈ 𝐵 𝜑 ) )
13 8 12 bitri ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( ∃* 𝑥 ∈ 𝐴 𝜑 ∨ ∃* 𝑦 ∈ 𝐵 𝜑 ) ↔ ( ∀ 𝑦 ∈ 𝐵 ∃* 𝑥 ∈ 𝐴 𝜑 ∨ ∀ 𝑥 ∈ 𝐴 ∃* 𝑦 ∈ 𝐵 𝜑 ) )
14 2reu1 ⊢ ( ∀ 𝑦 ∈ 𝐵 ∃* 𝑥 ∈ 𝐴 𝜑 → ( ∃! 𝑦 ∈ 𝐵 ∃! 𝑥 ∈ 𝐴 𝜑 ↔ ( ∃! 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝜑 ∧ ∃! 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ) ) )
15 14 biimpd ⊢ ( ∀ 𝑦 ∈ 𝐵 ∃* 𝑥 ∈ 𝐴 𝜑 → ( ∃! 𝑦 ∈ 𝐵 ∃! 𝑥 ∈ 𝐴 𝜑 → ( ∃! 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝜑 ∧ ∃! 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ) ) )
16 ancom ⊢ ( ( ∃! 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝜑 ∧ ∃! 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ) ↔ ( ∃! 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ∧ ∃! 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝜑 ) )
17 15 16 imbitrdi ⊢ ( ∀ 𝑦 ∈ 𝐵 ∃* 𝑥 ∈ 𝐴 𝜑 → ( ∃! 𝑦 ∈ 𝐵 ∃! 𝑥 ∈ 𝐴 𝜑 → ( ∃! 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ∧ ∃! 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝜑 ) ) )
18 17 adantld ⊢ ( ∀ 𝑦 ∈ 𝐵 ∃* 𝑥 ∈ 𝐴 𝜑 → ( ( ∃! 𝑥 ∈ 𝐴 ∃! 𝑦 ∈ 𝐵 𝜑 ∧ ∃! 𝑦 ∈ 𝐵 ∃! 𝑥 ∈ 𝐴 𝜑 ) → ( ∃! 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ∧ ∃! 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝜑 ) ) )
19 2reu1 ⊢ ( ∀ 𝑥 ∈ 𝐴 ∃* 𝑦 ∈ 𝐵 𝜑 → ( ∃! 𝑥 ∈ 𝐴 ∃! 𝑦 ∈ 𝐵 𝜑 ↔ ( ∃! 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ∧ ∃! 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝜑 ) ) )
20 19 biimpd ⊢ ( ∀ 𝑥 ∈ 𝐴 ∃* 𝑦 ∈ 𝐵 𝜑 → ( ∃! 𝑥 ∈ 𝐴 ∃! 𝑦 ∈ 𝐵 𝜑 → ( ∃! 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ∧ ∃! 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝜑 ) ) )
21 20 adantrd ⊢ ( ∀ 𝑥 ∈ 𝐴 ∃* 𝑦 ∈ 𝐵 𝜑 → ( ( ∃! 𝑥 ∈ 𝐴 ∃! 𝑦 ∈ 𝐵 𝜑 ∧ ∃! 𝑦 ∈ 𝐵 ∃! 𝑥 ∈ 𝐴 𝜑 ) → ( ∃! 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ∧ ∃! 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝜑 ) ) )
22 18 21 jaoi ⊢ ( ( ∀ 𝑦 ∈ 𝐵 ∃* 𝑥 ∈ 𝐴 𝜑 ∨ ∀ 𝑥 ∈ 𝐴 ∃* 𝑦 ∈ 𝐵 𝜑 ) → ( ( ∃! 𝑥 ∈ 𝐴 ∃! 𝑦 ∈ 𝐵 𝜑 ∧ ∃! 𝑦 ∈ 𝐵 ∃! 𝑥 ∈ 𝐴 𝜑 ) → ( ∃! 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ∧ ∃! 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝜑 ) ) )
23 2rexreu ⊢ ( ( ∃! 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ∧ ∃! 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝜑 ) → ∃! 𝑥 ∈ 𝐴 ∃! 𝑦 ∈ 𝐵 𝜑 )
24 2rexreu ⊢ ( ( ∃! 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝜑 ∧ ∃! 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ) → ∃! 𝑦 ∈ 𝐵 ∃! 𝑥 ∈ 𝐴 𝜑 )
25 24 ancoms ⊢ ( ( ∃! 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ∧ ∃! 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝜑 ) → ∃! 𝑦 ∈ 𝐵 ∃! 𝑥 ∈ 𝐴 𝜑 )
26 23 25 jca ⊢ ( ( ∃! 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ∧ ∃! 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝜑 ) → ( ∃! 𝑥 ∈ 𝐴 ∃! 𝑦 ∈ 𝐵 𝜑 ∧ ∃! 𝑦 ∈ 𝐵 ∃! 𝑥 ∈ 𝐴 𝜑 ) )
27 22 26 impbid1 ⊢ ( ( ∀ 𝑦 ∈ 𝐵 ∃* 𝑥 ∈ 𝐴 𝜑 ∨ ∀ 𝑥 ∈ 𝐴 ∃* 𝑦 ∈ 𝐵 𝜑 ) → ( ( ∃! 𝑥 ∈ 𝐴 ∃! 𝑦 ∈ 𝐵 𝜑 ∧ ∃! 𝑦 ∈ 𝐵 ∃! 𝑥 ∈ 𝐴 𝜑 ) ↔ ( ∃! 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ∧ ∃! 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝜑 ) ) )
28 13 27 sylbi ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( ∃* 𝑥 ∈ 𝐴 𝜑 ∨ ∃* 𝑦 ∈ 𝐵 𝜑 ) → ( ( ∃! 𝑥 ∈ 𝐴 ∃! 𝑦 ∈ 𝐵 𝜑 ∧ ∃! 𝑦 ∈ 𝐵 ∃! 𝑥 ∈ 𝐴 𝜑 ) ↔ ( ∃! 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ∧ ∃! 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝜑 ) ) )