unielss

Description: Two ways to say the union of a class is an element of a subclass. (Contributed by RP, 29-Jan-2025)

		Ref	Expression
	Assertion	unielss	$⊢ A \subseteq B \to (⋃ B \in A \leftrightarrow \exists x \in A \forall y \in B y \subseteq x)$

Proof

Step	Hyp	Ref	Expression
1		uniel	$⊢ ⋃ B \in A \leftrightarrow \exists x \in A \forall z (z \in x \leftrightarrow \exists y \in B z \in y)$
2		df-ss	$⊢ y \subseteq x \leftrightarrow \forall z (z \in y \to z \in x)$
3	2	ralbii	$⊢ \forall y \in B y \subseteq x \leftrightarrow \forall y \in B \forall z (z \in y \to z \in x)$
4		df-ral	$⊢ \forall y \in B \forall z (z \in y \to z \in x) \leftrightarrow \forall y (y \in B \to \forall z (z \in y \to z \in x))$
5		19.21v	$⊢ \forall z (y \in B \to (z \in y \to z \in x)) \leftrightarrow (y \in B \to \forall z (z \in y \to z \in x))$
6	5	albii	$⊢ \forall y \forall z (y \in B \to (z \in y \to z \in x)) \leftrightarrow \forall y (y \in B \to \forall z (z \in y \to z \in x))$
7		alcom	$⊢ \forall y \forall z (y \in B \to (z \in y \to z \in x)) \leftrightarrow \forall z \forall y (y \in B \to (z \in y \to z \in x))$
8	4 6 7	3bitr2i	$⊢ \forall y \in B \forall z (z \in y \to z \in x) \leftrightarrow \forall z \forall y (y \in B \to (z \in y \to z \in x))$
9	3 8	bitri	$⊢ \forall y \in B y \subseteq x \leftrightarrow \forall z \forall y (y \in B \to (z \in y \to z \in x))$
10		ssel2	$⊢ (A \subseteq B \land x \in A) \to x \in B$
11		pm2.27	$⊢ z \in x \to ((z \in x \to z \in x) \to z \in x)$
12		elequ2	$⊢ y = x \to (z \in y \leftrightarrow z \in x)$
13	12	imbi1d	$⊢ y = x \to ((z \in y \to z \in x) \leftrightarrow (z \in x \to z \in x))$
14	13 12	imbi12d	$⊢ y = x \to (((z \in y \to z \in x) \to z \in y) \leftrightarrow ((z \in x \to z \in x) \to z \in x))$
15	14	rspcev	$⊢ (x \in B \land ((z \in x \to z \in x) \to z \in x)) \to \exists y \in B ((z \in y \to z \in x) \to z \in y)$
16	10 11 15	syl2an	$⊢ ((A \subseteq B \land x \in A) \land z \in x) \to \exists y \in B ((z \in y \to z \in x) \to z \in y)$
17		r19.35	$⊢ \exists y \in B ((z \in y \to z \in x) \to z \in y) \leftrightarrow (\forall y \in B (z \in y \to z \in x) \to \exists y \in B z \in y)$
18		df-ral	$⊢ \forall y \in B (z \in y \to z \in x) \leftrightarrow \forall y (y \in B \to (z \in y \to z \in x))$
19	18	imbi1i	$⊢ (\forall y \in B (z \in y \to z \in x) \to \exists y \in B z \in y) \leftrightarrow (\forall y (y \in B \to (z \in y \to z \in x)) \to \exists y \in B z \in y)$
20	17 19	bitri	$⊢ \exists y \in B ((z \in y \to z \in x) \to z \in y) \leftrightarrow (\forall y (y \in B \to (z \in y \to z \in x)) \to \exists y \in B z \in y)$
21	16 20	sylib	$⊢ ((A \subseteq B \land x \in A) \land z \in x) \to (\forall y (y \in B \to (z \in y \to z \in x)) \to \exists y \in B z \in y)$
22	21	impancom	$⊢ ((A \subseteq B \land x \in A) \land \forall y (y \in B \to (z \in y \to z \in x))) \to (z \in x \to \exists y \in B z \in y)$
23		nfv	$⊢ Ⅎ y (A \subseteq B \land x \in A)$
24		nfa1	$⊢ Ⅎ y \forall y (y \in B \to (z \in y \to z \in x))$
25	23 24	nfan	$⊢ Ⅎ y ((A \subseteq B \land x \in A) \land \forall y (y \in B \to (z \in y \to z \in x)))$
26		nfv	$⊢ Ⅎ y z \in x$
27		sp	$⊢ \forall y (y \in B \to (z \in y \to z \in x)) \to (y \in B \to (z \in y \to z \in x))$
28	27	adantl	$⊢ ((A \subseteq B \land x \in A) \land \forall y (y \in B \to (z \in y \to z \in x))) \to (y \in B \to (z \in y \to z \in x))$
29	25 26 28	rexlimd	$⊢ ((A \subseteq B \land x \in A) \land \forall y (y \in B \to (z \in y \to z \in x))) \to (\exists y \in B z \in y \to z \in x)$
30	22 29	impbid	$⊢ ((A \subseteq B \land x \in A) \land \forall y (y \in B \to (z \in y \to z \in x))) \to (z \in x \leftrightarrow \exists y \in B z \in y)$
31		rspe	$⊢ (y \in B \land z \in y) \to \exists y \in B z \in y$
32	31	ex	$⊢ y \in B \to (z \in y \to \exists y \in B z \in y)$
33	32	ax-gen	$⊢ \forall y (y \in B \to (z \in y \to \exists y \in B z \in y))$
34		nfre1	$⊢ Ⅎ y \exists y \in B z \in y$
35	26 34	nfbi	$⊢ Ⅎ y (z \in x \leftrightarrow \exists y \in B z \in y)$
36		imbi2	$⊢ (z \in x \leftrightarrow \exists y \in B z \in y) \to ((z \in y \to z \in x) \leftrightarrow (z \in y \to \exists y \in B z \in y))$
37	36	imbi2d	$⊢ (z \in x \leftrightarrow \exists y \in B z \in y) \to ((y \in B \to (z \in y \to z \in x)) \leftrightarrow (y \in B \to (z \in y \to \exists y \in B z \in y)))$
38	35 37	albid	$⊢ (z \in x \leftrightarrow \exists y \in B z \in y) \to (\forall y (y \in B \to (z \in y \to z \in x)) \leftrightarrow \forall y (y \in B \to (z \in y \to \exists y \in B z \in y)))$
39	38	adantl	$⊢ ((A \subseteq B \land x \in A) \land (z \in x \leftrightarrow \exists y \in B z \in y)) \to (\forall y (y \in B \to (z \in y \to z \in x)) \leftrightarrow \forall y (y \in B \to (z \in y \to \exists y \in B z \in y)))$
40	33 39	mpbiri	$⊢ ((A \subseteq B \land x \in A) \land (z \in x \leftrightarrow \exists y \in B z \in y)) \to \forall y (y \in B \to (z \in y \to z \in x))$
41	30 40	impbida	$⊢ (A \subseteq B \land x \in A) \to (\forall y (y \in B \to (z \in y \to z \in x)) \leftrightarrow (z \in x \leftrightarrow \exists y \in B z \in y))$
42	41	albidv	$⊢ (A \subseteq B \land x \in A) \to (\forall z \forall y (y \in B \to (z \in y \to z \in x)) \leftrightarrow \forall z (z \in x \leftrightarrow \exists y \in B z \in y))$
43	9 42	bitrid	$⊢ (A \subseteq B \land x \in A) \to (\forall y \in B y \subseteq x \leftrightarrow \forall z (z \in x \leftrightarrow \exists y \in B z \in y))$
44	43	rexbidva	$⊢ A \subseteq B \to (\exists x \in A \forall y \in B y \subseteq x \leftrightarrow \exists x \in A \forall z (z \in x \leftrightarrow \exists y \in B z \in y))$
45	1 44	bitr4id	$⊢ A \subseteq B \to (⋃ B \in A \leftrightarrow \exists x \in A \forall y \in B y \subseteq x)$

Metamath Proof Explorer

Theorem unielss

Proof