rossros

Description: Rings of sets are semirings of sets. (Contributed by Thierry Arnoux, 18-Jul-2020)

	Ref	Expression
Hypotheses	rossros.q	$⊢ Q = \{s \in 𝒫 𝒫 O \| (\emptyset \in s \land \forall x \in s \forall y \in s (x \cup y \in s \land x ∖ y \in s))\}$
	rossros.n	$⊢ N = \{s \in 𝒫 𝒫 O \| (\emptyset \in s \land \forall x \in s \forall y \in s (x \cap y \in s \land \exists z \in 𝒫 s (z \in Fin \land \underset{t \in z}{Disj} t \land x ∖ y = ⋃ z)))\}$
Assertion	rossros	$⊢ S \in Q \to S \in N$

Proof

Step	Hyp	Ref	Expression
1		rossros.q	$⊢ Q = \{s \in 𝒫 𝒫 O \| (\emptyset \in s \land \forall x \in s \forall y \in s (x \cup y \in s \land x ∖ y \in s))\}$
2		rossros.n	$⊢ N = \{s \in 𝒫 𝒫 O \| (\emptyset \in s \land \forall x \in s \forall y \in s (x \cap y \in s \land \exists z \in 𝒫 s (z \in Fin \land \underset{t \in z}{Disj} t \land x ∖ y = ⋃ z)))\}$
3	1	rossspw	$⊢ S \in Q \to S \subseteq 𝒫 O$
4		elpwg	$⊢ S \in Q \to (S \in 𝒫 𝒫 O \leftrightarrow S \subseteq 𝒫 O)$
5	3 4	mpbird	$⊢ S \in Q \to S \in 𝒫 𝒫 O$
6	1	0elros	$⊢ S \in Q \to \emptyset \in S$
7		uneq1	$⊢ u = x \to u \cup v = x \cup v$
8	7	eleq1d	$⊢ u = x \to (u \cup v \in s \leftrightarrow x \cup v \in s)$
9		difeq1	$⊢ u = x \to u ∖ v = x ∖ v$
10	9	eleq1d	$⊢ u = x \to (u ∖ v \in s \leftrightarrow x ∖ v \in s)$
11	8 10	anbi12d	$⊢ u = x \to ((u \cup v \in s \land u ∖ v \in s) \leftrightarrow (x \cup v \in s \land x ∖ v \in s))$
12		uneq2	$⊢ v = y \to x \cup v = x \cup y$
13	12	eleq1d	$⊢ v = y \to (x \cup v \in s \leftrightarrow x \cup y \in s)$
14		difeq2	$⊢ v = y \to x ∖ v = x ∖ y$
15	14	eleq1d	$⊢ v = y \to (x ∖ v \in s \leftrightarrow x ∖ y \in s)$
16	13 15	anbi12d	$⊢ v = y \to ((x \cup v \in s \land x ∖ v \in s) \leftrightarrow (x \cup y \in s \land x ∖ y \in s))$
17	11 16	cbvral2vw	$⊢ \forall u \in s \forall v \in s (u \cup v \in s \land u ∖ v \in s) \leftrightarrow \forall x \in s \forall y \in s (x \cup y \in s \land x ∖ y \in s)$
18	17	anbi2i	$⊢ (\emptyset \in s \land \forall u \in s \forall v \in s (u \cup v \in s \land u ∖ v \in s)) \leftrightarrow (\emptyset \in s \land \forall x \in s \forall y \in s (x \cup y \in s \land x ∖ y \in s))$
19	18	rabbii	$⊢ \{s \in 𝒫 𝒫 O \| (\emptyset \in s \land \forall u \in s \forall v \in s (u \cup v \in s \land u ∖ v \in s))\} = \{s \in 𝒫 𝒫 O \| (\emptyset \in s \land \forall x \in s \forall y \in s (x \cup y \in s \land x ∖ y \in s))\}$
20	1 19	eqtr4i	$⊢ Q = \{s \in 𝒫 𝒫 O \| (\emptyset \in s \land \forall u \in s \forall v \in s (u \cup v \in s \land u ∖ v \in s))\}$
21	20	inelros	$⊢ (S \in Q \land x \in S \land y \in S) \to x \cap y \in S$
22	21	3expb	$⊢ (S \in Q \land (x \in S \land y \in S)) \to x \cap y \in S$
23	20	difelros	$⊢ (S \in Q \land x \in S \land y \in S) \to x ∖ y \in S$
24	23	3expb	$⊢ (S \in Q \land (x \in S \land y \in S)) \to x ∖ y \in S$
25	24	snssd	$⊢ (S \in Q \land (x \in S \land y \in S)) \to \{x ∖ y\} \subseteq S$
26		snex	$⊢ \{x ∖ y\} \in V$
27	26	elpw	$⊢ \{x ∖ y\} \in 𝒫 S \leftrightarrow \{x ∖ y\} \subseteq S$
28	25 27	sylibr	$⊢ (S \in Q \land (x \in S \land y \in S)) \to \{x ∖ y\} \in 𝒫 S$
29		snfi	$⊢ \{x ∖ y\} \in Fin$
30	29	a1i	$⊢ (S \in Q \land (x \in S \land y \in S)) \to \{x ∖ y\} \in Fin$
31		disjxsn	$⊢ \underset{t \in \{x ∖ y\}}{Disj} t$
32	31	a1i	$⊢ (S \in Q \land (x \in S \land y \in S)) \to \underset{t \in \{x ∖ y\}}{Disj} t$
33		unisng	$⊢ x ∖ y \in S \to ⋃ \{x ∖ y\} = x ∖ y$
34	24 33	syl	$⊢ (S \in Q \land (x \in S \land y \in S)) \to ⋃ \{x ∖ y\} = x ∖ y$
35	34	eqcomd	$⊢ (S \in Q \land (x \in S \land y \in S)) \to x ∖ y = ⋃ \{x ∖ y\}$
36		eleq1	$⊢ z = \{x ∖ y\} \to (z \in Fin \leftrightarrow \{x ∖ y\} \in Fin)$
37		disjeq1	$⊢ z = \{x ∖ y\} \to (\underset{t \in z}{Disj} t \leftrightarrow \underset{t \in \{x ∖ y\}}{Disj} t)$
38		unieq	$⊢ z = \{x ∖ y\} \to ⋃ z = ⋃ \{x ∖ y\}$
39	38	eqeq2d	$⊢ z = \{x ∖ y\} \to (x ∖ y = ⋃ z \leftrightarrow x ∖ y = ⋃ \{x ∖ y\})$
40	36 37 39	3anbi123d	$⊢ z = \{x ∖ y\} \to ((z \in Fin \land \underset{t \in z}{Disj} t \land x ∖ y = ⋃ z) \leftrightarrow (\{x ∖ y\} \in Fin \land \underset{t \in \{x ∖ y\}}{Disj} t \land x ∖ y = ⋃ \{x ∖ y\}))$
41	40	rspcev	$⊢ (\{x ∖ y\} \in 𝒫 S \land (\{x ∖ y\} \in Fin \land \underset{t \in \{x ∖ y\}}{Disj} t \land x ∖ y = ⋃ \{x ∖ y\})) \to \exists z \in 𝒫 S (z \in Fin \land \underset{t \in z}{Disj} t \land x ∖ y = ⋃ z)$
42	28 30 32 35 41	syl13anc	$⊢ (S \in Q \land (x \in S \land y \in S)) \to \exists z \in 𝒫 S (z \in Fin \land \underset{t \in z}{Disj} t \land x ∖ y = ⋃ z)$
43	22 42	jca	$⊢ (S \in Q \land (x \in S \land y \in S)) \to (x \cap y \in S \land \exists z \in 𝒫 S (z \in Fin \land \underset{t \in z}{Disj} t \land x ∖ y = ⋃ z))$
44	43	ralrimivva	$⊢ S \in Q \to \forall x \in S \forall y \in S (x \cap y \in S \land \exists z \in 𝒫 S (z \in Fin \land \underset{t \in z}{Disj} t \land x ∖ y = ⋃ z))$
45	5 6 44	3jca	$⊢ S \in Q \to (S \in 𝒫 𝒫 O \land \emptyset \in S \land \forall x \in S \forall y \in S (x \cap y \in S \land \exists z \in 𝒫 S (z \in Fin \land \underset{t \in z}{Disj} t \land x ∖ y = ⋃ z)))$
46	2	issros	$⊢ S \in N \leftrightarrow (S \in 𝒫 𝒫 O \land \emptyset \in S \land \forall x \in S \forall y \in S (x \cap y \in S \land \exists z \in 𝒫 S (z \in Fin \land \underset{t \in z}{Disj} t \land x ∖ y = ⋃ z)))$
47	45 46	sylibr	$⊢ S \in Q \to S \in N$

Metamath Proof Explorer

Theorem rossros

Proof