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 ( ∀ 𝑦𝑧 ∃* 𝑥 𝜑 → ∃* 𝑥𝑦𝑧 ( 𝐴 = ⟨ 𝑦 , 𝑧 ⟩ ∧ 𝜑 ) )