Theorem rossros

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

	Ref	Expression
Hypotheses	rossros.q	⊢ 𝑄 = { 𝑠 ∈ 𝒫 𝒫 𝑂 ∣ ( ∅ ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑠 ( ( 𝑥 ∪ 𝑦 ) ∈ 𝑠 ∧ ( 𝑥 ∖ 𝑦 ) ∈ 𝑠 ) ) }
	rossros.n	⊢ 𝑁 = { 𝑠 ∈ 𝒫 𝒫 𝑂 ∣ ( ∅ ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑠 ( ( 𝑥 ∩ 𝑦 ) ∈ 𝑠 ∧ ∃ 𝑧 ∈ 𝒫 𝑠 ( 𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ ( 𝑥 ∖ 𝑦 ) = ∪ 𝑧 ) ) ) }
Assertion	rossros	⊢ ( 𝑆 ∈ 𝑄 → 𝑆 ∈ 𝑁 )

Proof

Step	Hyp	Ref	Expression
1		rossros.q	⊢ 𝑄 = { 𝑠 ∈ 𝒫 𝒫 𝑂 ∣ ( ∅ ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑠 ( ( 𝑥 ∪ 𝑦 ) ∈ 𝑠 ∧ ( 𝑥 ∖ 𝑦 ) ∈ 𝑠 ) ) }
2		rossros.n	⊢ 𝑁 = { 𝑠 ∈ 𝒫 𝒫 𝑂 ∣ ( ∅ ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑠 ( ( 𝑥 ∩ 𝑦 ) ∈ 𝑠 ∧ ∃ 𝑧 ∈ 𝒫 𝑠 ( 𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ ( 𝑥 ∖ 𝑦 ) = ∪ 𝑧 ) ) ) }
3	1	rossspw	⊢ ( 𝑆 ∈ 𝑄 → 𝑆 ⊆ 𝒫 𝑂 )
4		elpwg	⊢ ( 𝑆 ∈ 𝑄 → ( 𝑆 ∈ 𝒫 𝒫 𝑂 ↔ 𝑆 ⊆ 𝒫 𝑂 ) )
5	3 4	mpbird	⊢ ( 𝑆 ∈ 𝑄 → 𝑆 ∈ 𝒫 𝒫 𝑂 )
6	1	0elros	⊢ ( 𝑆 ∈ 𝑄 → ∅ ∈ 𝑆 )
7		uneq1	⊢ ( 𝑢 = 𝑥 → ( 𝑢 ∪ 𝑣 ) = ( 𝑥 ∪ 𝑣 ) )
8	7	eleq1d	⊢ ( 𝑢 = 𝑥 → ( ( 𝑢 ∪ 𝑣 ) ∈ 𝑠 ↔ ( 𝑥 ∪ 𝑣 ) ∈ 𝑠 ) )
9		difeq1	⊢ ( 𝑢 = 𝑥 → ( 𝑢 ∖ 𝑣 ) = ( 𝑥 ∖ 𝑣 ) )
10	9	eleq1d	⊢ ( 𝑢 = 𝑥 → ( ( 𝑢 ∖ 𝑣 ) ∈ 𝑠 ↔ ( 𝑥 ∖ 𝑣 ) ∈ 𝑠 ) )
11	8 10	anbi12d	⊢ ( 𝑢 = 𝑥 → ( ( ( 𝑢 ∪ 𝑣 ) ∈ 𝑠 ∧ ( 𝑢 ∖ 𝑣 ) ∈ 𝑠 ) ↔ ( ( 𝑥 ∪ 𝑣 ) ∈ 𝑠 ∧ ( 𝑥 ∖ 𝑣 ) ∈ 𝑠 ) ) )
12		uneq2	⊢ ( 𝑣 = 𝑦 → ( 𝑥 ∪ 𝑣 ) = ( 𝑥 ∪ 𝑦 ) )
13	12	eleq1d	⊢ ( 𝑣 = 𝑦 → ( ( 𝑥 ∪ 𝑣 ) ∈ 𝑠 ↔ ( 𝑥 ∪ 𝑦 ) ∈ 𝑠 ) )
14		difeq2	⊢ ( 𝑣 = 𝑦 → ( 𝑥 ∖ 𝑣 ) = ( 𝑥 ∖ 𝑦 ) )
15	14	eleq1d	⊢ ( 𝑣 = 𝑦 → ( ( 𝑥 ∖ 𝑣 ) ∈ 𝑠 ↔ ( 𝑥 ∖ 𝑦 ) ∈ 𝑠 ) )
16	13 15	anbi12d	⊢ ( 𝑣 = 𝑦 → ( ( ( 𝑥 ∪ 𝑣 ) ∈ 𝑠 ∧ ( 𝑥 ∖ 𝑣 ) ∈ 𝑠 ) ↔ ( ( 𝑥 ∪ 𝑦 ) ∈ 𝑠 ∧ ( 𝑥 ∖ 𝑦 ) ∈ 𝑠 ) ) )
17	11 16	cbvral2vw	⊢ ( ∀ 𝑢 ∈ 𝑠 ∀ 𝑣 ∈ 𝑠 ( ( 𝑢 ∪ 𝑣 ) ∈ 𝑠 ∧ ( 𝑢 ∖ 𝑣 ) ∈ 𝑠 ) ↔ ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑠 ( ( 𝑥 ∪ 𝑦 ) ∈ 𝑠 ∧ ( 𝑥 ∖ 𝑦 ) ∈ 𝑠 ) )
18	17	anbi2i	⊢ ( ( ∅ ∈ 𝑠 ∧ ∀ 𝑢 ∈ 𝑠 ∀ 𝑣 ∈ 𝑠 ( ( 𝑢 ∪ 𝑣 ) ∈ 𝑠 ∧ ( 𝑢 ∖ 𝑣 ) ∈ 𝑠 ) ) ↔ ( ∅ ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑠 ( ( 𝑥 ∪ 𝑦 ) ∈ 𝑠 ∧ ( 𝑥 ∖ 𝑦 ) ∈ 𝑠 ) ) )
19	18	rabbii	⊢ { 𝑠 ∈ 𝒫 𝒫 𝑂 ∣ ( ∅ ∈ 𝑠 ∧ ∀ 𝑢 ∈ 𝑠 ∀ 𝑣 ∈ 𝑠 ( ( 𝑢 ∪ 𝑣 ) ∈ 𝑠 ∧ ( 𝑢 ∖ 𝑣 ) ∈ 𝑠 ) ) } = { 𝑠 ∈ 𝒫 𝒫 𝑂 ∣ ( ∅ ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑠 ( ( 𝑥 ∪ 𝑦 ) ∈ 𝑠 ∧ ( 𝑥 ∖ 𝑦 ) ∈ 𝑠 ) ) }
20	1 19	eqtr4i	⊢ 𝑄 = { 𝑠 ∈ 𝒫 𝒫 𝑂 ∣ ( ∅ ∈ 𝑠 ∧ ∀ 𝑢 ∈ 𝑠 ∀ 𝑣 ∈ 𝑠 ( ( 𝑢 ∪ 𝑣 ) ∈ 𝑠 ∧ ( 𝑢 ∖ 𝑣 ) ∈ 𝑠 ) ) }
21	20	inelros	⊢ ( ( 𝑆 ∈ 𝑄 ∧ 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) → ( 𝑥 ∩ 𝑦 ) ∈ 𝑆 )
22	21	3expb	⊢ ( ( 𝑆 ∈ 𝑄 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 ∩ 𝑦 ) ∈ 𝑆 )
23	20	difelros	⊢ ( ( 𝑆 ∈ 𝑄 ∧ 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) → ( 𝑥 ∖ 𝑦 ) ∈ 𝑆 )
24	23	3expb	⊢ ( ( 𝑆 ∈ 𝑄 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 ∖ 𝑦 ) ∈ 𝑆 )
25	24	snssd	⊢ ( ( 𝑆 ∈ 𝑄 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → { ( 𝑥 ∖ 𝑦 ) } ⊆ 𝑆 )
26		snex	⊢ { ( 𝑥 ∖ 𝑦 ) } ∈ V
27	26	elpw	⊢ ( { ( 𝑥 ∖ 𝑦 ) } ∈ 𝒫 𝑆 ↔ { ( 𝑥 ∖ 𝑦 ) } ⊆ 𝑆 )
28	25 27	sylibr	⊢ ( ( 𝑆 ∈ 𝑄 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → { ( 𝑥 ∖ 𝑦 ) } ∈ 𝒫 𝑆 )
29		snfi	⊢ { ( 𝑥 ∖ 𝑦 ) } ∈ Fin
30	29	a1i	⊢ ( ( 𝑆 ∈ 𝑄 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → { ( 𝑥 ∖ 𝑦 ) } ∈ Fin )
31		disjxsn	⊢ Disj 𝑡 ∈ { ( 𝑥 ∖ 𝑦 ) } 𝑡
32	31	a1i	⊢ ( ( 𝑆 ∈ 𝑄 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → Disj 𝑡 ∈ { ( 𝑥 ∖ 𝑦 ) } 𝑡 )
33		unisng	⊢ ( ( 𝑥 ∖ 𝑦 ) ∈ 𝑆 → ∪ { ( 𝑥 ∖ 𝑦 ) } = ( 𝑥 ∖ 𝑦 ) )
34	24 33	syl	⊢ ( ( 𝑆 ∈ 𝑄 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ∪ { ( 𝑥 ∖ 𝑦 ) } = ( 𝑥 ∖ 𝑦 ) )
35	34	eqcomd	⊢ ( ( 𝑆 ∈ 𝑄 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 ∖ 𝑦 ) = ∪ { ( 𝑥 ∖ 𝑦 ) } )
36		eleq1	⊢ ( 𝑧 = { ( 𝑥 ∖ 𝑦 ) } → ( 𝑧 ∈ Fin ↔ { ( 𝑥 ∖ 𝑦 ) } ∈ Fin ) )
37		disjeq1	⊢ ( 𝑧 = { ( 𝑥 ∖ 𝑦 ) } → ( Disj 𝑡 ∈ 𝑧 𝑡 ↔ Disj 𝑡 ∈ { ( 𝑥 ∖ 𝑦 ) } 𝑡 ) )
38		unieq	⊢ ( 𝑧 = { ( 𝑥 ∖ 𝑦 ) } → ∪ 𝑧 = ∪ { ( 𝑥 ∖ 𝑦 ) } )
39	38	eqeq2d	⊢ ( 𝑧 = { ( 𝑥 ∖ 𝑦 ) } → ( ( 𝑥 ∖ 𝑦 ) = ∪ 𝑧 ↔ ( 𝑥 ∖ 𝑦 ) = ∪ { ( 𝑥 ∖ 𝑦 ) } ) )
40	36 37 39	3anbi123d	⊢ ( 𝑧 = { ( 𝑥 ∖ 𝑦 ) } → ( ( 𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ ( 𝑥 ∖ 𝑦 ) = ∪ 𝑧 ) ↔ ( { ( 𝑥 ∖ 𝑦 ) } ∈ Fin ∧ Disj 𝑡 ∈ { ( 𝑥 ∖ 𝑦 ) } 𝑡 ∧ ( 𝑥 ∖ 𝑦 ) = ∪ { ( 𝑥 ∖ 𝑦 ) } ) ) )
41	40	rspcev	⊢ ( ( { ( 𝑥 ∖ 𝑦 ) } ∈ 𝒫 𝑆 ∧ ( { ( 𝑥 ∖ 𝑦 ) } ∈ Fin ∧ Disj 𝑡 ∈ { ( 𝑥 ∖ 𝑦 ) } 𝑡 ∧ ( 𝑥 ∖ 𝑦 ) = ∪ { ( 𝑥 ∖ 𝑦 ) } ) ) → ∃ 𝑧 ∈ 𝒫 𝑆 ( 𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ ( 𝑥 ∖ 𝑦 ) = ∪ 𝑧 ) )
42	28 30 32 35 41	syl13anc	⊢ ( ( 𝑆 ∈ 𝑄 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ∃ 𝑧 ∈ 𝒫 𝑆 ( 𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ ( 𝑥 ∖ 𝑦 ) = ∪ 𝑧 ) )
43	22 42	jca	⊢ ( ( 𝑆 ∈ 𝑄 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( ( 𝑥 ∩ 𝑦 ) ∈ 𝑆 ∧ ∃ 𝑧 ∈ 𝒫 𝑆 ( 𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ ( 𝑥 ∖ 𝑦 ) = ∪ 𝑧 ) ) )
44	43	ralrimivva	⊢ ( 𝑆 ∈ 𝑄 → ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( ( 𝑥 ∩ 𝑦 ) ∈ 𝑆 ∧ ∃ 𝑧 ∈ 𝒫 𝑆 ( 𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ ( 𝑥 ∖ 𝑦 ) = ∪ 𝑧 ) ) )
45	5 6 44	3jca	⊢ ( 𝑆 ∈ 𝑄 → ( 𝑆 ∈ 𝒫 𝒫 𝑂 ∧ ∅ ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( ( 𝑥 ∩ 𝑦 ) ∈ 𝑆 ∧ ∃ 𝑧 ∈ 𝒫 𝑆 ( 𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ ( 𝑥 ∖ 𝑦 ) = ∪ 𝑧 ) ) ) )
46	2	issros	⊢ ( 𝑆 ∈ 𝑁 ↔ ( 𝑆 ∈ 𝒫 𝒫 𝑂 ∧ ∅ ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( ( 𝑥 ∩ 𝑦 ) ∈ 𝑆 ∧ ∃ 𝑧 ∈ 𝒫 𝑆 ( 𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ ( 𝑥 ∖ 𝑦 ) = ∪ 𝑧 ) ) ) )
47	45 46	sylibr	⊢ ( 𝑆 ∈ 𝑄 → 𝑆 ∈ 𝑁 )