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	imbitrdi	⊢ ( ( 𝑎 = 𝑑 ∧ ( 𝜓 → ( 𝜂 ∧ 𝑒 = 𝑓 ) ) ) → ( 𝜓 → ( 𝜂 ∧ ( 𝑎 = 𝑑 ∧ 𝑒 = 𝑓 ) ) ) )
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	biimtrrdi	⊢ ( 𝑉 ≠ ∅ → ( ( ∀ 𝑐 ∈ 𝑉 ( 𝜒 ∧ ( 𝜏 → 𝑏 = 𝑐 ) ) → 𝑎 = 𝑑 ) → ( 𝜂 → ( ( 𝜓 → 𝑒 = 𝑓 ) → ∃ 𝑐 ∈ 𝑉 ( ( 𝜒 ∧ ( 𝜏 → 𝑏 = 𝑐 ) ) → ( 𝜓 → ( 𝜂 ∧ ( 𝑎 = 𝑑 ∧ 𝑒 = 𝑓 ) ) ) ) ) ) ) )
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	⊢ ( ( 𝑉 ≠ ∅ ∧ ∃! 𝑎 ∈ 𝑉 ∃! 𝑏 ∈ 𝑉 𝜑 ) → ∃ 𝑎 ∈ 𝑉 ∀ 𝑑 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ∃ 𝑒 ∈ 𝑉 ∀ 𝑓 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( ( 𝜒 ∧ ( 𝜏 → 𝑏 = 𝑐 ) ) → ( 𝜓 → ( 𝜂 ∧ ( 𝑎 = 𝑑 ∧ 𝑒 = 𝑓 ) ) ) ) )