Theorem iunopeqop

Description: Implication of an ordered pair being equal to an indexed union of singletons of ordered pairs. (Contributed by AV, 20-Sep-2020) (Avoid depending on this detail.)

	Ref	Expression
Hypotheses	iunopeqop.b	$$⊢B\in \mathrm{V}$$
	iunopeqop.c	$$⊢C\in \mathrm{V}$$
	iunopeqop.d	$$⊢D\in \mathrm{V}$$
Assertion	iunopeqop	$$⊢A\ne \varnothing \to \left(\bigcup _{x\in A}\left\{⟨x,B⟩\right\}=⟨C,D⟩\to \exists zA=\left\{z\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		iunopeqop.b	$$⊢B\in \mathrm{V}$$
2		iunopeqop.c	$$⊢C\in \mathrm{V}$$
3		iunopeqop.d	$$⊢D\in \mathrm{V}$$
4		n0snor2el	$$⊢A\ne \varnothing \to \left(\exists x\in A\exists y\in Ax\ne y\vee \exists zA=\left\{z\right\}\right)$$
5		nfiu1	$$⊢\underset{\_}{Ⅎ}x\bigcup _{x\in A}\left\{⟨x,B⟩\right\}$$
6	5	nfeq1	$$⊢Ⅎx\bigcup _{x\in A}\left\{⟨x,B⟩\right\}=⟨C,D⟩$$
7		nfv	$$⊢Ⅎx\exists zA=\left\{z\right\}$$
8	6 7	nfim	$$⊢Ⅎx\left(\bigcup _{x\in A}\left\{⟨x,B⟩\right\}=⟨C,D⟩\to \exists zA=\left\{z\right\}\right)$$
9		ssiun2	$$⊢x\in A\to \left\{⟨x,B⟩\right\}\subseteq \bigcup _{x\in A}\left\{⟨x,B⟩\right\}$$
10		nfcv	$$⊢\underset{\_}{Ⅎ}xy$$
11		nfcsb1v	$$⊢\underset{\_}{Ⅎ}x⦋y/x⦌B$$
12	10 11	nfop	$$⊢\underset{\_}{Ⅎ}x⟨y,⦋y/x⦌B⟩$$
13	12	nfsn	$$⊢\underset{\_}{Ⅎ}x\left\{⟨y,⦋y/x⦌B⟩\right\}$$
14	13 5	nfss	$$⊢Ⅎx\left\{⟨y,⦋y/x⦌B⟩\right\}\subseteq \bigcup _{x\in A}\left\{⟨x,B⟩\right\}$$
15		id	$$⊢x=y\to x=y$$
16		csbeq1a	$$⊢x=y\to B=⦋y/x⦌B$$
17	15 16	opeq12d	$$⊢x=y\to ⟨x,B⟩=⟨y,⦋y/x⦌B⟩$$
18	17	sneqd	$$⊢x=y\to \left\{⟨x,B⟩\right\}=\left\{⟨y,⦋y/x⦌B⟩\right\}$$
19	18	sseq1d	$$⊢x=y\to \left(\left\{⟨x,B⟩\right\}\subseteq \bigcup _{x\in A}\left\{⟨x,B⟩\right\}\leftrightarrow \left\{⟨y,⦋y/x⦌B⟩\right\}\subseteq \bigcup _{x\in A}\left\{⟨x,B⟩\right\}\right)$$
20	10 14 19 9	vtoclgaf	$$⊢y\in A\to \left\{⟨y,⦋y/x⦌B⟩\right\}\subseteq \bigcup _{x\in A}\left\{⟨x,B⟩\right\}$$
21	9 20	anim12i	$$⊢\left(x\in A\wedge y\in A\right)\to \left(\left\{⟨x,B⟩\right\}\subseteq \bigcup _{x\in A}\left\{⟨x,B⟩\right\}\wedge \left\{⟨y,⦋y/x⦌B⟩\right\}\subseteq \bigcup _{x\in A}\left\{⟨x,B⟩\right\}\right)$$
22		unss	$$⊢\left(\left\{⟨x,B⟩\right\}\subseteq \bigcup _{x\in A}\left\{⟨x,B⟩\right\}\wedge \left\{⟨y,⦋y/x⦌B⟩\right\}\subseteq \bigcup _{x\in A}\left\{⟨x,B⟩\right\}\right)\leftrightarrow \left\{⟨x,B⟩\right\}\cup \left\{⟨y,⦋y/x⦌B⟩\right\}\subseteq \bigcup _{x\in A}\left\{⟨x,B⟩\right\}$$
23		sseq2	$$⊢\bigcup _{x\in A}\left\{⟨x,B⟩\right\}=⟨C,D⟩\to \left(\left\{⟨x,B⟩\right\}\cup \left\{⟨y,⦋y/x⦌B⟩\right\}\subseteq \bigcup _{x\in A}\left\{⟨x,B⟩\right\}\leftrightarrow \left\{⟨x,B⟩\right\}\cup \left\{⟨y,⦋y/x⦌B⟩\right\}\subseteq ⟨C,D⟩\right)$$
24		df-pr	$$⊢\left\{⟨x,B⟩,⟨y,⦋y/x⦌B⟩\right\}=\left\{⟨x,B⟩\right\}\cup \left\{⟨y,⦋y/x⦌B⟩\right\}$$
25	24	eqcomi	$$⊢\left\{⟨x,B⟩\right\}\cup \left\{⟨y,⦋y/x⦌B⟩\right\}=\left\{⟨x,B⟩,⟨y,⦋y/x⦌B⟩\right\}$$
26	25	sseq1i	$$⊢\left\{⟨x,B⟩\right\}\cup \left\{⟨y,⦋y/x⦌B⟩\right\}\subseteq ⟨C,D⟩\leftrightarrow \left\{⟨x,B⟩,⟨y,⦋y/x⦌B⟩\right\}\subseteq ⟨C,D⟩$$
27		vex	$$⊢x\in \mathrm{V}$$
28		vex	$$⊢y\in \mathrm{V}$$
29	1	csbex	$$⊢⦋y/x⦌B\in \mathrm{V}$$
30	27 1 28 29 2 3	propssopi	$$⊢\left\{⟨x,B⟩,⟨y,⦋y/x⦌B⟩\right\}\subseteq ⟨C,D⟩\to x=y$$
31		eqneqall	$$⊢x=y\to \left(x\ne y\to \left(\left(x\in A\wedge y\in A\right)\to \exists zA=\left\{z\right\}\right)\right)$$
32	30 31	syl	$$⊢\left\{⟨x,B⟩,⟨y,⦋y/x⦌B⟩\right\}\subseteq ⟨C,D⟩\to \left(x\ne y\to \left(\left(x\in A\wedge y\in A\right)\to \exists zA=\left\{z\right\}\right)\right)$$
33	26 32	sylbi	$$⊢\left\{⟨x,B⟩\right\}\cup \left\{⟨y,⦋y/x⦌B⟩\right\}\subseteq ⟨C,D⟩\to \left(x\ne y\to \left(\left(x\in A\wedge y\in A\right)\to \exists zA=\left\{z\right\}\right)\right)$$
34	23 33	syl6bi	$$⊢\bigcup _{x\in A}\left\{⟨x,B⟩\right\}=⟨C,D⟩\to \left(\left\{⟨x,B⟩\right\}\cup \left\{⟨y,⦋y/x⦌B⟩\right\}\subseteq \bigcup _{x\in A}\left\{⟨x,B⟩\right\}\to \left(x\ne y\to \left(\left(x\in A\wedge y\in A\right)\to \exists zA=\left\{z\right\}\right)\right)\right)$$
35	34	com14	$$⊢\left(x\in A\wedge y\in A\right)\to \left(\left\{⟨x,B⟩\right\}\cup \left\{⟨y,⦋y/x⦌B⟩\right\}\subseteq \bigcup _{x\in A}\left\{⟨x,B⟩\right\}\to \left(x\ne y\to \left(\bigcup _{x\in A}\left\{⟨x,B⟩\right\}=⟨C,D⟩\to \exists zA=\left\{z\right\}\right)\right)\right)$$
36	22 35	syl5bi	$$⊢\left(x\in A\wedge y\in A\right)\to \left(\left(\left\{⟨x,B⟩\right\}\subseteq \bigcup _{x\in A}\left\{⟨x,B⟩\right\}\wedge \left\{⟨y,⦋y/x⦌B⟩\right\}\subseteq \bigcup _{x\in A}\left\{⟨x,B⟩\right\}\right)\to \left(x\ne y\to \left(\bigcup _{x\in A}\left\{⟨x,B⟩\right\}=⟨C,D⟩\to \exists zA=\left\{z\right\}\right)\right)\right)$$
37	21 36	mpd	$$⊢\left(x\in A\wedge y\in A\right)\to \left(x\ne y\to \left(\bigcup _{x\in A}\left\{⟨x,B⟩\right\}=⟨C,D⟩\to \exists zA=\left\{z\right\}\right)\right)$$
38	37	rexlimdva	$$⊢x\in A\to \left(\exists y\in Ax\ne y\to \left(\bigcup _{x\in A}\left\{⟨x,B⟩\right\}=⟨C,D⟩\to \exists zA=\left\{z\right\}\right)\right)$$
39	8 38	rexlimi	$$⊢\exists x\in A\exists y\in Ax\ne y\to \left(\bigcup _{x\in A}\left\{⟨x,B⟩\right\}=⟨C,D⟩\to \exists zA=\left\{z\right\}\right)$$
40		ax-1	$$⊢\exists zA=\left\{z\right\}\to \left(\bigcup _{x\in A}\left\{⟨x,B⟩\right\}=⟨C,D⟩\to \exists zA=\left\{z\right\}\right)$$
41	39 40	jaoi	$$⊢\left(\exists x\in A\exists y\in Ax\ne y\vee \exists zA=\left\{z\right\}\right)\to \left(\bigcup _{x\in A}\left\{⟨x,B⟩\right\}=⟨C,D⟩\to \exists zA=\left\{z\right\}\right)$$
42	4 41	syl	$$⊢A\ne \varnothing \to \left(\bigcup _{x\in A}\left\{⟨x,B⟩\right\}=⟨C,D⟩\to \exists zA=\left\{z\right\}\right)$$