Metamath Proof Explorer

Theorem 2reuimp

Description: Implication of a double restricted existential uniqueness in terms of restricted existential quantification and restricted universal quantification if the class of the quantified elements is not empty. (Contributed by AV, 13-Mar-2023)

Ref Expression
Hypotheses 2reuimp.c ⊢ ( 𝑏 = 𝑐 → ( 𝜑 ↔ 𝜃 ) )
2reuimp.d ⊢ ( 𝑎 = 𝑑 → ( 𝜑 ↔ 𝜒 ) )
2reuimp.a ⊢ ( 𝑎 = 𝑑 → ( 𝜃 ↔ 𝜏 ) )
2reuimp.e ⊢ ( 𝑏 = 𝑒 → ( 𝜑 ↔ 𝜂 ) )
2reuimp.f ⊢ ( 𝑐 = 𝑓 → ( 𝜃 ↔ 𝜓 ) )
Assertion 2reuimp ( ( 𝑉 ≠ ∅ ∧ ∃! 𝑎 ∈ 𝑉 ∃! 𝑏 ∈ 𝑉 𝜑 ) → ∃ 𝑎 ∈ 𝑉 ∀ 𝑑 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ∃ 𝑒 ∈ 𝑉 ∀ 𝑓 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( ( 𝜒 ∧ ( 𝜏 → 𝑏 = 𝑐 ) ) → ( 𝜓 → ( 𝜂 ∧ ( 𝑎 = 𝑑 ∧ 𝑒 = 𝑓 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 2reuimp.c ⊢ ( 𝑏 = 𝑐 → ( 𝜑 ↔ 𝜃 ) )
2 2reuimp.d ⊢ ( 𝑎 = 𝑑 → ( 𝜑 ↔ 𝜒 ) )
3 2reuimp.a ⊢ ( 𝑎 = 𝑑 → ( 𝜃 ↔ 𝜏 ) )
4 2reuimp.e ⊢ ( 𝑏 = 𝑒 → ( 𝜑 ↔ 𝜂 ) )
5 2reuimp.f ⊢ ( 𝑐 = 𝑓 → ( 𝜃 ↔ 𝜓 ) )
6 r19.28zv ⊢ ( 𝑉 ≠ ∅ → ( ∀ 𝑐 ∈ 𝑉 ( 𝜒 ∧ ( 𝜏 → 𝑏 = 𝑐 ) ) ↔ ( 𝜒 ∧ ∀ 𝑐 ∈ 𝑉 ( 𝜏 → 𝑏 = 𝑐 ) ) ) )
7 6 bicomd ⊢ ( 𝑉 ≠ ∅ → ( ( 𝜒 ∧ ∀ 𝑐 ∈ 𝑉 ( 𝜏 → 𝑏 = 𝑐 ) ) ↔ ∀ 𝑐 ∈ 𝑉 ( 𝜒 ∧ ( 𝜏 → 𝑏 = 𝑐 ) ) ) )
8 7 imbi1d ⊢ ( 𝑉 ≠ ∅ → ( ( ( 𝜒 ∧ ∀ 𝑐 ∈ 𝑉 ( 𝜏 → 𝑏 = 𝑐 ) ) → 𝑎 = 𝑑 ) ↔ ( ∀ 𝑐 ∈ 𝑉 ( 𝜒 ∧ ( 𝜏 → 𝑏 = 𝑐 ) ) → 𝑎 = 𝑑 ) ) )
9 r19.36zv ⊢ ( 𝑉 ≠ ∅ → ( ∃ 𝑐 ∈ 𝑉 ( ( 𝜒 ∧ ( 𝜏 → 𝑏 = 𝑐 ) ) → 𝑎 = 𝑑 ) ↔ ( ∀ 𝑐 ∈ 𝑉 ( 𝜒 ∧ ( 𝜏 → 𝑏 = 𝑐 ) ) → 𝑎 = 𝑑 ) ) )
10 r19.42v ⊢ ( ∃ 𝑐 ∈ 𝑉 ( ( 𝜂 ∧ ( 𝜓 → 𝑒 = 𝑓 ) ) ∧ ( ( 𝜒 ∧ ( 𝜏 → 𝑏 = 𝑐 ) ) → 𝑎 = 𝑑 ) ) ↔ ( ( 𝜂 ∧ ( 𝜓 → 𝑒 = 𝑓 ) ) ∧ ∃ 𝑐 ∈ 𝑉 ( ( 𝜒 ∧ ( 𝜏 → 𝑏 = 𝑐 ) ) → 𝑎 = 𝑑 ) ) )
11 pm5.31r ⊢ ( ( 𝜂 ∧ ( 𝜓 → 𝑒 = 𝑓 ) ) → ( 𝜓 → ( 𝜂 ∧ 𝑒 = 𝑓 ) ) )
12 pm5.31r ⊢ ( ( ( 𝜓 → ( 𝜂 ∧ 𝑒 = 𝑓 ) ) ∧ ( ( 𝜒 ∧ ( 𝜏 → 𝑏 = 𝑐 ) ) → 𝑎 = 𝑑 ) ) → ( ( 𝜒 ∧ ( 𝜏 → 𝑏 = 𝑐 ) ) → ( ( 𝜓 → ( 𝜂 ∧ 𝑒 = 𝑓 ) ) ∧ 𝑎 = 𝑑 ) ) )
13 pm5.31r ⊢ ( ( 𝑎 = 𝑑 ∧ ( 𝜓 → ( 𝜂 ∧ 𝑒 = 𝑓 ) ) ) → ( 𝜓 → ( 𝑎 = 𝑑 ∧ ( 𝜂 ∧ 𝑒 = 𝑓 ) ) ) )
14 an12 ⊢ ( ( 𝑎 = 𝑑 ∧ ( 𝜂 ∧ 𝑒 = 𝑓 ) ) ↔ ( 𝜂 ∧ ( 𝑎 = 𝑑 ∧ 𝑒 = 𝑓 ) ) )
15 13 14 syl6ib ⊢ ( ( 𝑎 = 𝑑 ∧ ( 𝜓 → ( 𝜂 ∧ 𝑒 = 𝑓 ) ) ) → ( 𝜓 → ( 𝜂 ∧ ( 𝑎 = 𝑑 ∧ 𝑒 = 𝑓 ) ) ) )
16 15 ancoms ⊢ ( ( ( 𝜓 → ( 𝜂 ∧ 𝑒 = 𝑓 ) ) ∧ 𝑎 = 𝑑 ) → ( 𝜓 → ( 𝜂 ∧ ( 𝑎 = 𝑑 ∧ 𝑒 = 𝑓 ) ) ) )
17 12 16 syl6 ⊢ ( ( ( 𝜓 → ( 𝜂 ∧ 𝑒 = 𝑓 ) ) ∧ ( ( 𝜒 ∧ ( 𝜏 → 𝑏 = 𝑐 ) ) → 𝑎 = 𝑑 ) ) → ( ( 𝜒 ∧ ( 𝜏 → 𝑏 = 𝑐 ) ) → ( 𝜓 → ( 𝜂 ∧ ( 𝑎 = 𝑑 ∧ 𝑒 = 𝑓 ) ) ) ) )
18 11 17 sylan ⊢ ( ( ( 𝜂 ∧ ( 𝜓 → 𝑒 = 𝑓 ) ) ∧ ( ( 𝜒 ∧ ( 𝜏 → 𝑏 = 𝑐 ) ) → 𝑎 = 𝑑 ) ) → ( ( 𝜒 ∧ ( 𝜏 → 𝑏 = 𝑐 ) ) → ( 𝜓 → ( 𝜂 ∧ ( 𝑎 = 𝑑 ∧ 𝑒 = 𝑓 ) ) ) ) )
19 18 reximi ⊢ ( ∃ 𝑐 ∈ 𝑉 ( ( 𝜂 ∧ ( 𝜓 → 𝑒 = 𝑓 ) ) ∧ ( ( 𝜒 ∧ ( 𝜏 → 𝑏 = 𝑐 ) ) → 𝑎 = 𝑑 ) ) → ∃ 𝑐 ∈ 𝑉 ( ( 𝜒 ∧ ( 𝜏 → 𝑏 = 𝑐 ) ) → ( 𝜓 → ( 𝜂 ∧ ( 𝑎 = 𝑑 ∧ 𝑒 = 𝑓 ) ) ) ) )
20 10 19 sylbir ⊢ ( ( ( 𝜂 ∧ ( 𝜓 → 𝑒 = 𝑓 ) ) ∧ ∃ 𝑐 ∈ 𝑉 ( ( 𝜒 ∧ ( 𝜏 → 𝑏 = 𝑐 ) ) → 𝑎 = 𝑑 ) ) → ∃ 𝑐 ∈ 𝑉 ( ( 𝜒 ∧ ( 𝜏 → 𝑏 = 𝑐 ) ) → ( 𝜓 → ( 𝜂 ∧ ( 𝑎 = 𝑑 ∧ 𝑒 = 𝑓 ) ) ) ) )
21 20 expcom ⊢ ( ∃ 𝑐 ∈ 𝑉 ( ( 𝜒 ∧ ( 𝜏 → 𝑏 = 𝑐 ) ) → 𝑎 = 𝑑 ) → ( ( 𝜂 ∧ ( 𝜓 → 𝑒 = 𝑓 ) ) → ∃ 𝑐 ∈ 𝑉 ( ( 𝜒 ∧ ( 𝜏 → 𝑏 = 𝑐 ) ) → ( 𝜓 → ( 𝜂 ∧ ( 𝑎 = 𝑑 ∧ 𝑒 = 𝑓 ) ) ) ) ) )
22 21 expd ⊢ ( ∃ 𝑐 ∈ 𝑉 ( ( 𝜒 ∧ ( 𝜏 → 𝑏 = 𝑐 ) ) → 𝑎 = 𝑑 ) → ( 𝜂 → ( ( 𝜓 → 𝑒 = 𝑓 ) → ∃ 𝑐 ∈ 𝑉 ( ( 𝜒 ∧ ( 𝜏 → 𝑏 = 𝑐 ) ) → ( 𝜓 → ( 𝜂 ∧ ( 𝑎 = 𝑑 ∧ 𝑒 = 𝑓 ) ) ) ) ) ) )
23 9 22 syl6bir ⊢ ( 𝑉 ≠ ∅ → ( ( ∀ 𝑐 ∈ 𝑉 ( 𝜒 ∧ ( 𝜏 → 𝑏 = 𝑐 ) ) → 𝑎 = 𝑑 ) → ( 𝜂 → ( ( 𝜓 → 𝑒 = 𝑓 ) → ∃ 𝑐 ∈ 𝑉 ( ( 𝜒 ∧ ( 𝜏 → 𝑏 = 𝑐 ) ) → ( 𝜓 → ( 𝜂 ∧ ( 𝑎 = 𝑑 ∧ 𝑒 = 𝑓 ) ) ) ) ) ) ) )
24 8 23 sylbid ⊢ ( 𝑉 ≠ ∅ → ( ( ( 𝜒 ∧ ∀ 𝑐 ∈ 𝑉 ( 𝜏 → 𝑏 = 𝑐 ) ) → 𝑎 = 𝑑 ) → ( 𝜂 → ( ( 𝜓 → 𝑒 = 𝑓 ) → ∃ 𝑐 ∈ 𝑉 ( ( 𝜒 ∧ ( 𝜏 → 𝑏 = 𝑐 ) ) → ( 𝜓 → ( 𝜂 ∧ ( 𝑎 = 𝑑 ∧ 𝑒 = 𝑓 ) ) ) ) ) ) ) )
25 24 com23 ⊢ ( 𝑉 ≠ ∅ → ( 𝜂 → ( ( ( 𝜒 ∧ ∀ 𝑐 ∈ 𝑉 ( 𝜏 → 𝑏 = 𝑐 ) ) → 𝑎 = 𝑑 ) → ( ( 𝜓 → 𝑒 = 𝑓 ) → ∃ 𝑐 ∈ 𝑉 ( ( 𝜒 ∧ ( 𝜏 → 𝑏 = 𝑐 ) ) → ( 𝜓 → ( 𝜂 ∧ ( 𝑎 = 𝑑 ∧ 𝑒 = 𝑓 ) ) ) ) ) ) ) )
26 25 imp4c ⊢ ( 𝑉 ≠ ∅ → ( ( ( 𝜂 ∧ ( ( 𝜒 ∧ ∀ 𝑐 ∈ 𝑉 ( 𝜏 → 𝑏 = 𝑐 ) ) → 𝑎 = 𝑑 ) ) ∧ ( 𝜓 → 𝑒 = 𝑓 ) ) → ∃ 𝑐 ∈ 𝑉 ( ( 𝜒 ∧ ( 𝜏 → 𝑏 = 𝑐 ) ) → ( 𝜓 → ( 𝜂 ∧ ( 𝑎 = 𝑑 ∧ 𝑒 = 𝑓 ) ) ) ) ) )
27 26 ralimdv ⊢ ( 𝑉 ≠ ∅ → ( ∀ 𝑓 ∈ 𝑉 ( ( 𝜂 ∧ ( ( 𝜒 ∧ ∀ 𝑐 ∈ 𝑉 ( 𝜏 → 𝑏 = 𝑐 ) ) → 𝑎 = 𝑑 ) ) ∧ ( 𝜓 → 𝑒 = 𝑓 ) ) → ∀ 𝑓 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( ( 𝜒 ∧ ( 𝜏 → 𝑏 = 𝑐 ) ) → ( 𝜓 → ( 𝜂 ∧ ( 𝑎 = 𝑑 ∧ 𝑒 = 𝑓 ) ) ) ) ) )
28 27 reximdv ⊢ ( 𝑉 ≠ ∅ → ( ∃ 𝑒 ∈ 𝑉 ∀ 𝑓 ∈ 𝑉 ( ( 𝜂 ∧ ( ( 𝜒 ∧ ∀ 𝑐 ∈ 𝑉 ( 𝜏 → 𝑏 = 𝑐 ) ) → 𝑎 = 𝑑 ) ) ∧ ( 𝜓 → 𝑒 = 𝑓 ) ) → ∃ 𝑒 ∈ 𝑉 ∀ 𝑓 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( ( 𝜒 ∧ ( 𝜏 → 𝑏 = 𝑐 ) ) → ( 𝜓 → ( 𝜂 ∧ ( 𝑎 = 𝑑 ∧ 𝑒 = 𝑓 ) ) ) ) ) )
29 28 ralimdv ⊢ ( 𝑉 ≠ ∅ → ( ∀ 𝑏 ∈ 𝑉 ∃ 𝑒 ∈ 𝑉 ∀ 𝑓 ∈ 𝑉 ( ( 𝜂 ∧ ( ( 𝜒 ∧ ∀ 𝑐 ∈ 𝑉 ( 𝜏 → 𝑏 = 𝑐 ) ) → 𝑎 = 𝑑 ) ) ∧ ( 𝜓 → 𝑒 = 𝑓 ) ) → ∀ 𝑏 ∈ 𝑉 ∃ 𝑒 ∈ 𝑉 ∀ 𝑓 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( ( 𝜒 ∧ ( 𝜏 → 𝑏 = 𝑐 ) ) → ( 𝜓 → ( 𝜂 ∧ ( 𝑎 = 𝑑 ∧ 𝑒 = 𝑓 ) ) ) ) ) )
30 29 ralimdv ⊢ ( 𝑉 ≠ ∅ → ( ∀ 𝑑 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ∃ 𝑒 ∈ 𝑉 ∀ 𝑓 ∈ 𝑉 ( ( 𝜂 ∧ ( ( 𝜒 ∧ ∀ 𝑐 ∈ 𝑉 ( 𝜏 → 𝑏 = 𝑐 ) ) → 𝑎 = 𝑑 ) ) ∧ ( 𝜓 → 𝑒 = 𝑓 ) ) → ∀ 𝑑 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ∃ 𝑒 ∈ 𝑉 ∀ 𝑓 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( ( 𝜒 ∧ ( 𝜏 → 𝑏 = 𝑐 ) ) → ( 𝜓 → ( 𝜂 ∧ ( 𝑎 = 𝑑 ∧ 𝑒 = 𝑓 ) ) ) ) ) )
31 30 reximdv ⊢ ( 𝑉 ≠ ∅ → ( ∃ 𝑎 ∈ 𝑉 ∀ 𝑑 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ∃ 𝑒 ∈ 𝑉 ∀ 𝑓 ∈ 𝑉 ( ( 𝜂 ∧ ( ( 𝜒 ∧ ∀ 𝑐 ∈ 𝑉 ( 𝜏 → 𝑏 = 𝑐 ) ) → 𝑎 = 𝑑 ) ) ∧ ( 𝜓 → 𝑒 = 𝑓 ) ) → ∃ 𝑎 ∈ 𝑉 ∀ 𝑑 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ∃ 𝑒 ∈ 𝑉 ∀ 𝑓 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( ( 𝜒 ∧ ( 𝜏 → 𝑏 = 𝑐 ) ) → ( 𝜓 → ( 𝜂 ∧ ( 𝑎 = 𝑑 ∧ 𝑒 = 𝑓 ) ) ) ) ) )
32 1 2 3 4 5 2reuimp0 ⊢ ( ∃! 𝑎 ∈ 𝑉 ∃! 𝑏 ∈ 𝑉 𝜑 → ∃ 𝑎 ∈ 𝑉 ∀ 𝑑 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ∃ 𝑒 ∈ 𝑉 ∀ 𝑓 ∈ 𝑉 ( ( 𝜂 ∧ ( ( 𝜒 ∧ ∀ 𝑐 ∈ 𝑉 ( 𝜏 → 𝑏 = 𝑐 ) ) → 𝑎 = 𝑑 ) ) ∧ ( 𝜓 → 𝑒 = 𝑓 ) ) )
33 31 32 impel ⊢ ( ( 𝑉 ≠ ∅ ∧ ∃! 𝑎 ∈ 𝑉 ∃! 𝑏 ∈ 𝑉 𝜑 ) → ∃ 𝑎 ∈ 𝑉 ∀ 𝑑 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ∃ 𝑒 ∈ 𝑉 ∀ 𝑓 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( ( 𝜒 ∧ ( 𝜏 → 𝑏 = 𝑐 ) ) → ( 𝜓 → ( 𝜂 ∧ ( 𝑎 = 𝑑 ∧ 𝑒 = 𝑓 ) ) ) ) )