Metamath Proof Explorer


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 ( 𝑆𝑄𝑆𝑁 )