Metamath Proof Explorer

Theorem 2reu1

Description: Double restricted existential uniqueness. This theorem shows a condition under which a "naive" definition matches the correct one, analogous to 2eu1 . (Contributed by Alexander van der Vekens, 25-Jun-2017)

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

Proof

Step Hyp Ref Expression
1 2reu5a ⊢ ( ∃! 𝑥 ∈ 𝐴 ∃! 𝑦 ∈ 𝐵 𝜑 ↔ ( ∃ 𝑥 ∈ 𝐴 ( ∃ 𝑦 ∈ 𝐵 𝜑 ∧ ∃* 𝑦 ∈ 𝐵 𝜑 ) ∧ ∃* 𝑥 ∈ 𝐴 ( ∃ 𝑦 ∈ 𝐵 𝜑 ∧ ∃* 𝑦 ∈ 𝐵 𝜑 ) ) )
2 simprr ⊢ ( ( 𝑥 ∈ 𝐴 ∧ ( ∀ 𝑥 ∈ 𝐴 ∃* 𝑦 ∈ 𝐵 𝜑 ∧ ∃ 𝑦 ∈ 𝐵 𝜑 ) ) → ∃ 𝑦 ∈ 𝐵 𝜑 )
3 rsp ⊢ ( ∀ 𝑥 ∈ 𝐴 ∃* 𝑦 ∈ 𝐵 𝜑 → ( 𝑥 ∈ 𝐴 → ∃* 𝑦 ∈ 𝐵 𝜑 ) )
4 3 adantr ⊢ ( ( ∀ 𝑥 ∈ 𝐴 ∃* 𝑦 ∈ 𝐵 𝜑 ∧ ∃ 𝑦 ∈ 𝐵 𝜑 ) → ( 𝑥 ∈ 𝐴 → ∃* 𝑦 ∈ 𝐵 𝜑 ) )
5 4 impcom ⊢ ( ( 𝑥 ∈ 𝐴 ∧ ( ∀ 𝑥 ∈ 𝐴 ∃* 𝑦 ∈ 𝐵 𝜑 ∧ ∃ 𝑦 ∈ 𝐵 𝜑 ) ) → ∃* 𝑦 ∈ 𝐵 𝜑 )
6 2 5 jca ⊢ ( ( 𝑥 ∈ 𝐴 ∧ ( ∀ 𝑥 ∈ 𝐴 ∃* 𝑦 ∈ 𝐵 𝜑 ∧ ∃ 𝑦 ∈ 𝐵 𝜑 ) ) → ( ∃ 𝑦 ∈ 𝐵 𝜑 ∧ ∃* 𝑦 ∈ 𝐵 𝜑 ) )
7 6 ex ⊢ ( 𝑥 ∈ 𝐴 → ( ( ∀ 𝑥 ∈ 𝐴 ∃* 𝑦 ∈ 𝐵 𝜑 ∧ ∃ 𝑦 ∈ 𝐵 𝜑 ) → ( ∃ 𝑦 ∈ 𝐵 𝜑 ∧ ∃* 𝑦 ∈ 𝐵 𝜑 ) ) )
8 7 rmoimia ⊢ ( ∃* 𝑥 ∈ 𝐴 ( ∃ 𝑦 ∈ 𝐵 𝜑 ∧ ∃* 𝑦 ∈ 𝐵 𝜑 ) → ∃* 𝑥 ∈ 𝐴 ( ∀ 𝑥 ∈ 𝐴 ∃* 𝑦 ∈ 𝐵 𝜑 ∧ ∃ 𝑦 ∈ 𝐵 𝜑 ) )
9 nfra1 ⊢ Ⅎ 𝑥 ∀ 𝑥 ∈ 𝐴 ∃* 𝑦 ∈ 𝐵 𝜑
10 9 rmoanim ⊢ ( ∃* 𝑥 ∈ 𝐴 ( ∀ 𝑥 ∈ 𝐴 ∃* 𝑦 ∈ 𝐵 𝜑 ∧ ∃ 𝑦 ∈ 𝐵 𝜑 ) ↔ ( ∀ 𝑥 ∈ 𝐴 ∃* 𝑦 ∈ 𝐵 𝜑 → ∃* 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ) )
11 8 10 sylib ⊢ ( ∃* 𝑥 ∈ 𝐴 ( ∃ 𝑦 ∈ 𝐵 𝜑 ∧ ∃* 𝑦 ∈ 𝐵 𝜑 ) → ( ∀ 𝑥 ∈ 𝐴 ∃* 𝑦 ∈ 𝐵 𝜑 → ∃* 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ) )
12 11 ancrd ⊢ ( ∃* 𝑥 ∈ 𝐴 ( ∃ 𝑦 ∈ 𝐵 𝜑 ∧ ∃* 𝑦 ∈ 𝐵 𝜑 ) → ( ∀ 𝑥 ∈ 𝐴 ∃* 𝑦 ∈ 𝐵 𝜑 → ( ∃* 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 ∃* 𝑦 ∈ 𝐵 𝜑 ) ) )
13 2rmoswap ⊢ ( ∀ 𝑥 ∈ 𝐴 ∃* 𝑦 ∈ 𝐵 𝜑 → ( ∃* 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 → ∃* 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝜑 ) )
14 13 com12 ⊢ ( ∃* 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 → ( ∀ 𝑥 ∈ 𝐴 ∃* 𝑦 ∈ 𝐵 𝜑 → ∃* 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝜑 ) )
15 14 imdistani ⊢ ( ( ∃* 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 ∃* 𝑦 ∈ 𝐵 𝜑 ) → ( ∃* 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ∧ ∃* 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝜑 ) )
16 12 15 syl6 ⊢ ( ∃* 𝑥 ∈ 𝐴 ( ∃ 𝑦 ∈ 𝐵 𝜑 ∧ ∃* 𝑦 ∈ 𝐵 𝜑 ) → ( ∀ 𝑥 ∈ 𝐴 ∃* 𝑦 ∈ 𝐵 𝜑 → ( ∃* 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ∧ ∃* 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝜑 ) ) )
17 1 16 simplbiim ⊢ ( ∃! 𝑥 ∈ 𝐴 ∃! 𝑦 ∈ 𝐵 𝜑 → ( ∀ 𝑥 ∈ 𝐴 ∃* 𝑦 ∈ 𝐵 𝜑 → ( ∃* 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ∧ ∃* 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝜑 ) ) )
18 2reu2rex ⊢ ( ∃! 𝑥 ∈ 𝐴 ∃! 𝑦 ∈ 𝐵 𝜑 → ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 )
19 rexcom ⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ↔ ∃ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝜑 )
20 18 19 sylib ⊢ ( ∃! 𝑥 ∈ 𝐴 ∃! 𝑦 ∈ 𝐵 𝜑 → ∃ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝜑 )
21 18 20 jca ⊢ ( ∃! 𝑥 ∈ 𝐴 ∃! 𝑦 ∈ 𝐵 𝜑 → ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ∧ ∃ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝜑 ) )
22 17 21 jctild ⊢ ( ∃! 𝑥 ∈ 𝐴 ∃! 𝑦 ∈ 𝐵 𝜑 → ( ∀ 𝑥 ∈ 𝐴 ∃* 𝑦 ∈ 𝐵 𝜑 → ( ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ∧ ∃ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝜑 ) ∧ ( ∃* 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ∧ ∃* 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝜑 ) ) ) )
23 reu5 ⊢ ( ∃! 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ↔ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ∧ ∃* 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ) )
24 reu5 ⊢ ( ∃! 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝜑 ↔ ( ∃ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝜑 ∧ ∃* 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝜑 ) )
25 23 24 anbi12i ⊢ ( ( ∃! 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ∧ ∃! 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝜑 ) ↔ ( ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ∧ ∃* 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ) ∧ ( ∃ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝜑 ∧ ∃* 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝜑 ) ) )
26 an4 ⊢ ( ( ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ∧ ∃* 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ) ∧ ( ∃ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝜑 ∧ ∃* 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝜑 ) ) ↔ ( ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ∧ ∃ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝜑 ) ∧ ( ∃* 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ∧ ∃* 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝜑 ) ) )
27 25 26 bitri ⊢ ( ( ∃! 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ∧ ∃! 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝜑 ) ↔ ( ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ∧ ∃ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝜑 ) ∧ ( ∃* 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ∧ ∃* 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝜑 ) ) )
28 22 27 syl6ibr ⊢ ( ∃! 𝑥 ∈ 𝐴 ∃! 𝑦 ∈ 𝐵 𝜑 → ( ∀ 𝑥 ∈ 𝐴 ∃* 𝑦 ∈ 𝐵 𝜑 → ( ∃! 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ∧ ∃! 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝜑 ) ) )
29 28 com12 ⊢ ( ∀ 𝑥 ∈ 𝐴 ∃* 𝑦 ∈ 𝐵 𝜑 → ( ∃! 𝑥 ∈ 𝐴 ∃! 𝑦 ∈ 𝐵 𝜑 → ( ∃! 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ∧ ∃! 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝜑 ) ) )
30 2rexreu ⊢ ( ( ∃! 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ∧ ∃! 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝜑 ) → ∃! 𝑥 ∈ 𝐴 ∃! 𝑦 ∈ 𝐵 𝜑 )
31 29 30 impbid1 ⊢ ( ∀ 𝑥 ∈ 𝐴 ∃* 𝑦 ∈ 𝐵 𝜑 → ( ∃! 𝑥 ∈ 𝐴 ∃! 𝑦 ∈ 𝐵 𝜑 ↔ ( ∃! 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ∧ ∃! 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝜑 ) ) )