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	$⊢ b = c \to (φ \leftrightarrow θ)$
	2reuimp.d	$⊢ a = d \to (φ \leftrightarrow χ)$
	2reuimp.a	$⊢ a = d \to (θ \leftrightarrow τ)$
	2reuimp.e	$⊢ b = e \to (φ \leftrightarrow η)$
	2reuimp.f	$⊢ c = f \to (θ \leftrightarrow ψ)$
Assertion	2reuimp	$⊢ (V \neq \emptyset \land \exists! a \in V \exists! b \in V φ) \to \exists a \in V \forall d \in V \forall b \in V \exists e \in V \forall f \in V \exists c \in V ((χ \land (τ \to b = c)) \to (ψ \to (η \land (a = d \land e = f))))$

Proof

Step	Hyp	Ref	Expression
1		2reuimp.c	$⊢ b = c \to (φ \leftrightarrow θ)$
2		2reuimp.d	$⊢ a = d \to (φ \leftrightarrow χ)$
3		2reuimp.a	$⊢ a = d \to (θ \leftrightarrow τ)$
4		2reuimp.e	$⊢ b = e \to (φ \leftrightarrow η)$
5		2reuimp.f	$⊢ c = f \to (θ \leftrightarrow ψ)$
6		r19.28zv	$⊢ V \neq \emptyset \to (\forall c \in V (χ \land (τ \to b = c)) \leftrightarrow (χ \land \forall c \in V (τ \to b = c)))$
7	6	bicomd	$⊢ V \neq \emptyset \to ((χ \land \forall c \in V (τ \to b = c)) \leftrightarrow \forall c \in V (χ \land (τ \to b = c)))$
8	7	imbi1d	$⊢ V \neq \emptyset \to (((χ \land \forall c \in V (τ \to b = c)) \to a = d) \leftrightarrow (\forall c \in V (χ \land (τ \to b = c)) \to a = d))$
9		r19.36zv	$⊢ V \neq \emptyset \to (\exists c \in V ((χ \land (τ \to b = c)) \to a = d) \leftrightarrow (\forall c \in V (χ \land (τ \to b = c)) \to a = d))$
10		r19.42v	$⊢ \exists c \in V ((η \land (ψ \to e = f)) \land ((χ \land (τ \to b = c)) \to a = d)) \leftrightarrow ((η \land (ψ \to e = f)) \land \exists c \in V ((χ \land (τ \to b = c)) \to a = d))$
11		pm5.31r	$⊢ (η \land (ψ \to e = f)) \to (ψ \to (η \land e = f))$
12		pm5.31r	$⊢ ((ψ \to (η \land e = f)) \land ((χ \land (τ \to b = c)) \to a = d)) \to ((χ \land (τ \to b = c)) \to ((ψ \to (η \land e = f)) \land a = d))$
13		pm5.31r	$⊢ (a = d \land (ψ \to (η \land e = f))) \to (ψ \to (a = d \land (η \land e = f)))$
14		an12	$⊢ (a = d \land (η \land e = f)) \leftrightarrow (η \land (a = d \land e = f))$
15	13 14	imbitrdi	$⊢ (a = d \land (ψ \to (η \land e = f))) \to (ψ \to (η \land (a = d \land e = f)))$
16	15	ancoms	$⊢ ((ψ \to (η \land e = f)) \land a = d) \to (ψ \to (η \land (a = d \land e = f)))$
17	12 16	syl6	$⊢ ((ψ \to (η \land e = f)) \land ((χ \land (τ \to b = c)) \to a = d)) \to ((χ \land (τ \to b = c)) \to (ψ \to (η \land (a = d \land e = f))))$
18	11 17	sylan	$⊢ ((η \land (ψ \to e = f)) \land ((χ \land (τ \to b = c)) \to a = d)) \to ((χ \land (τ \to b = c)) \to (ψ \to (η \land (a = d \land e = f))))$
19	18	reximi	$⊢ \exists c \in V ((η \land (ψ \to e = f)) \land ((χ \land (τ \to b = c)) \to a = d)) \to \exists c \in V ((χ \land (τ \to b = c)) \to (ψ \to (η \land (a = d \land e = f))))$
20	10 19	sylbir	$⊢ ((η \land (ψ \to e = f)) \land \exists c \in V ((χ \land (τ \to b = c)) \to a = d)) \to \exists c \in V ((χ \land (τ \to b = c)) \to (ψ \to (η \land (a = d \land e = f))))$
21	20	expcom	$⊢ \exists c \in V ((χ \land (τ \to b = c)) \to a = d) \to ((η \land (ψ \to e = f)) \to \exists c \in V ((χ \land (τ \to b = c)) \to (ψ \to (η \land (a = d \land e = f)))))$
22	21	expd	$⊢ \exists c \in V ((χ \land (τ \to b = c)) \to a = d) \to (η \to ((ψ \to e = f) \to \exists c \in V ((χ \land (τ \to b = c)) \to (ψ \to (η \land (a = d \land e = f))))))$
23	9 22	syl6bir	$⊢ V \neq \emptyset \to ((\forall c \in V (χ \land (τ \to b = c)) \to a = d) \to (η \to ((ψ \to e = f) \to \exists c \in V ((χ \land (τ \to b = c)) \to (ψ \to (η \land (a = d \land e = f)))))))$
24	8 23	sylbid	$⊢ V \neq \emptyset \to (((χ \land \forall c \in V (τ \to b = c)) \to a = d) \to (η \to ((ψ \to e = f) \to \exists c \in V ((χ \land (τ \to b = c)) \to (ψ \to (η \land (a = d \land e = f)))))))$
25	24	com23	$⊢ V \neq \emptyset \to (η \to (((χ \land \forall c \in V (τ \to b = c)) \to a = d) \to ((ψ \to e = f) \to \exists c \in V ((χ \land (τ \to b = c)) \to (ψ \to (η \land (a = d \land e = f)))))))$
26	25	imp4c	$⊢ V \neq \emptyset \to (((η \land ((χ \land \forall c \in V (τ \to b = c)) \to a = d)) \land (ψ \to e = f)) \to \exists c \in V ((χ \land (τ \to b = c)) \to (ψ \to (η \land (a = d \land e = f)))))$
27	26	ralimdv	$⊢ V \neq \emptyset \to (\forall f \in V ((η \land ((χ \land \forall c \in V (τ \to b = c)) \to a = d)) \land (ψ \to e = f)) \to \forall f \in V \exists c \in V ((χ \land (τ \to b = c)) \to (ψ \to (η \land (a = d \land e = f)))))$
28	27	reximdv	$⊢ V \neq \emptyset \to (\exists e \in V \forall f \in V ((η \land ((χ \land \forall c \in V (τ \to b = c)) \to a = d)) \land (ψ \to e = f)) \to \exists e \in V \forall f \in V \exists c \in V ((χ \land (τ \to b = c)) \to (ψ \to (η \land (a = d \land e = f)))))$
29	28	ralimdv	$⊢ V \neq \emptyset \to (\forall b \in V \exists e \in V \forall f \in V ((η \land ((χ \land \forall c \in V (τ \to b = c)) \to a = d)) \land (ψ \to e = f)) \to \forall b \in V \exists e \in V \forall f \in V \exists c \in V ((χ \land (τ \to b = c)) \to (ψ \to (η \land (a = d \land e = f)))))$
30	29	ralimdv	$⊢ V \neq \emptyset \to (\forall d \in V \forall b \in V \exists e \in V \forall f \in V ((η \land ((χ \land \forall c \in V (τ \to b = c)) \to a = d)) \land (ψ \to e = f)) \to \forall d \in V \forall b \in V \exists e \in V \forall f \in V \exists c \in V ((χ \land (τ \to b = c)) \to (ψ \to (η \land (a = d \land e = f)))))$
31	30	reximdv	$⊢ V \neq \emptyset \to (\exists a \in V \forall d \in V \forall b \in V \exists e \in V \forall f \in V ((η \land ((χ \land \forall c \in V (τ \to b = c)) \to a = d)) \land (ψ \to e = f)) \to \exists a \in V \forall d \in V \forall b \in V \exists e \in V \forall f \in V \exists c \in V ((χ \land (τ \to b = c)) \to (ψ \to (η \land (a = d \land e = f)))))$
32	1 2 3 4 5	2reuimp0	$⊢ \exists! a \in V \exists! b \in V φ \to \exists a \in V \forall d \in V \forall b \in V \exists e \in V \forall f \in V ((η \land ((χ \land \forall c \in V (τ \to b = c)) \to a = d)) \land (ψ \to e = f))$
33	31 32	impel	$⊢ (V \neq \emptyset \land \exists! a \in V \exists! b \in V φ) \to \exists a \in V \forall d \in V \forall b \in V \exists e \in V \forall f \in V \exists c \in V ((χ \land (τ \to b = c)) \to (ψ \to (η \land (a = d \land e = f))))$

Metamath Proof Explorer

Theorem 2reuimp

Proof