Metamath Proof Explorer

Theorem 2reuimp0

Description: Implication of a double restricted existential uniqueness in terms of restricted existential quantification and restricted universal quantification. The involved wffs depend on the setvar variables as follows: ph(a,b), th(a,c), ch(d,b), ta(d,c), et(a,e), ps(a,f) (Contributed by AV, 13-Mar-2023)

Ref Expression
Hypotheses 2reuimp.c ⊢ b = c → φ ↔ θ
2reuimp.d ⊢ a = d → φ ↔ χ
2reuimp.a ⊢ a = d → θ ↔ τ
2reuimp.e ⊢ b = e → φ ↔ η
2reuimp.f ⊢ c = f → θ ↔ ψ
Assertion 2reuimp0 ⊢ ∃! a ∈ V ∃! b ∈ V φ → ∃ a ∈ V ∀ d ∈ V ∀ b ∈ V ∃ e ∈ V ∀ f ∈ V η ∧ χ ∧ ∀ c ∈ V τ → b = c → a = d ∧ ψ → e = f

Proof

Step Hyp Ref Expression
1 2reuimp.c ⊢ b = c → φ ↔ θ
2 2reuimp.d ⊢ a = d → φ ↔ χ
3 2reuimp.a ⊢ a = d → θ ↔ τ
4 2reuimp.e ⊢ b = e → φ ↔ η
5 2reuimp.f ⊢ c = f → θ ↔ ψ
6 1 reu8 ⊢ ∃! b ∈ V φ ↔ ∃ b ∈ V φ ∧ ∀ c ∈ V θ → b = c
7 6 reubii ⊢ ∃! a ∈ V ∃! b ∈ V φ ↔ ∃! a ∈ V ∃ b ∈ V φ ∧ ∀ c ∈ V θ → b = c
8 3 imbi1d ⊢ a = d → θ → b = c ↔ τ → b = c
9 8 ralbidv ⊢ a = d → ∀ c ∈ V θ → b = c ↔ ∀ c ∈ V τ → b = c
10 2 9 anbi12d ⊢ a = d → φ ∧ ∀ c ∈ V θ → b = c ↔ χ ∧ ∀ c ∈ V τ → b = c
11 10 rexbidv ⊢ a = d → ∃ b ∈ V φ ∧ ∀ c ∈ V θ → b = c ↔ ∃ b ∈ V χ ∧ ∀ c ∈ V τ → b = c
12 11 reu8 ⊢ ∃! a ∈ V ∃ b ∈ V φ ∧ ∀ c ∈ V θ → b = c ↔ ∃ a ∈ V ∃ b ∈ V φ ∧ ∀ c ∈ V θ → b = c ∧ ∀ d ∈ V ∃ b ∈ V χ ∧ ∀ c ∈ V τ → b = c → a = d
13 r19.28v ⊢ ∃ b ∈ V φ ∧ ∀ c ∈ V θ → b = c ∧ ∀ d ∈ V ∃ b ∈ V χ ∧ ∀ c ∈ V τ → b = c → a = d → ∀ d ∈ V ∃ b ∈ V φ ∧ ∀ c ∈ V θ → b = c ∧ ∃ b ∈ V χ ∧ ∀ c ∈ V τ → b = c → a = d
14 equequ1 ⊢ b = e → b = c ↔ e = c
15 14 imbi2d ⊢ b = e → θ → b = c ↔ θ → e = c
16 15 ralbidv ⊢ b = e → ∀ c ∈ V θ → b = c ↔ ∀ c ∈ V θ → e = c
17 4 16 anbi12d ⊢ b = e → φ ∧ ∀ c ∈ V θ → b = c ↔ η ∧ ∀ c ∈ V θ → e = c
18 17 cbvrexvw ⊢ ∃ b ∈ V φ ∧ ∀ c ∈ V θ → b = c ↔ ∃ e ∈ V η ∧ ∀ c ∈ V θ → e = c
19 r19.23v ⊢ ∀ b ∈ V χ ∧ ∀ c ∈ V τ → b = c → a = d ↔ ∃ b ∈ V χ ∧ ∀ c ∈ V τ → b = c → a = d
20 r19.28v ⊢ ∃ e ∈ V η ∧ ∀ c ∈ V θ → e = c ∧ ∀ b ∈ V χ ∧ ∀ c ∈ V τ → b = c → a = d → ∀ b ∈ V ∃ e ∈ V η ∧ ∀ c ∈ V θ → e = c ∧ χ ∧ ∀ c ∈ V τ → b = c → a = d
21 ancom ⊢ ∃ e ∈ V η ∧ ∀ c ∈ V θ → e = c ∧ χ ∧ ∀ c ∈ V τ → b = c → a = d ↔ χ ∧ ∀ c ∈ V τ → b = c → a = d ∧ ∃ e ∈ V η ∧ ∀ c ∈ V θ → e = c
22 r19.42v ⊢ ∃ e ∈ V χ ∧ ∀ c ∈ V τ → b = c → a = d ∧ η ∧ ∀ c ∈ V θ → e = c ↔ χ ∧ ∀ c ∈ V τ → b = c → a = d ∧ ∃ e ∈ V η ∧ ∀ c ∈ V θ → e = c
23 21 22 bitr4i ⊢ ∃ e ∈ V η ∧ ∀ c ∈ V θ → e = c ∧ χ ∧ ∀ c ∈ V τ → b = c → a = d ↔ ∃ e ∈ V χ ∧ ∀ c ∈ V τ → b = c → a = d ∧ η ∧ ∀ c ∈ V θ → e = c
24 equequ2 ⊢ c = f → e = c ↔ e = f
25 5 24 imbi12d ⊢ c = f → θ → e = c ↔ ψ → e = f
26 25 cbvralvw ⊢ ∀ c ∈ V θ → e = c ↔ ∀ f ∈ V ψ → e = f
27 r19.28v ⊢ η ∧ χ ∧ ∀ c ∈ V τ → b = c → a = d ∧ ∀ f ∈ V ψ → e = f → ∀ f ∈ V η ∧ χ ∧ ∀ c ∈ V τ → b = c → a = d ∧ ψ → e = f
28 27 ex ⊢ η ∧ χ ∧ ∀ c ∈ V τ → b = c → a = d → ∀ f ∈ V ψ → e = f → ∀ f ∈ V η ∧ χ ∧ ∀ c ∈ V τ → b = c → a = d ∧ ψ → e = f
29 28 expcom ⊢ χ ∧ ∀ c ∈ V τ → b = c → a = d → η → ∀ f ∈ V ψ → e = f → ∀ f ∈ V η ∧ χ ∧ ∀ c ∈ V τ → b = c → a = d ∧ ψ → e = f
30 26 29 syl7bi ⊢ χ ∧ ∀ c ∈ V τ → b = c → a = d → η → ∀ c ∈ V θ → e = c → ∀ f ∈ V η ∧ χ ∧ ∀ c ∈ V τ → b = c → a = d ∧ ψ → e = f
31 30 imp32 ⊢ χ ∧ ∀ c ∈ V τ → b = c → a = d ∧ η ∧ ∀ c ∈ V θ → e = c → ∀ f ∈ V η ∧ χ ∧ ∀ c ∈ V τ → b = c → a = d ∧ ψ → e = f
32 31 reximi ⊢ ∃ e ∈ V χ ∧ ∀ c ∈ V τ → b = c → a = d ∧ η ∧ ∀ c ∈ V θ → e = c → ∃ e ∈ V ∀ f ∈ V η ∧ χ ∧ ∀ c ∈ V τ → b = c → a = d ∧ ψ → e = f
33 23 32 sylbi ⊢ ∃ e ∈ V η ∧ ∀ c ∈ V θ → e = c ∧ χ ∧ ∀ c ∈ V τ → b = c → a = d → ∃ e ∈ V ∀ f ∈ V η ∧ χ ∧ ∀ c ∈ V τ → b = c → a = d ∧ ψ → e = f
34 33 ralimi ⊢ ∀ b ∈ V ∃ e ∈ V η ∧ ∀ c ∈ V θ → e = c ∧ χ ∧ ∀ c ∈ V τ → b = c → a = d → ∀ b ∈ V ∃ e ∈ V ∀ f ∈ V η ∧ χ ∧ ∀ c ∈ V τ → b = c → a = d ∧ ψ → e = f
35 20 34 syl ⊢ ∃ e ∈ V η ∧ ∀ c ∈ V θ → e = c ∧ ∀ b ∈ V χ ∧ ∀ c ∈ V τ → b = c → a = d → ∀ b ∈ V ∃ e ∈ V ∀ f ∈ V η ∧ χ ∧ ∀ c ∈ V τ → b = c → a = d ∧ ψ → e = f
36 35 ex ⊢ ∃ e ∈ V η ∧ ∀ c ∈ V θ → e = c → ∀ b ∈ V χ ∧ ∀ c ∈ V τ → b = c → a = d → ∀ b ∈ V ∃ e ∈ V ∀ f ∈ V η ∧ χ ∧ ∀ c ∈ V τ → b = c → a = d ∧ ψ → e = f
37 19 36 syl5bir ⊢ ∃ e ∈ V η ∧ ∀ c ∈ V θ → e = c → ∃ b ∈ V χ ∧ ∀ c ∈ V τ → b = c → a = d → ∀ b ∈ V ∃ e ∈ V ∀ f ∈ V η ∧ χ ∧ ∀ c ∈ V τ → b = c → a = d ∧ ψ → e = f
38 18 37 sylbi ⊢ ∃ b ∈ V φ ∧ ∀ c ∈ V θ → b = c → ∃ b ∈ V χ ∧ ∀ c ∈ V τ → b = c → a = d → ∀ b ∈ V ∃ e ∈ V ∀ f ∈ V η ∧ χ ∧ ∀ c ∈ V τ → b = c → a = d ∧ ψ → e = f
39 38 imp ⊢ ∃ b ∈ V φ ∧ ∀ c ∈ V θ → b = c ∧ ∃ b ∈ V χ ∧ ∀ c ∈ V τ → b = c → a = d → ∀ b ∈ V ∃ e ∈ V ∀ f ∈ V η ∧ χ ∧ ∀ c ∈ V τ → b = c → a = d ∧ ψ → e = f
40 39 ralimi ⊢ ∀ d ∈ V ∃ b ∈ V φ ∧ ∀ c ∈ V θ → b = c ∧ ∃ b ∈ V χ ∧ ∀ c ∈ V τ → b = c → a = d → ∀ d ∈ V ∀ b ∈ V ∃ e ∈ V ∀ f ∈ V η ∧ χ ∧ ∀ c ∈ V τ → b = c → a = d ∧ ψ → e = f
41 13 40 syl ⊢ ∃ b ∈ V φ ∧ ∀ c ∈ V θ → b = c ∧ ∀ d ∈ V ∃ b ∈ V χ ∧ ∀ c ∈ V τ → b = c → a = d → ∀ d ∈ V ∀ b ∈ V ∃ e ∈ V ∀ f ∈ V η ∧ χ ∧ ∀ c ∈ V τ → b = c → a = d ∧ ψ → e = f
42 41 reximi ⊢ ∃ a ∈ V ∃ b ∈ V φ ∧ ∀ c ∈ V θ → b = c ∧ ∀ d ∈ V ∃ b ∈ V χ ∧ ∀ c ∈ V τ → b = c → a = d → ∃ a ∈ V ∀ d ∈ V ∀ b ∈ V ∃ e ∈ V ∀ f ∈ V η ∧ χ ∧ ∀ c ∈ V τ → b = c → a = d ∧ ψ → e = f
43 12 42 sylbi ⊢ ∃! a ∈ V ∃ b ∈ V φ ∧ ∀ c ∈ V θ → b = c → ∃ a ∈ V ∀ d ∈ V ∀ b ∈ V ∃ e ∈ V ∀ f ∈ V η ∧ χ ∧ ∀ c ∈ V τ → b = c → a = d ∧ ψ → e = f
44 7 43 sylbi ⊢ ∃! a ∈ V ∃! b ∈ V φ → ∃ a ∈ V ∀ d ∈ V ∀ b ∈ V ∃ e ∈ V ∀ f ∈ V η ∧ χ ∧ ∀ c ∈ V τ → b = c → a = d ∧ ψ → e = f