Theorem funsndifnop

Description: A singleton of an ordered pair is not an ordered pair if the components are different. (Contributed by AV, 23-Sep-2020) (Avoid depending on this detail.)

	Ref	Expression
Hypotheses	funsndifnop.a	$$⊢A\in \mathrm{V}$$
	funsndifnop.b	$$⊢B\in \mathrm{V}$$
	funsndifnop.g	$$⊢G=\left\{⟨A,B⟩\right\}$$
Assertion	funsndifnop	$$⊢A\ne B\to \neg G\in \left(\mathrm{V}\times \mathrm{V}\right)$$

Proof

Step	Hyp	Ref	Expression
1		funsndifnop.a	$$⊢A\in \mathrm{V}$$
2		funsndifnop.b	$$⊢B\in \mathrm{V}$$
3		funsndifnop.g	$$⊢G=\left\{⟨A,B⟩\right\}$$
4		elvv	$$⊢G\in \left(\mathrm{V}\times \mathrm{V}\right)\leftrightarrow \exists x\exists yG=⟨x,y⟩$$
5	1 2	funsn	$$⊢\mathrm{Fun}\left\{⟨A,B⟩\right\}$$
6		funeq	$$⊢G=\left\{⟨A,B⟩\right\}\to \left(\mathrm{Fun}G\leftrightarrow \mathrm{Fun}\left\{⟨A,B⟩\right\}\right)$$
7	5 6	mpbiri	$$⊢G=\left\{⟨A,B⟩\right\}\to \mathrm{Fun}G$$
8	3 7	ax-mp	$$⊢\mathrm{Fun}G$$
9		funeq	$$⊢G=⟨x,y⟩\to \left(\mathrm{Fun}G\leftrightarrow \mathrm{Fun}⟨x,y⟩\right)$$
10		vex	$$⊢x\in \mathrm{V}$$
11		vex	$$⊢y\in \mathrm{V}$$
12	10 11	funop	$$⊢\mathrm{Fun}⟨x,y⟩\leftrightarrow \exists a\left(x=\left\{a\right\}\wedge ⟨x,y⟩=\left\{⟨a,a⟩\right\}\right)$$
13	9 12	bitrdi	$$⊢G=⟨x,y⟩\to \left(\mathrm{Fun}G\leftrightarrow \exists a\left(x=\left\{a\right\}\wedge ⟨x,y⟩=\left\{⟨a,a⟩\right\}\right)\right)$$
14		eqeq2	$$⊢⟨x,y⟩=\left\{⟨a,a⟩\right\}\to \left(G=⟨x,y⟩\leftrightarrow G=\left\{⟨a,a⟩\right\}\right)$$
15		eqeq1	$$⊢G=\left\{⟨A,B⟩\right\}\to \left(G=\left\{⟨a,a⟩\right\}\leftrightarrow \left\{⟨A,B⟩\right\}=\left\{⟨a,a⟩\right\}\right)$$
16		opex	$$⊢⟨A,B⟩\in \mathrm{V}$$
17	16	sneqr	$$⊢\left\{⟨A,B⟩\right\}=\left\{⟨a,a⟩\right\}\to ⟨A,B⟩=⟨a,a⟩$$
18	1 2	opth	$$⊢⟨A,B⟩=⟨a,a⟩\leftrightarrow \left(A=a\wedge B=a\right)$$
19		eqtr3	$$⊢\left(A=a\wedge B=a\right)\to A=B$$
20	19	a1d	$$⊢\left(A=a\wedge B=a\right)\to \left(x=\left\{a\right\}\to A=B\right)$$
21	18 20	sylbi	$$⊢⟨A,B⟩=⟨a,a⟩\to \left(x=\left\{a\right\}\to A=B\right)$$
22	17 21	syl	$$⊢\left\{⟨A,B⟩\right\}=\left\{⟨a,a⟩\right\}\to \left(x=\left\{a\right\}\to A=B\right)$$
23	15 22	syl6bi	$$⊢G=\left\{⟨A,B⟩\right\}\to \left(G=\left\{⟨a,a⟩\right\}\to \left(x=\left\{a\right\}\to A=B\right)\right)$$
24	3 23	ax-mp	$$⊢G=\left\{⟨a,a⟩\right\}\to \left(x=\left\{a\right\}\to A=B\right)$$
25	14 24	syl6bi	$$⊢⟨x,y⟩=\left\{⟨a,a⟩\right\}\to \left(G=⟨x,y⟩\to \left(x=\left\{a\right\}\to A=B\right)\right)$$
26	25	com23	$$⊢⟨x,y⟩=\left\{⟨a,a⟩\right\}\to \left(x=\left\{a\right\}\to \left(G=⟨x,y⟩\to A=B\right)\right)$$
27	26	impcom	$$⊢\left(x=\left\{a\right\}\wedge ⟨x,y⟩=\left\{⟨a,a⟩\right\}\right)\to \left(G=⟨x,y⟩\to A=B\right)$$
28	27	exlimiv	$$⊢\exists a\left(x=\left\{a\right\}\wedge ⟨x,y⟩=\left\{⟨a,a⟩\right\}\right)\to \left(G=⟨x,y⟩\to A=B\right)$$
29	28	com12	$$⊢G=⟨x,y⟩\to \left(\exists a\left(x=\left\{a\right\}\wedge ⟨x,y⟩=\left\{⟨a,a⟩\right\}\right)\to A=B\right)$$
30	13 29	sylbid	$$⊢G=⟨x,y⟩\to \left(\mathrm{Fun}G\to A=B\right)$$
31	8 30	mpi	$$⊢G=⟨x,y⟩\to A=B$$
32	31	exlimivv	$$⊢\exists x\exists yG=⟨x,y⟩\to A=B$$
33	4 32	sylbi	$$⊢G\in \left(\mathrm{V}\times \mathrm{V}\right)\to A=B$$
34	33	necon3ai	$$⊢A\ne B\to \neg G\in \left(\mathrm{V}\times \mathrm{V}\right)$$