Metamath Proof Explorer

Theorem mosubopt

Description: "At most one" remains true inside ordered pair quantification. (Contributed by NM, 28-Aug-2007)

Ref Expression
Assertion mosubopt ( ∀ 𝑦 ∀ 𝑧 ∃* 𝑥 𝜑 → ∃* 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝐴 = ⟨ 𝑦 , 𝑧 ⟩ ∧ 𝜑 ) )

Proof

Step Hyp Ref Expression
1 nfa1 ⊢ Ⅎ 𝑦 ∀ 𝑦 ∀ 𝑧 ∃* 𝑥 𝜑
2 nfe1 ⊢ Ⅎ 𝑦 ∃ 𝑦 ∃ 𝑧 ( 𝐴 = ⟨ 𝑦 , 𝑧 ⟩ ∧ 𝜑 )
3 2 nfmov ⊢ Ⅎ 𝑦 ∃* 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝐴 = ⟨ 𝑦 , 𝑧 ⟩ ∧ 𝜑 )
4 nfa1 ⊢ Ⅎ 𝑧 ∀ 𝑧 ∃* 𝑥 𝜑
5 nfe1 ⊢ Ⅎ 𝑧 ∃ 𝑧 ( 𝐴 = ⟨ 𝑦 , 𝑧 ⟩ ∧ 𝜑 )
6 5 nfex ⊢ Ⅎ 𝑧 ∃ 𝑦 ∃ 𝑧 ( 𝐴 = ⟨ 𝑦 , 𝑧 ⟩ ∧ 𝜑 )
7 6 nfmov ⊢ Ⅎ 𝑧 ∃* 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝐴 = ⟨ 𝑦 , 𝑧 ⟩ ∧ 𝜑 )
8 copsexgw ⊢ ( 𝐴 = ⟨ 𝑦 , 𝑧 ⟩ → ( 𝜑 ↔ ∃ 𝑦 ∃ 𝑧 ( 𝐴 = ⟨ 𝑦 , 𝑧 ⟩ ∧ 𝜑 ) ) )
9 8 mobidv ⊢ ( 𝐴 = ⟨ 𝑦 , 𝑧 ⟩ → ( ∃* 𝑥 𝜑 ↔ ∃* 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝐴 = ⟨ 𝑦 , 𝑧 ⟩ ∧ 𝜑 ) ) )
10 9 biimpcd ⊢ ( ∃* 𝑥 𝜑 → ( 𝐴 = ⟨ 𝑦 , 𝑧 ⟩ → ∃* 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝐴 = ⟨ 𝑦 , 𝑧 ⟩ ∧ 𝜑 ) ) )
11 10 sps ⊢ ( ∀ 𝑧 ∃* 𝑥 𝜑 → ( 𝐴 = ⟨ 𝑦 , 𝑧 ⟩ → ∃* 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝐴 = ⟨ 𝑦 , 𝑧 ⟩ ∧ 𝜑 ) ) )
12 4 7 11 exlimd ⊢ ( ∀ 𝑧 ∃* 𝑥 𝜑 → ( ∃ 𝑧 𝐴 = ⟨ 𝑦 , 𝑧 ⟩ → ∃* 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝐴 = ⟨ 𝑦 , 𝑧 ⟩ ∧ 𝜑 ) ) )
13 12 sps ⊢ ( ∀ 𝑦 ∀ 𝑧 ∃* 𝑥 𝜑 → ( ∃ 𝑧 𝐴 = ⟨ 𝑦 , 𝑧 ⟩ → ∃* 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝐴 = ⟨ 𝑦 , 𝑧 ⟩ ∧ 𝜑 ) ) )
14 1 3 13 exlimd ⊢ ( ∀ 𝑦 ∀ 𝑧 ∃* 𝑥 𝜑 → ( ∃ 𝑦 ∃ 𝑧 𝐴 = ⟨ 𝑦 , 𝑧 ⟩ → ∃* 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝐴 = ⟨ 𝑦 , 𝑧 ⟩ ∧ 𝜑 ) ) )
15 simpl ⊢ ( ( 𝐴 = ⟨ 𝑦 , 𝑧 ⟩ ∧ 𝜑 ) → 𝐴 = ⟨ 𝑦 , 𝑧 ⟩ )
16 15 2eximi ⊢ ( ∃ 𝑦 ∃ 𝑧 ( 𝐴 = ⟨ 𝑦 , 𝑧 ⟩ ∧ 𝜑 ) → ∃ 𝑦 ∃ 𝑧 𝐴 = ⟨ 𝑦 , 𝑧 ⟩ )
17 16 exlimiv ⊢ ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝐴 = ⟨ 𝑦 , 𝑧 ⟩ ∧ 𝜑 ) → ∃ 𝑦 ∃ 𝑧 𝐴 = ⟨ 𝑦 , 𝑧 ⟩ )
18 nexmo ⊢ ( ¬ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝐴 = ⟨ 𝑦 , 𝑧 ⟩ ∧ 𝜑 ) → ∃* 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝐴 = ⟨ 𝑦 , 𝑧 ⟩ ∧ 𝜑 ) )
19 17 18 nsyl5 ⊢ ( ¬ ∃ 𝑦 ∃ 𝑧 𝐴 = ⟨ 𝑦 , 𝑧 ⟩ → ∃* 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝐴 = ⟨ 𝑦 , 𝑧 ⟩ ∧ 𝜑 ) )
20 14 19 pm2.61d1 ⊢ ( ∀ 𝑦 ∀ 𝑧 ∃* 𝑥 𝜑 → ∃* 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝐴 = ⟨ 𝑦 , 𝑧 ⟩ ∧ 𝜑 ) )