Metamath Proof Explorer

Theorem mosubott

Description: "At most one" remains true inside ordered triple quantification, analogous to mosubopt . (Contributed by BTernaryTau, 8-Sep-2026)

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

Proof

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