dfiun2g

Description: Alternate definition of indexed union when B is a set. Definition 15(a) of Suppes p. 44. (Contributed by NM, 23-Mar-2006) (Proof shortened by Andrew Salmon, 25-Jul-2011) (Proof shortened by Rohan Ridenour, 11-Aug-2023) Avoid ax-10 , ax-12 . (Revised by SN, 11-Dec-2024)

		Ref	Expression
	Assertion	dfiun2g	\|- ( A. x e. A B e. C -> U_ x e. A B = U. { y \| E. x e. A y = B } )

Proof

Step	Hyp	Ref	Expression
1		df-iun	\|- U_ x e. A B = { z \| E. x e. A z e. B }
2		elisset	\|- ( B e. C -> E. z z = B )
3		eleq2	\|- ( z = B -> ( w e. z <-> w e. B ) )
4	3	pm5.32ri	\|- ( ( w e. z /\ z = B ) <-> ( w e. B /\ z = B ) )
5	4	simplbi2	\|- ( w e. B -> ( z = B -> ( w e. z /\ z = B ) ) )
6	5	eximdv	\|- ( w e. B -> ( E. z z = B -> E. z ( w e. z /\ z = B ) ) )
7	2 6	syl5com	\|- ( B e. C -> ( w e. B -> E. z ( w e. z /\ z = B ) ) )
8	7	ralimi	\|- ( A. x e. A B e. C -> A. x e. A ( w e. B -> E. z ( w e. z /\ z = B ) ) )
9		rexim	\|- ( A. x e. A ( w e. B -> E. z ( w e. z /\ z = B ) ) -> ( E. x e. A w e. B -> E. x e. A E. z ( w e. z /\ z = B ) ) )
10	8 9	syl	\|- ( A. x e. A B e. C -> ( E. x e. A w e. B -> E. x e. A E. z ( w e. z /\ z = B ) ) )
11		rexcom4	\|- ( E. x e. A E. z ( w e. z /\ z = B ) <-> E. z E. x e. A ( w e. z /\ z = B ) )
12		r19.42v	\|- ( E. x e. A ( w e. z /\ z = B ) <-> ( w e. z /\ E. x e. A z = B ) )
13	12	exbii	\|- ( E. z E. x e. A ( w e. z /\ z = B ) <-> E. z ( w e. z /\ E. x e. A z = B ) )
14	11 13	bitri	\|- ( E. x e. A E. z ( w e. z /\ z = B ) <-> E. z ( w e. z /\ E. x e. A z = B ) )
15	10 14	imbitrdi	\|- ( A. x e. A B e. C -> ( E. x e. A w e. B -> E. z ( w e. z /\ E. x e. A z = B ) ) )
16	3	biimpac	\|- ( ( w e. z /\ z = B ) -> w e. B )
17	16	reximi	\|- ( E. x e. A ( w e. z /\ z = B ) -> E. x e. A w e. B )
18	12 17	sylbir	\|- ( ( w e. z /\ E. x e. A z = B ) -> E. x e. A w e. B )
19	18	exlimiv	\|- ( E. z ( w e. z /\ E. x e. A z = B ) -> E. x e. A w e. B )
20	15 19	impbid1	\|- ( A. x e. A B e. C -> ( E. x e. A w e. B <-> E. z ( w e. z /\ E. x e. A z = B ) ) )
21		vex	\|- w e. _V
22		eleq1w	\|- ( z = w -> ( z e. B <-> w e. B ) )
23	22	rexbidv	\|- ( z = w -> ( E. x e. A z e. B <-> E. x e. A w e. B ) )
24	21 23	elab	\|- ( w e. { z \| E. x e. A z e. B } <-> E. x e. A w e. B )
25		eluni	\|- ( w e. U. { y \| E. x e. A y = B } <-> E. z ( w e. z /\ z e. { y \| E. x e. A y = B } ) )
26		vex	\|- z e. _V
27		eqeq1	\|- ( y = z -> ( y = B <-> z = B ) )
28	27	rexbidv	\|- ( y = z -> ( E. x e. A y = B <-> E. x e. A z = B ) )
29	26 28	elab	\|- ( z e. { y \| E. x e. A y = B } <-> E. x e. A z = B )
30	29	anbi2i	\|- ( ( w e. z /\ z e. { y \| E. x e. A y = B } ) <-> ( w e. z /\ E. x e. A z = B ) )
31	30	exbii	\|- ( E. z ( w e. z /\ z e. { y \| E. x e. A y = B } ) <-> E. z ( w e. z /\ E. x e. A z = B ) )
32	25 31	bitri	\|- ( w e. U. { y \| E. x e. A y = B } <-> E. z ( w e. z /\ E. x e. A z = B ) )
33	20 24 32	3bitr4g	\|- ( A. x e. A B e. C -> ( w e. { z \| E. x e. A z e. B } <-> w e. U. { y \| E. x e. A y = B } ) )
34	33	eqrdv	\|- ( A. x e. A B e. C -> { z \| E. x e. A z e. B } = U. { y \| E. x e. A y = B } )
35	1 34	eqtrid	\|- ( A. x e. A B e. C -> U_ x e. A B = U. { y \| E. x e. A y = B } )

Metamath Proof Explorer

Theorem dfiun2g

Proof