Theorem ich2exprop

Description: If the setvar variables are interchangeable in a wff, there is an ordered pair fulfilling the wff iff there is an unordered pair fulfilling the wff. (Contributed by AV, 16-Jul-2023)

	Ref	Expression
Assertion	ich2exprop	$$⊢\left(A\in X\wedge B\in X\wedge \left[a\rightleftarrows b\right]\phi \right)\to \left(\exists a\exists b\left(\left\{A,B\right\}=\left\{a,b\right\}\wedge \phi \right)\leftrightarrow \exists a\exists b\left(⟨A,B⟩=⟨a,b⟩\wedge \phi \right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		nfv	$$⊢ℲaA\in X$$
2		nfv	$$⊢ℲaB\in X$$
3		nfich1	$$⊢Ⅎa\left[a\rightleftarrows b\right]\phi$$
4	1 2 3	nf3an	$$⊢Ⅎa\left(A\in X\wedge B\in X\wedge \left[a\rightleftarrows b\right]\phi \right)$$
5		nfv	$$⊢Ⅎa⟨A,B⟩=⟨x,y⟩$$
6		nfcv	$$⊢\underset{\_}{Ⅎ}ay$$
7		nfsbc1v	$$⊢Ⅎa\underset{\dot{}}{[}x/a\underset{\dot{}}{]}\phi$$
8	6 7	nfsbcw	$$⊢Ⅎa\underset{\dot{}}{[}y/b\underset{\dot{}}{]}\underset{\dot{}}{[}x/a\underset{\dot{}}{]}\phi$$
9	5 8	nfan	$$⊢Ⅎa\left(⟨A,B⟩=⟨x,y⟩\wedge \underset{\dot{}}{[}y/b\underset{\dot{}}{]}\underset{\dot{}}{[}x/a\underset{\dot{}}{]}\phi \right)$$
10	9	nfex	$$⊢Ⅎa\exists y\left(⟨A,B⟩=⟨x,y⟩\wedge \underset{\dot{}}{[}y/b\underset{\dot{}}{]}\underset{\dot{}}{[}x/a\underset{\dot{}}{]}\phi \right)$$
11	10	nfex	$$⊢Ⅎa\exists x\exists y\left(⟨A,B⟩=⟨x,y⟩\wedge \underset{\dot{}}{[}y/b\underset{\dot{}}{]}\underset{\dot{}}{[}x/a\underset{\dot{}}{]}\phi \right)$$
12		nfv	$$⊢ℲbA\in X$$
13		nfv	$$⊢ℲbB\in X$$
14		nfich2	$$⊢Ⅎb\left[a\rightleftarrows b\right]\phi$$
15	12 13 14	nf3an	$$⊢Ⅎb\left(A\in X\wedge B\in X\wedge \left[a\rightleftarrows b\right]\phi \right)$$
16		nfv	$$⊢Ⅎb⟨A,B⟩=⟨x,y⟩$$
17		nfsbc1v	$$⊢Ⅎb\underset{\dot{}}{[}y/b\underset{\dot{}}{]}\underset{\dot{}}{[}x/a\underset{\dot{}}{]}\phi$$
18	16 17	nfan	$$⊢Ⅎb\left(⟨A,B⟩=⟨x,y⟩\wedge \underset{\dot{}}{[}y/b\underset{\dot{}}{]}\underset{\dot{}}{[}x/a\underset{\dot{}}{]}\phi \right)$$
19	18	nfex	$$⊢Ⅎb\exists y\left(⟨A,B⟩=⟨x,y⟩\wedge \underset{\dot{}}{[}y/b\underset{\dot{}}{]}\underset{\dot{}}{[}x/a\underset{\dot{}}{]}\phi \right)$$
20	19	nfex	$$⊢Ⅎb\exists x\exists y\left(⟨A,B⟩=⟨x,y⟩\wedge \underset{\dot{}}{[}y/b\underset{\dot{}}{]}\underset{\dot{}}{[}x/a\underset{\dot{}}{]}\phi \right)$$
21		vex	$$⊢a\in \mathrm{V}$$
22		vex	$$⊢b\in \mathrm{V}$$
23		preq12bg	$$⊢\left(\left(A\in X\wedge B\in X\right)\wedge \left(a\in \mathrm{V}\wedge b\in \mathrm{V}\right)\right)\to \left(\left\{A,B\right\}=\left\{a,b\right\}\leftrightarrow \left(\left(A=a\wedge B=b\right)\vee \left(A=b\wedge B=a\right)\right)\right)$$
24	21 22 23	mpanr12	$$⊢\left(A\in X\wedge B\in X\right)\to \left(\left\{A,B\right\}=\left\{a,b\right\}\leftrightarrow \left(\left(A=a\wedge B=b\right)\vee \left(A=b\wedge B=a\right)\right)\right)$$
25	24	3adant3	$$⊢\left(A\in X\wedge B\in X\wedge \left[a\rightleftarrows b\right]\phi \right)\to \left(\left\{A,B\right\}=\left\{a,b\right\}\leftrightarrow \left(\left(A=a\wedge B=b\right)\vee \left(A=b\wedge B=a\right)\right)\right)$$
26		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)$$
27	26	3adant3	$$⊢\left(A\in X\wedge B\in X\wedge \left[a\rightleftarrows b\right]\phi \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)$$
28		ichcom	$$⊢\left[a\rightleftarrows b\right]\phi \leftrightarrow \left[b\rightleftarrows a\right]\phi$$
29	28	biimpi	$$⊢\left[a\rightleftarrows b\right]\phi \to \left[b\rightleftarrows a\right]\phi$$
30	29	3ad2ant3	$$⊢\left(A\in X\wedge B\in X\wedge \left[a\rightleftarrows b\right]\phi \right)\to \left[b\rightleftarrows a\right]\phi$$
31	30	adantr	$$⊢\left(\left(A\in X\wedge B\in X\wedge \left[a\rightleftarrows b\right]\phi \right)\wedge \phi \right)\to \left[b\rightleftarrows a\right]\phi$$
32	22 21	pm3.2i	$$⊢\left(b\in \mathrm{V}\wedge a\in \mathrm{V}\right)$$
33	32	a1i	$$⊢\left(A=b\wedge B=a\right)\to \left(b\in \mathrm{V}\wedge a\in \mathrm{V}\right)$$
34	31 33	anim12i	$$⊢\left(\left(\left(A\in X\wedge B\in X\wedge \left[a\rightleftarrows b\right]\phi \right)\wedge \phi \right)\wedge \left(A=b\wedge B=a\right)\right)\to \left(\left[b\rightleftarrows a\right]\phi \wedge \left(b\in \mathrm{V}\wedge a\in \mathrm{V}\right)\right)$$
35		simpr	$$⊢\left(\left(A\in X\wedge B\in X\wedge \left[a\rightleftarrows b\right]\phi \right)\wedge \phi \right)\to \phi$$
36		opeq12	$$⊢\left(A=b\wedge B=a\right)\to ⟨A,B⟩=⟨b,a⟩$$
37	35 36	anim12ci	$$⊢\left(\left(\left(A\in X\wedge B\in X\wedge \left[a\rightleftarrows b\right]\phi \right)\wedge \phi \right)\wedge \left(A=b\wedge B=a\right)\right)\to \left(⟨A,B⟩=⟨b,a⟩\wedge \phi \right)$$
38		nfv	$$⊢Ⅎx\left(⟨A,B⟩=⟨b,a⟩\wedge \phi \right)$$
39		nfv	$$⊢Ⅎy\left(⟨A,B⟩=⟨b,a⟩\wedge \phi \right)$$
40		opeq12	$$⊢\left(x=b\wedge y=a\right)\to ⟨x,y⟩=⟨b,a⟩$$
41	40	eqeq2d	$$⊢\left(x=b\wedge y=a\right)\to \left(⟨A,B⟩=⟨x,y⟩\leftrightarrow ⟨A,B⟩=⟨b,a⟩\right)$$
42	41	adantl	$$⊢\left(\left[b\rightleftarrows a\right]\phi \wedge \left(x=b\wedge y=a\right)\right)\to \left(⟨A,B⟩=⟨x,y⟩\leftrightarrow ⟨A,B⟩=⟨b,a⟩\right)$$
43		dfsbcq	$$⊢y=a\to \left(\underset{\dot{}}{[}y/b\underset{\dot{}}{]}\underset{\dot{}}{[}x/a\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}a/b\underset{\dot{}}{]}\underset{\dot{}}{[}x/a\underset{\dot{}}{]}\phi \right)$$
44	43	adantl	$$⊢\left(x=b\wedge y=a\right)\to \left(\underset{\dot{}}{[}y/b\underset{\dot{}}{]}\underset{\dot{}}{[}x/a\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}a/b\underset{\dot{}}{]}\underset{\dot{}}{[}x/a\underset{\dot{}}{]}\phi \right)$$
45	44	adantl	$$⊢\left(\left[b\rightleftarrows a\right]\phi \wedge \left(x=b\wedge y=a\right)\right)\to \left(\underset{\dot{}}{[}y/b\underset{\dot{}}{]}\underset{\dot{}}{[}x/a\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}a/b\underset{\dot{}}{]}\underset{\dot{}}{[}x/a\underset{\dot{}}{]}\phi \right)$$
46		sbceq1a	$$⊢x=b\to \left(\underset{\dot{}}{[}a/b\underset{\dot{}}{]}\underset{\dot{}}{[}x/a\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}b/x\underset{\dot{}}{]}\underset{\dot{}}{[}a/b\underset{\dot{}}{]}\underset{\dot{}}{[}x/a\underset{\dot{}}{]}\phi \right)$$
47	46	adantr	$$⊢\left(x=b\wedge y=a\right)\to \left(\underset{\dot{}}{[}a/b\underset{\dot{}}{]}\underset{\dot{}}{[}x/a\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}b/x\underset{\dot{}}{]}\underset{\dot{}}{[}a/b\underset{\dot{}}{]}\underset{\dot{}}{[}x/a\underset{\dot{}}{]}\phi \right)$$
48		df-ich	$$⊢\left[b\rightleftarrows a\right]\phi \leftrightarrow \forall b\forall a\left(\left[b/x\right]\left[a/b\right]\left[x/a\right]\phi \leftrightarrow \phi \right)$$
49		sbsbc	$$⊢\left[b/x\right]\left[a/b\right]\left[x/a\right]\phi \leftrightarrow \underset{\dot{}}{[}b/x\underset{\dot{}}{]}\left[a/b\right]\left[x/a\right]\phi$$
50		sbsbc	$$⊢\left[a/b\right]\left[x/a\right]\phi \leftrightarrow \underset{\dot{}}{[}a/b\underset{\dot{}}{]}\left[x/a\right]\phi$$
51		sbsbc	$$⊢\left[x/a\right]\phi \leftrightarrow \underset{\dot{}}{[}x/a\underset{\dot{}}{]}\phi$$
52	51	sbcbii	$$⊢\underset{\dot{}}{[}a/b\underset{\dot{}}{]}\left[x/a\right]\phi \leftrightarrow \underset{\dot{}}{[}a/b\underset{\dot{}}{]}\underset{\dot{}}{[}x/a\underset{\dot{}}{]}\phi$$
53	50 52	bitri	$$⊢\left[a/b\right]\left[x/a\right]\phi \leftrightarrow \underset{\dot{}}{[}a/b\underset{\dot{}}{]}\underset{\dot{}}{[}x/a\underset{\dot{}}{]}\phi$$
54	53	sbcbii	$$⊢\underset{\dot{}}{[}b/x\underset{\dot{}}{]}\left[a/b\right]\left[x/a\right]\phi \leftrightarrow \underset{\dot{}}{[}b/x\underset{\dot{}}{]}\underset{\dot{}}{[}a/b\underset{\dot{}}{]}\underset{\dot{}}{[}x/a\underset{\dot{}}{]}\phi$$
55	49 54	bitri	$$⊢\left[b/x\right]\left[a/b\right]\left[x/a\right]\phi \leftrightarrow \underset{\dot{}}{[}b/x\underset{\dot{}}{]}\underset{\dot{}}{[}a/b\underset{\dot{}}{]}\underset{\dot{}}{[}x/a\underset{\dot{}}{]}\phi$$
56		2sp	$$⊢\forall b\forall a\left(\left[b/x\right]\left[a/b\right]\left[x/a\right]\phi \leftrightarrow \phi \right)\to \left(\left[b/x\right]\left[a/b\right]\left[x/a\right]\phi \leftrightarrow \phi \right)$$
57	55 56	bitr3id	$$⊢\forall b\forall a\left(\left[b/x\right]\left[a/b\right]\left[x/a\right]\phi \leftrightarrow \phi \right)\to \left(\underset{\dot{}}{[}b/x\underset{\dot{}}{]}\underset{\dot{}}{[}a/b\underset{\dot{}}{]}\underset{\dot{}}{[}x/a\underset{\dot{}}{]}\phi \leftrightarrow \phi \right)$$
58	48 57	sylbi	$$⊢\left[b\rightleftarrows a\right]\phi \to \left(\underset{\dot{}}{[}b/x\underset{\dot{}}{]}\underset{\dot{}}{[}a/b\underset{\dot{}}{]}\underset{\dot{}}{[}x/a\underset{\dot{}}{]}\phi \leftrightarrow \phi \right)$$
59	47 58	sylan9bbr	$$⊢\left(\left[b\rightleftarrows a\right]\phi \wedge \left(x=b\wedge y=a\right)\right)\to \left(\underset{\dot{}}{[}a/b\underset{\dot{}}{]}\underset{\dot{}}{[}x/a\underset{\dot{}}{]}\phi \leftrightarrow \phi \right)$$
60	45 59	bitrd	$$⊢\left(\left[b\rightleftarrows a\right]\phi \wedge \left(x=b\wedge y=a\right)\right)\to \left(\underset{\dot{}}{[}y/b\underset{\dot{}}{]}\underset{\dot{}}{[}x/a\underset{\dot{}}{]}\phi \leftrightarrow \phi \right)$$
61	42 60	anbi12d	$$⊢\left(\left[b\rightleftarrows a\right]\phi \wedge \left(x=b\wedge y=a\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⟩=⟨b,a⟩\wedge \phi \right)\right)$$
62	38 39 61	spc2ed	$$⊢\left(\left[b\rightleftarrows a\right]\phi \wedge \left(b\in \mathrm{V}\wedge a\in \mathrm{V}\right)\right)\to \left(\left(⟨A,B⟩=⟨b,a⟩\wedge \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)$$
63	34 37 62	sylc	$$⊢\left(\left(\left(A\in X\wedge B\in X\wedge \left[a\rightleftarrows b\right]\phi \right)\wedge \phi \right)\wedge \left(A=b\wedge B=a\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)$$
64	63	exp31	$$⊢\left(A\in X\wedge B\in X\wedge \left[a\rightleftarrows b\right]\phi \right)\to \left(\phi \to \left(\left(A=b\wedge B=a\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)$$
65	64	com23	$$⊢\left(A\in X\wedge B\in X\wedge \left[a\rightleftarrows b\right]\phi \right)\to \left(\left(A=b\wedge B=a\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)$$
66	27 65	jaod	$$⊢\left(A\in X\wedge B\in X\wedge \left[a\rightleftarrows b\right]\phi \right)\to \left(\left(\left(A=a\wedge B=b\right)\vee \left(A=b\wedge B=a\right)\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)$$
67	25 66	sylbid	$$⊢\left(A\in X\wedge B\in X\wedge \left[a\rightleftarrows b\right]\phi \right)\to \left(\left\{A,B\right\}=\left\{a,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)$$
68	67	impd	$$⊢\left(A\in X\wedge B\in X\wedge \left[a\rightleftarrows b\right]\phi \right)\to \left(\left(\left\{A,B\right\}=\left\{a,b\right\}\wedge \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)$$
69	15 20 68	exlimd	$$⊢\left(A\in X\wedge B\in X\wedge \left[a\rightleftarrows b\right]\phi \right)\to \left(\exists b\left(\left\{A,B\right\}=\left\{a,b\right\}\wedge \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)$$
70	4 11 69	exlimd	$$⊢\left(A\in X\wedge B\in X\wedge \left[a\rightleftarrows b\right]\phi \right)\to \left(\exists a\exists b\left(\left\{A,B\right\}=\left\{a,b\right\}\wedge \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)$$
71		or2expropbilem2	$$⊢\exists a\exists b\left(⟨A,B⟩=⟨a,b⟩\wedge \phi \right)\leftrightarrow \exists x\exists y\left(⟨A,B⟩=⟨x,y⟩\wedge \underset{\dot{}}{[}y/b\underset{\dot{}}{]}\underset{\dot{}}{[}x/a\underset{\dot{}}{]}\phi \right)$$
72	70 71	syl6ibr	$$⊢\left(A\in X\wedge B\in X\wedge \left[a\rightleftarrows b\right]\phi \right)\to \left(\exists a\exists b\left(\left\{A,B\right\}=\left\{a,b\right\}\wedge \phi \right)\to \exists a\exists b\left(⟨A,B⟩=⟨a,b⟩\wedge \phi \right)\right)$$
73		oppr	$$⊢\left(A\in X\wedge B\in X\right)\to \left(⟨A,B⟩=⟨a,b⟩\to \left\{A,B\right\}=\left\{a,b\right\}\right)$$
74	73	anim1d	$$⊢\left(A\in X\wedge B\in X\right)\to \left(\left(⟨A,B⟩=⟨a,b⟩\wedge \phi \right)\to \left(\left\{A,B\right\}=\left\{a,b\right\}\wedge \phi \right)\right)$$
75	74	2eximdv	$$⊢\left(A\in X\wedge B\in X\right)\to \left(\exists a\exists b\left(⟨A,B⟩=⟨a,b⟩\wedge \phi \right)\to \exists a\exists b\left(\left\{A,B\right\}=\left\{a,b\right\}\wedge \phi \right)\right)$$
76	75	3adant3	$$⊢\left(A\in X\wedge B\in X\wedge \left[a\rightleftarrows b\right]\phi \right)\to \left(\exists a\exists b\left(⟨A,B⟩=⟨a,b⟩\wedge \phi \right)\to \exists a\exists b\left(\left\{A,B\right\}=\left\{a,b\right\}\wedge \phi \right)\right)$$
77	72 76	impbid	$$⊢\left(A\in X\wedge B\in X\wedge \left[a\rightleftarrows b\right]\phi \right)\to \left(\exists a\exists b\left(\left\{A,B\right\}=\left\{a,b\right\}\wedge \phi \right)\leftrightarrow \exists a\exists b\left(⟨A,B⟩=⟨a,b⟩\wedge \phi \right)\right)$$