Theorem or2expropbilem1

Description: Lemma 1 for or2expropbi and ich2exprop . (Contributed by AV, 16-Jul-2023)

	Ref	Expression
Assertion	or2expropbilem1	$$⊢\left(A\in X\wedge B\in X\right)\to \left(\left(A=a\wedge B=b\right)\to \left(\phi \to \exists x\exists y\left(⟨A,B⟩=⟨x,y⟩\wedge \underset{\dot{}}{[}y/b\underset{\dot{}}{]}\underset{\dot{}}{[}x/a\underset{\dot{}}{]}\phi \right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		vex	$$⊢a\in \mathrm{V}$$
2		vex	$$⊢b\in \mathrm{V}$$
3	1 2	pm3.2i	$$⊢\left(a\in \mathrm{V}\wedge b\in \mathrm{V}\right)$$
4	3	a1i	$$⊢\left(A\in X\wedge B\in X\right)\to \left(a\in \mathrm{V}\wedge b\in \mathrm{V}\right)$$
5	4	anim1ci	$$⊢\left(\left(A\in X\wedge B\in X\right)\wedge \phi \right)\to \left(\phi \wedge \left(a\in \mathrm{V}\wedge b\in \mathrm{V}\right)\right)$$
6	5	adantr	$$⊢\left(\left(\left(A\in X\wedge B\in X\right)\wedge \phi \right)\wedge \left(A=a\wedge B=b\right)\right)\to \left(\phi \wedge \left(a\in \mathrm{V}\wedge b\in \mathrm{V}\right)\right)$$
7		sbcid	$$⊢\underset{\dot{}}{[}b/b\underset{\dot{}}{]}\underset{\dot{}}{[}a/a\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}a/a\underset{\dot{}}{]}\phi$$
8		sbcid	$$⊢\underset{\dot{}}{[}a/a\underset{\dot{}}{]}\phi \leftrightarrow \phi$$
9	7 8	sylbbr	$$⊢\phi \to \underset{\dot{}}{[}b/b\underset{\dot{}}{]}\underset{\dot{}}{[}a/a\underset{\dot{}}{]}\phi$$
10	9	adantl	$$⊢\left(\left(A\in X\wedge B\in X\right)\wedge \phi \right)\to \underset{\dot{}}{[}b/b\underset{\dot{}}{]}\underset{\dot{}}{[}a/a\underset{\dot{}}{]}\phi$$
11		opeq12	$$⊢\left(A=a\wedge B=b\right)\to ⟨A,B⟩=⟨a,b⟩$$
12	10 11	anim12ci	$$⊢\left(\left(\left(A\in X\wedge B\in X\right)\wedge \phi \right)\wedge \left(A=a\wedge B=b\right)\right)\to \left(⟨A,B⟩=⟨a,b⟩\wedge \underset{\dot{}}{[}b/b\underset{\dot{}}{]}\underset{\dot{}}{[}a/a\underset{\dot{}}{]}\phi \right)$$
13		nfv	$$⊢Ⅎx\left(⟨A,B⟩=⟨a,b⟩\wedge \underset{\dot{}}{[}b/b\underset{\dot{}}{]}\underset{\dot{}}{[}a/a\underset{\dot{}}{]}\phi \right)$$
14		nfv	$$⊢Ⅎy\left(⟨A,B⟩=⟨a,b⟩\wedge \underset{\dot{}}{[}b/b\underset{\dot{}}{]}\underset{\dot{}}{[}a/a\underset{\dot{}}{]}\phi \right)$$
15		opeq12	$$⊢\left(x=a\wedge y=b\right)\to ⟨x,y⟩=⟨a,b⟩$$
16	15	eqeq2d	$$⊢\left(x=a\wedge y=b\right)\to \left(⟨A,B⟩=⟨x,y⟩\leftrightarrow ⟨A,B⟩=⟨a,b⟩\right)$$
17		dfsbcq	$$⊢y=b\to \left(\underset{\dot{}}{[}y/b\underset{\dot{}}{]}\underset{\dot{}}{[}x/a\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}b/b\underset{\dot{}}{]}\underset{\dot{}}{[}x/a\underset{\dot{}}{]}\phi \right)$$
18		dfsbcq	$$⊢x=a\to \left(\underset{\dot{}}{[}x/a\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}a/a\underset{\dot{}}{]}\phi \right)$$
19	18	sbcbidv	$$⊢x=a\to \left(\underset{\dot{}}{[}b/b\underset{\dot{}}{]}\underset{\dot{}}{[}x/a\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}b/b\underset{\dot{}}{]}\underset{\dot{}}{[}a/a\underset{\dot{}}{]}\phi \right)$$
20	17 19	sylan9bbr	$$⊢\left(x=a\wedge y=b\right)\to \left(\underset{\dot{}}{[}y/b\underset{\dot{}}{]}\underset{\dot{}}{[}x/a\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}b/b\underset{\dot{}}{]}\underset{\dot{}}{[}a/a\underset{\dot{}}{]}\phi \right)$$
21	16 20	anbi12d	$$⊢\left(x=a\wedge y=b\right)\to \left(\left(⟨A,B⟩=⟨x,y⟩\wedge \underset{\dot{}}{[}y/b\underset{\dot{}}{]}\underset{\dot{}}{[}x/a\underset{\dot{}}{]}\phi \right)\leftrightarrow \left(⟨A,B⟩=⟨a,b⟩\wedge \underset{\dot{}}{[}b/b\underset{\dot{}}{]}\underset{\dot{}}{[}a/a\underset{\dot{}}{]}\phi \right)\right)$$
22	21	adantl	$$⊢\left(\phi \wedge \left(x=a\wedge y=b\right)\right)\to \left(\left(⟨A,B⟩=⟨x,y⟩\wedge \underset{\dot{}}{[}y/b\underset{\dot{}}{]}\underset{\dot{}}{[}x/a\underset{\dot{}}{]}\phi \right)\leftrightarrow \left(⟨A,B⟩=⟨a,b⟩\wedge \underset{\dot{}}{[}b/b\underset{\dot{}}{]}\underset{\dot{}}{[}a/a\underset{\dot{}}{]}\phi \right)\right)$$
23	13 14 22	spc2ed	$$⊢\left(\phi \wedge \left(a\in \mathrm{V}\wedge b\in \mathrm{V}\right)\right)\to \left(\left(⟨A,B⟩=⟨a,b⟩\wedge \underset{\dot{}}{[}b/b\underset{\dot{}}{]}\underset{\dot{}}{[}a/a\underset{\dot{}}{]}\phi \right)\to \exists x\exists y\left(⟨A,B⟩=⟨x,y⟩\wedge \underset{\dot{}}{[}y/b\underset{\dot{}}{]}\underset{\dot{}}{[}x/a\underset{\dot{}}{]}\phi \right)\right)$$
24	6 12 23	sylc	$$⊢\left(\left(\left(A\in X\wedge B\in X\right)\wedge \phi \right)\wedge \left(A=a\wedge B=b\right)\right)\to \exists x\exists y\left(⟨A,B⟩=⟨x,y⟩\wedge \underset{\dot{}}{[}y/b\underset{\dot{}}{]}\underset{\dot{}}{[}x/a\underset{\dot{}}{]}\phi \right)$$
25	24	exp31	$$⊢\left(A\in X\wedge B\in X\right)\to \left(\phi \to \left(\left(A=a\wedge B=b\right)\to \exists x\exists y\left(⟨A,B⟩=⟨x,y⟩\wedge \underset{\dot{}}{[}y/b\underset{\dot{}}{]}\underset{\dot{}}{[}x/a\underset{\dot{}}{]}\phi \right)\right)\right)$$
26	25	com23	$$⊢\left(A\in X\wedge B\in X\right)\to \left(\left(A=a\wedge B=b\right)\to \left(\phi \to \exists x\exists y\left(⟨A,B⟩=⟨x,y⟩\wedge \underset{\dot{}}{[}y/b\underset{\dot{}}{]}\underset{\dot{}}{[}x/a\underset{\dot{}}{]}\phi \right)\right)\right)$$