This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem isacs3lem

Description: An algebraic closure system satisfies isacs3 . (Contributed by Stefan O'Rear, 2-Apr-2015)

Ref Expression
Assertion isacs3lem ( 𝐶 ∈ ( ACS ‘ 𝑋 ) → ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑠 ∈ 𝒫 𝐶 ( ( toInc ‘ 𝑠 ) ∈ Dirset → ∪ 𝑠 ∈ 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 acsmre ⊢ ( 𝐶 ∈ ( ACS ‘ 𝑋 ) → 𝐶 ∈ ( Moore ‘ 𝑋 ) )
2 mresspw ⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → 𝐶 ⊆ 𝒫 𝑋 )
3 1 2 syl ⊢ ( 𝐶 ∈ ( ACS ‘ 𝑋 ) → 𝐶 ⊆ 𝒫 𝑋 )
4 3 sspwd ⊢ ( 𝐶 ∈ ( ACS ‘ 𝑋 ) → 𝒫 𝐶 ⊆ 𝒫 𝒫 𝑋 )
5 4 sselda ⊢ ( ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ∧ 𝑠 ∈ 𝒫 𝐶 ) → 𝑠 ∈ 𝒫 𝒫 𝑋 )
6 5 elpwid ⊢ ( ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ∧ 𝑠 ∈ 𝒫 𝐶 ) → 𝑠 ⊆ 𝒫 𝑋 )
7 sspwuni ⊢ ( 𝑠 ⊆ 𝒫 𝑋 ↔ ∪ 𝑠 ⊆ 𝑋 )
8 6 7 sylib ⊢ ( ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ∧ 𝑠 ∈ 𝒫 𝐶 ) → ∪ 𝑠 ⊆ 𝑋 )
9 8 adantr ⊢ ( ( ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ∧ 𝑠 ∈ 𝒫 𝐶 ) ∧ ( toInc ‘ 𝑠 ) ∈ Dirset ) → ∪ 𝑠 ⊆ 𝑋 )
10 elinel1 ⊢ ( 𝑥 ∈ ( 𝒫 ∪ 𝑠 ∩ Fin ) → 𝑥 ∈ 𝒫 ∪ 𝑠 )
11 10 elpwid ⊢ ( 𝑥 ∈ ( 𝒫 ∪ 𝑠 ∩ Fin ) → 𝑥 ⊆ ∪ 𝑠 )
12 elinel2 ⊢ ( 𝑥 ∈ ( 𝒫 ∪ 𝑠 ∩ Fin ) → 𝑥 ∈ Fin )
13 fissuni ⊢ ( ( 𝑥 ⊆ ∪ 𝑠 ∧ 𝑥 ∈ Fin ) → ∃ 𝑦 ∈ ( 𝒫 𝑠 ∩ Fin ) 𝑥 ⊆ ∪ 𝑦 )
14 11 12 13 syl2anc ⊢ ( 𝑥 ∈ ( 𝒫 ∪ 𝑠 ∩ Fin ) → ∃ 𝑦 ∈ ( 𝒫 𝑠 ∩ Fin ) 𝑥 ⊆ ∪ 𝑦 )
15 14 ad2antll ⊢ ( ( ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ∧ 𝑠 ∈ 𝒫 𝐶 ) ∧ ( ( toInc ‘ 𝑠 ) ∈ Dirset ∧ 𝑥 ∈ ( 𝒫 ∪ 𝑠 ∩ Fin ) ) ) → ∃ 𝑦 ∈ ( 𝒫 𝑠 ∩ Fin ) 𝑥 ⊆ ∪ 𝑦 )
16 1 ad3antrrr ⊢ ( ( ( ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ∧ 𝑠 ∈ 𝒫 𝐶 ) ∧ ( ( toInc ‘ 𝑠 ) ∈ Dirset ∧ 𝑥 ∈ ( 𝒫 ∪ 𝑠 ∩ Fin ) ) ) ∧ ( 𝑦 ∈ ( 𝒫 𝑠 ∩ Fin ) ∧ 𝑥 ⊆ ∪ 𝑦 ) ) → 𝐶 ∈ ( Moore ‘ 𝑋 ) )
17 eqid ⊢ ( mrCls ‘ 𝐶 ) = ( mrCls ‘ 𝐶 )
18 simprr ⊢ ( ( ( ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ∧ 𝑠 ∈ 𝒫 𝐶 ) ∧ ( ( toInc ‘ 𝑠 ) ∈ Dirset ∧ 𝑥 ∈ ( 𝒫 ∪ 𝑠 ∩ Fin ) ) ) ∧ ( 𝑦 ∈ ( 𝒫 𝑠 ∩ Fin ) ∧ 𝑥 ⊆ ∪ 𝑦 ) ) → 𝑥 ⊆ ∪ 𝑦 )
19 elinel1 ⊢ ( 𝑦 ∈ ( 𝒫 𝑠 ∩ Fin ) → 𝑦 ∈ 𝒫 𝑠 )
20 19 elpwid ⊢ ( 𝑦 ∈ ( 𝒫 𝑠 ∩ Fin ) → 𝑦 ⊆ 𝑠 )
21 20 unissd ⊢ ( 𝑦 ∈ ( 𝒫 𝑠 ∩ Fin ) → ∪ 𝑦 ⊆ ∪ 𝑠 )
22 21 ad2antrl ⊢ ( ( ( ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ∧ 𝑠 ∈ 𝒫 𝐶 ) ∧ ( ( toInc ‘ 𝑠 ) ∈ Dirset ∧ 𝑥 ∈ ( 𝒫 ∪ 𝑠 ∩ Fin ) ) ) ∧ ( 𝑦 ∈ ( 𝒫 𝑠 ∩ Fin ) ∧ 𝑥 ⊆ ∪ 𝑦 ) ) → ∪ 𝑦 ⊆ ∪ 𝑠 )
23 8 ad2antrr ⊢ ( ( ( ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ∧ 𝑠 ∈ 𝒫 𝐶 ) ∧ ( ( toInc ‘ 𝑠 ) ∈ Dirset ∧ 𝑥 ∈ ( 𝒫 ∪ 𝑠 ∩ Fin ) ) ) ∧ ( 𝑦 ∈ ( 𝒫 𝑠 ∩ Fin ) ∧ 𝑥 ⊆ ∪ 𝑦 ) ) → ∪ 𝑠 ⊆ 𝑋 )
24 22 23 sstrd ⊢ ( ( ( ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ∧ 𝑠 ∈ 𝒫 𝐶 ) ∧ ( ( toInc ‘ 𝑠 ) ∈ Dirset ∧ 𝑥 ∈ ( 𝒫 ∪ 𝑠 ∩ Fin ) ) ) ∧ ( 𝑦 ∈ ( 𝒫 𝑠 ∩ Fin ) ∧ 𝑥 ⊆ ∪ 𝑦 ) ) → ∪ 𝑦 ⊆ 𝑋 )
25 16 17 18 24 mrcssd ⊢ ( ( ( ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ∧ 𝑠 ∈ 𝒫 𝐶 ) ∧ ( ( toInc ‘ 𝑠 ) ∈ Dirset ∧ 𝑥 ∈ ( 𝒫 ∪ 𝑠 ∩ Fin ) ) ) ∧ ( 𝑦 ∈ ( 𝒫 𝑠 ∩ Fin ) ∧ 𝑥 ⊆ ∪ 𝑦 ) ) → ( ( mrCls ‘ 𝐶 ) ‘ 𝑥 ) ⊆ ( ( mrCls ‘ 𝐶 ) ‘ ∪ 𝑦 ) )
26 simpl ⊢ ( ( ( toInc ‘ 𝑠 ) ∈ Dirset ∧ 𝑦 ∈ ( 𝒫 𝑠 ∩ Fin ) ) → ( toInc ‘ 𝑠 ) ∈ Dirset )
27 20 adantl ⊢ ( ( ( toInc ‘ 𝑠 ) ∈ Dirset ∧ 𝑦 ∈ ( 𝒫 𝑠 ∩ Fin ) ) → 𝑦 ⊆ 𝑠 )
28 elinel2 ⊢ ( 𝑦 ∈ ( 𝒫 𝑠 ∩ Fin ) → 𝑦 ∈ Fin )
29 28 adantl ⊢ ( ( ( toInc ‘ 𝑠 ) ∈ Dirset ∧ 𝑦 ∈ ( 𝒫 𝑠 ∩ Fin ) ) → 𝑦 ∈ Fin )
30 ipodrsfi ⊢ ( ( ( toInc ‘ 𝑠 ) ∈ Dirset ∧ 𝑦 ⊆ 𝑠 ∧ 𝑦 ∈ Fin ) → ∃ 𝑥 ∈ 𝑠 ∪ 𝑦 ⊆ 𝑥 )
31 26 27 29 30 syl3anc ⊢ ( ( ( toInc ‘ 𝑠 ) ∈ Dirset ∧ 𝑦 ∈ ( 𝒫 𝑠 ∩ Fin ) ) → ∃ 𝑥 ∈ 𝑠 ∪ 𝑦 ⊆ 𝑥 )
32 31 adantl ⊢ ( ( ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ∧ 𝑠 ∈ 𝒫 𝐶 ) ∧ ( ( toInc ‘ 𝑠 ) ∈ Dirset ∧ 𝑦 ∈ ( 𝒫 𝑠 ∩ Fin ) ) ) → ∃ 𝑥 ∈ 𝑠 ∪ 𝑦 ⊆ 𝑥 )
33 1 ad3antrrr ⊢ ( ( ( ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ∧ 𝑠 ∈ 𝒫 𝐶 ) ∧ ( ( toInc ‘ 𝑠 ) ∈ Dirset ∧ 𝑦 ∈ ( 𝒫 𝑠 ∩ Fin ) ) ) ∧ ( 𝑥 ∈ 𝑠 ∧ ∪ 𝑦 ⊆ 𝑥 ) ) → 𝐶 ∈ ( Moore ‘ 𝑋 ) )
34 simprr ⊢ ( ( ( ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ∧ 𝑠 ∈ 𝒫 𝐶 ) ∧ ( ( toInc ‘ 𝑠 ) ∈ Dirset ∧ 𝑦 ∈ ( 𝒫 𝑠 ∩ Fin ) ) ) ∧ ( 𝑥 ∈ 𝑠 ∧ ∪ 𝑦 ⊆ 𝑥 ) ) → ∪ 𝑦 ⊆ 𝑥 )
35 elpwi ⊢ ( 𝑠 ∈ 𝒫 𝐶 → 𝑠 ⊆ 𝐶 )
36 35 adantl ⊢ ( ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ∧ 𝑠 ∈ 𝒫 𝐶 ) → 𝑠 ⊆ 𝐶 )
37 36 ad2antrr ⊢ ( ( ( ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ∧ 𝑠 ∈ 𝒫 𝐶 ) ∧ ( ( toInc ‘ 𝑠 ) ∈ Dirset ∧ 𝑦 ∈ ( 𝒫 𝑠 ∩ Fin ) ) ) ∧ ( 𝑥 ∈ 𝑠 ∧ ∪ 𝑦 ⊆ 𝑥 ) ) → 𝑠 ⊆ 𝐶 )
38 simprl ⊢ ( ( ( ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ∧ 𝑠 ∈ 𝒫 𝐶 ) ∧ ( ( toInc ‘ 𝑠 ) ∈ Dirset ∧ 𝑦 ∈ ( 𝒫 𝑠 ∩ Fin ) ) ) ∧ ( 𝑥 ∈ 𝑠 ∧ ∪ 𝑦 ⊆ 𝑥 ) ) → 𝑥 ∈ 𝑠 )
39 37 38 sseldd ⊢ ( ( ( ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ∧ 𝑠 ∈ 𝒫 𝐶 ) ∧ ( ( toInc ‘ 𝑠 ) ∈ Dirset ∧ 𝑦 ∈ ( 𝒫 𝑠 ∩ Fin ) ) ) ∧ ( 𝑥 ∈ 𝑠 ∧ ∪ 𝑦 ⊆ 𝑥 ) ) → 𝑥 ∈ 𝐶 )
40 17 mrcsscl ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∪ 𝑦 ⊆ 𝑥 ∧ 𝑥 ∈ 𝐶 ) → ( ( mrCls ‘ 𝐶 ) ‘ ∪ 𝑦 ) ⊆ 𝑥 )
41 33 34 39 40 syl3anc ⊢ ( ( ( ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ∧ 𝑠 ∈ 𝒫 𝐶 ) ∧ ( ( toInc ‘ 𝑠 ) ∈ Dirset ∧ 𝑦 ∈ ( 𝒫 𝑠 ∩ Fin ) ) ) ∧ ( 𝑥 ∈ 𝑠 ∧ ∪ 𝑦 ⊆ 𝑥 ) ) → ( ( mrCls ‘ 𝐶 ) ‘ ∪ 𝑦 ) ⊆ 𝑥 )
42 elssuni ⊢ ( 𝑥 ∈ 𝑠 → 𝑥 ⊆ ∪ 𝑠 )
43 42 ad2antrl ⊢ ( ( ( ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ∧ 𝑠 ∈ 𝒫 𝐶 ) ∧ ( ( toInc ‘ 𝑠 ) ∈ Dirset ∧ 𝑦 ∈ ( 𝒫 𝑠 ∩ Fin ) ) ) ∧ ( 𝑥 ∈ 𝑠 ∧ ∪ 𝑦 ⊆ 𝑥 ) ) → 𝑥 ⊆ ∪ 𝑠 )
44 41 43 sstrd ⊢ ( ( ( ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ∧ 𝑠 ∈ 𝒫 𝐶 ) ∧ ( ( toInc ‘ 𝑠 ) ∈ Dirset ∧ 𝑦 ∈ ( 𝒫 𝑠 ∩ Fin ) ) ) ∧ ( 𝑥 ∈ 𝑠 ∧ ∪ 𝑦 ⊆ 𝑥 ) ) → ( ( mrCls ‘ 𝐶 ) ‘ ∪ 𝑦 ) ⊆ ∪ 𝑠 )
45 32 44 rexlimddv ⊢ ( ( ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ∧ 𝑠 ∈ 𝒫 𝐶 ) ∧ ( ( toInc ‘ 𝑠 ) ∈ Dirset ∧ 𝑦 ∈ ( 𝒫 𝑠 ∩ Fin ) ) ) → ( ( mrCls ‘ 𝐶 ) ‘ ∪ 𝑦 ) ⊆ ∪ 𝑠 )
46 45 anassrs ⊢ ( ( ( ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ∧ 𝑠 ∈ 𝒫 𝐶 ) ∧ ( toInc ‘ 𝑠 ) ∈ Dirset ) ∧ 𝑦 ∈ ( 𝒫 𝑠 ∩ Fin ) ) → ( ( mrCls ‘ 𝐶 ) ‘ ∪ 𝑦 ) ⊆ ∪ 𝑠 )
47 46 adantrr ⊢ ( ( ( ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ∧ 𝑠 ∈ 𝒫 𝐶 ) ∧ ( toInc ‘ 𝑠 ) ∈ Dirset ) ∧ ( 𝑦 ∈ ( 𝒫 𝑠 ∩ Fin ) ∧ 𝑥 ⊆ ∪ 𝑦 ) ) → ( ( mrCls ‘ 𝐶 ) ‘ ∪ 𝑦 ) ⊆ ∪ 𝑠 )
48 47 adantlrr ⊢ ( ( ( ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ∧ 𝑠 ∈ 𝒫 𝐶 ) ∧ ( ( toInc ‘ 𝑠 ) ∈ Dirset ∧ 𝑥 ∈ ( 𝒫 ∪ 𝑠 ∩ Fin ) ) ) ∧ ( 𝑦 ∈ ( 𝒫 𝑠 ∩ Fin ) ∧ 𝑥 ⊆ ∪ 𝑦 ) ) → ( ( mrCls ‘ 𝐶 ) ‘ ∪ 𝑦 ) ⊆ ∪ 𝑠 )
49 25 48 sstrd ⊢ ( ( ( ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ∧ 𝑠 ∈ 𝒫 𝐶 ) ∧ ( ( toInc ‘ 𝑠 ) ∈ Dirset ∧ 𝑥 ∈ ( 𝒫 ∪ 𝑠 ∩ Fin ) ) ) ∧ ( 𝑦 ∈ ( 𝒫 𝑠 ∩ Fin ) ∧ 𝑥 ⊆ ∪ 𝑦 ) ) → ( ( mrCls ‘ 𝐶 ) ‘ 𝑥 ) ⊆ ∪ 𝑠 )
50 15 49 rexlimddv ⊢ ( ( ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ∧ 𝑠 ∈ 𝒫 𝐶 ) ∧ ( ( toInc ‘ 𝑠 ) ∈ Dirset ∧ 𝑥 ∈ ( 𝒫 ∪ 𝑠 ∩ Fin ) ) ) → ( ( mrCls ‘ 𝐶 ) ‘ 𝑥 ) ⊆ ∪ 𝑠 )
51 50 anassrs ⊢ ( ( ( ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ∧ 𝑠 ∈ 𝒫 𝐶 ) ∧ ( toInc ‘ 𝑠 ) ∈ Dirset ) ∧ 𝑥 ∈ ( 𝒫 ∪ 𝑠 ∩ Fin ) ) → ( ( mrCls ‘ 𝐶 ) ‘ 𝑥 ) ⊆ ∪ 𝑠 )
52 51 ralrimiva ⊢ ( ( ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ∧ 𝑠 ∈ 𝒫 𝐶 ) ∧ ( toInc ‘ 𝑠 ) ∈ Dirset ) → ∀ 𝑥 ∈ ( 𝒫 ∪ 𝑠 ∩ Fin ) ( ( mrCls ‘ 𝐶 ) ‘ 𝑥 ) ⊆ ∪ 𝑠 )
53 17 acsfiel ⊢ ( 𝐶 ∈ ( ACS ‘ 𝑋 ) → ( ∪ 𝑠 ∈ 𝐶 ↔ ( ∪ 𝑠 ⊆ 𝑋 ∧ ∀ 𝑥 ∈ ( 𝒫 ∪ 𝑠 ∩ Fin ) ( ( mrCls ‘ 𝐶 ) ‘ 𝑥 ) ⊆ ∪ 𝑠 ) ) )
54 53 ad2antrr ⊢ ( ( ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ∧ 𝑠 ∈ 𝒫 𝐶 ) ∧ ( toInc ‘ 𝑠 ) ∈ Dirset ) → ( ∪ 𝑠 ∈ 𝐶 ↔ ( ∪ 𝑠 ⊆ 𝑋 ∧ ∀ 𝑥 ∈ ( 𝒫 ∪ 𝑠 ∩ Fin ) ( ( mrCls ‘ 𝐶 ) ‘ 𝑥 ) ⊆ ∪ 𝑠 ) ) )
55 9 52 54 mpbir2and ⊢ ( ( ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ∧ 𝑠 ∈ 𝒫 𝐶 ) ∧ ( toInc ‘ 𝑠 ) ∈ Dirset ) → ∪ 𝑠 ∈ 𝐶 )
56 55 ex ⊢ ( ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ∧ 𝑠 ∈ 𝒫 𝐶 ) → ( ( toInc ‘ 𝑠 ) ∈ Dirset → ∪ 𝑠 ∈ 𝐶 ) )
57 56 ralrimiva ⊢ ( 𝐶 ∈ ( ACS ‘ 𝑋 ) → ∀ 𝑠 ∈ 𝒫 𝐶 ( ( toInc ‘ 𝑠 ) ∈ Dirset → ∪ 𝑠 ∈ 𝐶 ) )
58 1 57 jca ⊢ ( 𝐶 ∈ ( ACS ‘ 𝑋 ) → ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑠 ∈ 𝒫 𝐶 ( ( toInc ‘ 𝑠 ) ∈ Dirset → ∪ 𝑠 ∈ 𝐶 ) ) )