Theorem bj-cbveximt

Description: A lemma in closed form used to prove bj-cbvex in a weak axiomatization. (Contributed by BJ, 12-Mar-2023) Do not use 19.35 since only the direction of the biconditional used here holds in intuitionistic logic. (Proof modification is discouraged.)

	Ref	Expression
Assertion	bj-cbveximt	$$⊢\forall x\exists y\chi \to \left(\forall x\forall y\left(\chi \to \left(\phi \to \psi \right)\right)\to \left(\forall x\left(\phi \to \forall y\phi \right)\to \left(\left(\exists x\exists y\psi \to \exists y\psi \right)\to \left(\exists x\phi \to \exists y\psi \right)\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		bj-exalim	$$⊢\forall y\left(\chi \to \left(\phi \to \psi \right)\right)\to \left(\exists y\chi \to \left(\forall y\phi \to \exists y\psi \right)\right)$$
2	1	alimi	$$⊢\forall x\forall y\left(\chi \to \left(\phi \to \psi \right)\right)\to \forall x\left(\exists y\chi \to \left(\forall y\phi \to \exists y\psi \right)\right)$$
3		bj-alexim	$$⊢\forall x\left(\exists y\chi \to \left(\forall y\phi \to \exists y\psi \right)\right)\to \left(\forall x\exists y\chi \to \left(\exists x\forall y\phi \to \exists x\exists y\psi \right)\right)$$
4	2 3	syl	$$⊢\forall x\forall y\left(\chi \to \left(\phi \to \psi \right)\right)\to \left(\forall x\exists y\chi \to \left(\exists x\forall y\phi \to \exists x\exists y\psi \right)\right)$$
5		exim	$$⊢\forall x\left(\phi \to \forall y\phi \right)\to \left(\exists x\phi \to \exists x\forall y\phi \right)$$
6		imim2	$$⊢\left(\exists x\forall y\phi \to \exists x\exists y\psi \right)\to \left(\left(\exists x\phi \to \exists x\forall y\phi \right)\to \left(\exists x\phi \to \exists x\exists y\psi \right)\right)$$
7		imim1	$$⊢\left(\exists x\phi \to \exists x\exists y\psi \right)\to \left(\left(\exists x\exists y\psi \to \exists y\psi \right)\to \left(\exists x\phi \to \exists y\psi \right)\right)$$
8	5 6 7	syl56	$$⊢\left(\exists x\forall y\phi \to \exists x\exists y\psi \right)\to \left(\forall x\left(\phi \to \forall y\phi \right)\to \left(\left(\exists x\exists y\psi \to \exists y\psi \right)\to \left(\exists x\phi \to \exists y\psi \right)\right)\right)$$
9	4 8	syl6com	$$⊢\forall x\exists y\chi \to \left(\forall x\forall y\left(\chi \to \left(\phi \to \psi \right)\right)\to \left(\forall x\left(\phi \to \forall y\phi \right)\to \left(\left(\exists x\exists y\psi \to \exists y\psi \right)\to \left(\exists x\phi \to \exists y\psi \right)\right)\right)\right)$$