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 biimtrrid ⊢∃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