Metamath Proof Explorer

Theorem 2rmoswap

Description: A condition allowing to swap restricted "at most one" and restricted existential quantifiers, analogous to 2moswap . (Contributed by Alexander van der Vekens, 25-Jun-2017)

Ref Expression
Assertion 2rmoswap ( ∀ 𝑥 ∈ 𝐴 ∃* 𝑦 ∈ 𝐵 𝜑 → ( ∃* 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 → ∃* 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝜑 ) )

Proof

Step Hyp Ref Expression
1 df-rmo ⊢ ( ∃* 𝑦 ∈ 𝐵 𝜑 ↔ ∃* 𝑦 ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) )
2 1 ralbii ⊢ ( ∀ 𝑥 ∈ 𝐴 ∃* 𝑦 ∈ 𝐵 𝜑 ↔ ∀ 𝑥 ∈ 𝐴 ∃* 𝑦 ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) )
3 df-ral ⊢ ( ∀ 𝑥 ∈ 𝐴 ∃* 𝑦 ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ∃* 𝑦 ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ) )
4 moanimv ⊢ ( ∃* 𝑦 ( 𝑥 ∈ 𝐴 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ) ↔ ( 𝑥 ∈ 𝐴 → ∃* 𝑦 ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ) )
5 4 albii ⊢ ( ∀ 𝑥 ∃* 𝑦 ( 𝑥 ∈ 𝐴 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ∃* 𝑦 ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ) )
6 3 5 bitr4i ⊢ ( ∀ 𝑥 ∈ 𝐴 ∃* 𝑦 ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ↔ ∀ 𝑥 ∃* 𝑦 ( 𝑥 ∈ 𝐴 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ) )
7 2moswapv ⊢ ( ∀ 𝑥 ∃* 𝑦 ( 𝑥 ∈ 𝐴 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ) → ( ∃* 𝑥 ∃ 𝑦 ( 𝑥 ∈ 𝐴 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ) → ∃* 𝑦 ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ) ) )
8 df-rmo ⊢ ( ∃* 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ↔ ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ ∃ 𝑦 ∈ 𝐵 𝜑 ) )
9 r19.42v ⊢ ( ∃ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ ( 𝑥 ∈ 𝐴 ∧ ∃ 𝑦 ∈ 𝐵 𝜑 ) )
10 df-rex ⊢ ( ∃ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ ∃ 𝑦 ( 𝑦 ∈ 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) )
11 an12 ⊢ ( ( 𝑦 ∈ 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ) )
12 11 exbii ⊢ ( ∃ 𝑦 ( 𝑦 ∈ 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) ↔ ∃ 𝑦 ( 𝑥 ∈ 𝐴 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ) )
13 10 12 bitri ⊢ ( ∃ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ ∃ 𝑦 ( 𝑥 ∈ 𝐴 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ) )
14 9 13 bitr3i ⊢ ( ( 𝑥 ∈ 𝐴 ∧ ∃ 𝑦 ∈ 𝐵 𝜑 ) ↔ ∃ 𝑦 ( 𝑥 ∈ 𝐴 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ) )
15 14 mobii ⊢ ( ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ ∃ 𝑦 ∈ 𝐵 𝜑 ) ↔ ∃* 𝑥 ∃ 𝑦 ( 𝑥 ∈ 𝐴 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ) )
16 8 15 bitri ⊢ ( ∃* 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ↔ ∃* 𝑥 ∃ 𝑦 ( 𝑥 ∈ 𝐴 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ) )
17 df-rmo ⊢ ( ∃* 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝜑 ↔ ∃* 𝑦 ( 𝑦 ∈ 𝐵 ∧ ∃ 𝑥 ∈ 𝐴 𝜑 ) )
18 r19.42v ⊢ ( ∃ 𝑥 ∈ 𝐴 ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ↔ ( 𝑦 ∈ 𝐵 ∧ ∃ 𝑥 ∈ 𝐴 𝜑 ) )
19 df-rex ⊢ ( ∃ 𝑥 ∈ 𝐴 ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ) )
20 18 19 bitr3i ⊢ ( ( 𝑦 ∈ 𝐵 ∧ ∃ 𝑥 ∈ 𝐴 𝜑 ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ) )
21 20 mobii ⊢ ( ∃* 𝑦 ( 𝑦 ∈ 𝐵 ∧ ∃ 𝑥 ∈ 𝐴 𝜑 ) ↔ ∃* 𝑦 ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ) )
22 17 21 bitri ⊢ ( ∃* 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝜑 ↔ ∃* 𝑦 ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ) )
23 7 16 22 3imtr4g ⊢ ( ∀ 𝑥 ∃* 𝑦 ( 𝑥 ∈ 𝐴 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ) → ( ∃* 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 → ∃* 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝜑 ) )
24 6 23 sylbi ⊢ ( ∀ 𝑥 ∈ 𝐴 ∃* 𝑦 ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) → ( ∃* 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 → ∃* 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝜑 ) )
25 2 24 sylbi ⊢ ( ∀ 𝑥 ∈ 𝐴 ∃* 𝑦 ∈ 𝐵 𝜑 → ( ∃* 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 → ∃* 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝜑 ) )