Users' Mathboxes Mathbox for Stefan O'Rear < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  isnacs3 Structured version   Visualization version   GIF version

Theorem isnacs3 37590
Description: A choice-free order equivalent to the Noetherian condition on a closure system. (Contributed by Stefan O'Rear, 4-Apr-2015.)
Assertion
Ref Expression
isnacs3 (𝐶 ∈ (NoeACS‘𝑋) ↔ (𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → 𝑠𝑠)))
Distinct variable groups:   𝐶,𝑠   𝑋,𝑠

Proof of Theorem isnacs3
Dummy variables 𝑔 𝑖 𝑡 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nacsacs 37589 . . . 4 (𝐶 ∈ (NoeACS‘𝑋) → 𝐶 ∈ (ACS‘𝑋))
21acsmred 16364 . . 3 (𝐶 ∈ (NoeACS‘𝑋) → 𝐶 ∈ (Moore‘𝑋))
3 simpll 805 . . . . . . . 8 (((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (toInc‘𝑠) ∈ Dirset) → 𝐶 ∈ (NoeACS‘𝑋))
41ad2antrr 762 . . . . . . . . 9 (((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (toInc‘𝑠) ∈ Dirset) → 𝐶 ∈ (ACS‘𝑋))
5 elpwi 4201 . . . . . . . . . 10 (𝑠 ∈ 𝒫 𝐶𝑠𝐶)
65ad2antlr 763 . . . . . . . . 9 (((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (toInc‘𝑠) ∈ Dirset) → 𝑠𝐶)
7 simpr 476 . . . . . . . . 9 (((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (toInc‘𝑠) ∈ Dirset) → (toInc‘𝑠) ∈ Dirset)
8 acsdrsel 17214 . . . . . . . . 9 ((𝐶 ∈ (ACS‘𝑋) ∧ 𝑠𝐶 ∧ (toInc‘𝑠) ∈ Dirset) → 𝑠𝐶)
94, 6, 7, 8syl3anc 1366 . . . . . . . 8 (((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (toInc‘𝑠) ∈ Dirset) → 𝑠𝐶)
10 eqid 2651 . . . . . . . . 9 (mrCls‘𝐶) = (mrCls‘𝐶)
1110nacsfg 37585 . . . . . . . 8 ((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑠𝐶) → ∃𝑔 ∈ (𝒫 𝑋 ∩ Fin) 𝑠 = ((mrCls‘𝐶)‘𝑔))
123, 9, 11syl2anc 694 . . . . . . 7 (((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (toInc‘𝑠) ∈ Dirset) → ∃𝑔 ∈ (𝒫 𝑋 ∩ Fin) 𝑠 = ((mrCls‘𝐶)‘𝑔))
1310mrefg2 37587 . . . . . . . . 9 (𝐶 ∈ (Moore‘𝑋) → (∃𝑔 ∈ (𝒫 𝑋 ∩ Fin) 𝑠 = ((mrCls‘𝐶)‘𝑔) ↔ ∃𝑔 ∈ (𝒫 𝑠 ∩ Fin) 𝑠 = ((mrCls‘𝐶)‘𝑔)))
142, 13syl 17 . . . . . . . 8 (𝐶 ∈ (NoeACS‘𝑋) → (∃𝑔 ∈ (𝒫 𝑋 ∩ Fin) 𝑠 = ((mrCls‘𝐶)‘𝑔) ↔ ∃𝑔 ∈ (𝒫 𝑠 ∩ Fin) 𝑠 = ((mrCls‘𝐶)‘𝑔)))
1514ad2antrr 762 . . . . . . 7 (((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (toInc‘𝑠) ∈ Dirset) → (∃𝑔 ∈ (𝒫 𝑋 ∩ Fin) 𝑠 = ((mrCls‘𝐶)‘𝑔) ↔ ∃𝑔 ∈ (𝒫 𝑠 ∩ Fin) 𝑠 = ((mrCls‘𝐶)‘𝑔)))
1612, 15mpbid 222 . . . . . 6 (((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (toInc‘𝑠) ∈ Dirset) → ∃𝑔 ∈ (𝒫 𝑠 ∩ Fin) 𝑠 = ((mrCls‘𝐶)‘𝑔))
17 elfpw 8309 . . . . . . . . 9 (𝑔 ∈ (𝒫 𝑠 ∩ Fin) ↔ (𝑔 𝑠𝑔 ∈ Fin))
18 fissuni 8312 . . . . . . . . 9 ((𝑔 𝑠𝑔 ∈ Fin) → ∃ ∈ (𝒫 𝑠 ∩ Fin)𝑔 )
1917, 18sylbi 207 . . . . . . . 8 (𝑔 ∈ (𝒫 𝑠 ∩ Fin) → ∃ ∈ (𝒫 𝑠 ∩ Fin)𝑔 )
20 elfpw 8309 . . . . . . . . . . . 12 ( ∈ (𝒫 𝑠 ∩ Fin) ↔ (𝑠 ∈ Fin))
21 ipodrsfi 17210 . . . . . . . . . . . . 13 (((toInc‘𝑠) ∈ Dirset ∧ 𝑠 ∈ Fin) → ∃𝑖𝑠 𝑖)
22213expb 1285 . . . . . . . . . . . 12 (((toInc‘𝑠) ∈ Dirset ∧ (𝑠 ∈ Fin)) → ∃𝑖𝑠 𝑖)
2320, 22sylan2b 491 . . . . . . . . . . 11 (((toInc‘𝑠) ∈ Dirset ∧ ∈ (𝒫 𝑠 ∩ Fin)) → ∃𝑖𝑠 𝑖)
24 sstr 3644 . . . . . . . . . . . . . . 15 ((𝑔 𝑖) → 𝑔𝑖)
2524ancoms 468 . . . . . . . . . . . . . 14 (( 𝑖𝑔 ) → 𝑔𝑖)
26 simpr 476 . . . . . . . . . . . . . . . . . . 19 ((((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (𝑖𝑠𝑔𝑖)) ∧ 𝑠 = ((mrCls‘𝐶)‘𝑔)) → 𝑠 = ((mrCls‘𝐶)‘𝑔))
272ad2antrr 762 . . . . . . . . . . . . . . . . . . . . 21 (((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (𝑖𝑠𝑔𝑖)) → 𝐶 ∈ (Moore‘𝑋))
28 simprr 811 . . . . . . . . . . . . . . . . . . . . 21 (((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (𝑖𝑠𝑔𝑖)) → 𝑔𝑖)
295ad2antlr 763 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (𝑖𝑠𝑔𝑖)) → 𝑠𝐶)
30 simprl 809 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (𝑖𝑠𝑔𝑖)) → 𝑖𝑠)
3129, 30sseldd 3637 . . . . . . . . . . . . . . . . . . . . 21 (((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (𝑖𝑠𝑔𝑖)) → 𝑖𝐶)
3210mrcsscl 16327 . . . . . . . . . . . . . . . . . . . . 21 ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑔𝑖𝑖𝐶) → ((mrCls‘𝐶)‘𝑔) ⊆ 𝑖)
3327, 28, 31, 32syl3anc 1366 . . . . . . . . . . . . . . . . . . . 20 (((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (𝑖𝑠𝑔𝑖)) → ((mrCls‘𝐶)‘𝑔) ⊆ 𝑖)
3433adantr 480 . . . . . . . . . . . . . . . . . . 19 ((((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (𝑖𝑠𝑔𝑖)) ∧ 𝑠 = ((mrCls‘𝐶)‘𝑔)) → ((mrCls‘𝐶)‘𝑔) ⊆ 𝑖)
3526, 34eqsstrd 3672 . . . . . . . . . . . . . . . . . 18 ((((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (𝑖𝑠𝑔𝑖)) ∧ 𝑠 = ((mrCls‘𝐶)‘𝑔)) → 𝑠𝑖)
36 simplrl 817 . . . . . . . . . . . . . . . . . . 19 ((((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (𝑖𝑠𝑔𝑖)) ∧ 𝑠 = ((mrCls‘𝐶)‘𝑔)) → 𝑖𝑠)
37 elssuni 4499 . . . . . . . . . . . . . . . . . . 19 (𝑖𝑠𝑖 𝑠)
3836, 37syl 17 . . . . . . . . . . . . . . . . . 18 ((((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (𝑖𝑠𝑔𝑖)) ∧ 𝑠 = ((mrCls‘𝐶)‘𝑔)) → 𝑖 𝑠)
3935, 38eqssd 3653 . . . . . . . . . . . . . . . . 17 ((((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (𝑖𝑠𝑔𝑖)) ∧ 𝑠 = ((mrCls‘𝐶)‘𝑔)) → 𝑠 = 𝑖)
4039, 36eqeltrd 2730 . . . . . . . . . . . . . . . 16 ((((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (𝑖𝑠𝑔𝑖)) ∧ 𝑠 = ((mrCls‘𝐶)‘𝑔)) → 𝑠𝑠)
4140ex 449 . . . . . . . . . . . . . . 15 (((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (𝑖𝑠𝑔𝑖)) → ( 𝑠 = ((mrCls‘𝐶)‘𝑔) → 𝑠𝑠))
4241expr 642 . . . . . . . . . . . . . 14 (((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ 𝑖𝑠) → (𝑔𝑖 → ( 𝑠 = ((mrCls‘𝐶)‘𝑔) → 𝑠𝑠)))
4325, 42syl5 34 . . . . . . . . . . . . 13 (((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ 𝑖𝑠) → (( 𝑖𝑔 ) → ( 𝑠 = ((mrCls‘𝐶)‘𝑔) → 𝑠𝑠)))
4443expd 451 . . . . . . . . . . . 12 (((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ 𝑖𝑠) → ( 𝑖 → (𝑔 → ( 𝑠 = ((mrCls‘𝐶)‘𝑔) → 𝑠𝑠))))
4544rexlimdva 3060 . . . . . . . . . . 11 ((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) → (∃𝑖𝑠 𝑖 → (𝑔 → ( 𝑠 = ((mrCls‘𝐶)‘𝑔) → 𝑠𝑠))))
4623, 45syl5 34 . . . . . . . . . 10 ((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) → (((toInc‘𝑠) ∈ Dirset ∧ ∈ (𝒫 𝑠 ∩ Fin)) → (𝑔 → ( 𝑠 = ((mrCls‘𝐶)‘𝑔) → 𝑠𝑠))))
4746expdimp 452 . . . . . . . . 9 (((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (toInc‘𝑠) ∈ Dirset) → ( ∈ (𝒫 𝑠 ∩ Fin) → (𝑔 → ( 𝑠 = ((mrCls‘𝐶)‘𝑔) → 𝑠𝑠))))
4847rexlimdv 3059 . . . . . . . 8 (((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (toInc‘𝑠) ∈ Dirset) → (∃ ∈ (𝒫 𝑠 ∩ Fin)𝑔 → ( 𝑠 = ((mrCls‘𝐶)‘𝑔) → 𝑠𝑠)))
4919, 48syl5 34 . . . . . . 7 (((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (toInc‘𝑠) ∈ Dirset) → (𝑔 ∈ (𝒫 𝑠 ∩ Fin) → ( 𝑠 = ((mrCls‘𝐶)‘𝑔) → 𝑠𝑠)))
5049rexlimdv 3059 . . . . . 6 (((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (toInc‘𝑠) ∈ Dirset) → (∃𝑔 ∈ (𝒫 𝑠 ∩ Fin) 𝑠 = ((mrCls‘𝐶)‘𝑔) → 𝑠𝑠))
5116, 50mpd 15 . . . . 5 (((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) ∧ (toInc‘𝑠) ∈ Dirset) → 𝑠𝑠)
5251ex 449 . . . 4 ((𝐶 ∈ (NoeACS‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) → ((toInc‘𝑠) ∈ Dirset → 𝑠𝑠))
5352ralrimiva 2995 . . 3 (𝐶 ∈ (NoeACS‘𝑋) → ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → 𝑠𝑠))
542, 53jca 553 . 2 (𝐶 ∈ (NoeACS‘𝑋) → (𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → 𝑠𝑠)))
55 simpl 472 . . . 4 ((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → 𝑠𝑠)) → 𝐶 ∈ (Moore‘𝑋))
565adantl 481 . . . . . . . 8 ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) → 𝑠𝐶)
5756sseld 3635 . . . . . . 7 ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) → ( 𝑠𝑠 𝑠𝐶))
5857imim2d 57 . . . . . 6 ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑠 ∈ 𝒫 𝐶) → (((toInc‘𝑠) ∈ Dirset → 𝑠𝑠) → ((toInc‘𝑠) ∈ Dirset → 𝑠𝐶)))
5958ralimdva 2991 . . . . 5 (𝐶 ∈ (Moore‘𝑋) → (∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → 𝑠𝑠) → ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → 𝑠𝐶)))
6059imp 444 . . . 4 ((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → 𝑠𝑠)) → ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → 𝑠𝐶))
61 isacs3 17221 . . . 4 (𝐶 ∈ (ACS‘𝑋) ↔ (𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → 𝑠𝐶)))
6255, 60, 61sylanbrc 699 . . 3 ((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → 𝑠𝑠)) → 𝐶 ∈ (ACS‘𝑋))
6310mrcid 16320 . . . . . . . . . 10 ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑡𝐶) → ((mrCls‘𝐶)‘𝑡) = 𝑡)
6463adantlr 751 . . . . . . . . 9 (((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → 𝑠𝑠)) ∧ 𝑡𝐶) → ((mrCls‘𝐶)‘𝑡) = 𝑡)
6562adantr 480 . . . . . . . . . 10 (((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → 𝑠𝑠)) ∧ 𝑡𝐶) → 𝐶 ∈ (ACS‘𝑋))
66 mress 16300 . . . . . . . . . . 11 ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑡𝐶) → 𝑡𝑋)
6766adantlr 751 . . . . . . . . . 10 (((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → 𝑠𝑠)) ∧ 𝑡𝐶) → 𝑡𝑋)
6865, 10, 67acsficld 17222 . . . . . . . . 9 (((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → 𝑠𝑠)) ∧ 𝑡𝐶) → ((mrCls‘𝐶)‘𝑡) = ((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin)))
6964, 68eqtr3d 2687 . . . . . . . 8 (((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → 𝑠𝑠)) ∧ 𝑡𝐶) → 𝑡 = ((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin)))
7010mrcf 16316 . . . . . . . . . . . . 13 (𝐶 ∈ (Moore‘𝑋) → (mrCls‘𝐶):𝒫 𝑋𝐶)
71 ffn 6083 . . . . . . . . . . . . 13 ((mrCls‘𝐶):𝒫 𝑋𝐶 → (mrCls‘𝐶) Fn 𝒫 𝑋)
7270, 71syl 17 . . . . . . . . . . . 12 (𝐶 ∈ (Moore‘𝑋) → (mrCls‘𝐶) Fn 𝒫 𝑋)
7372adantr 480 . . . . . . . . . . 11 ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑡𝐶) → (mrCls‘𝐶) Fn 𝒫 𝑋)
7410mrcss 16323 . . . . . . . . . . . . 13 ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑔𝑋) → ((mrCls‘𝐶)‘𝑔) ⊆ ((mrCls‘𝐶)‘))
75743expb 1285 . . . . . . . . . . . 12 ((𝐶 ∈ (Moore‘𝑋) ∧ (𝑔𝑋)) → ((mrCls‘𝐶)‘𝑔) ⊆ ((mrCls‘𝐶)‘))
7675adantlr 751 . . . . . . . . . . 11 (((𝐶 ∈ (Moore‘𝑋) ∧ 𝑡𝐶) ∧ (𝑔𝑋)) → ((mrCls‘𝐶)‘𝑔) ⊆ ((mrCls‘𝐶)‘))
77 vex 3234 . . . . . . . . . . . 12 𝑡 ∈ V
78 fpwipodrs 17211 . . . . . . . . . . . 12 (𝑡 ∈ V → (toInc‘(𝒫 𝑡 ∩ Fin)) ∈ Dirset)
7977, 78mp1i 13 . . . . . . . . . . 11 ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑡𝐶) → (toInc‘(𝒫 𝑡 ∩ Fin)) ∈ Dirset)
80 inss1 3866 . . . . . . . . . . . 12 (𝒫 𝑡 ∩ Fin) ⊆ 𝒫 𝑡
81 sspwb 4947 . . . . . . . . . . . . 13 (𝑡𝑋 ↔ 𝒫 𝑡 ⊆ 𝒫 𝑋)
8266, 81sylib 208 . . . . . . . . . . . 12 ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑡𝐶) → 𝒫 𝑡 ⊆ 𝒫 𝑋)
8380, 82syl5ss 3647 . . . . . . . . . . 11 ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑡𝐶) → (𝒫 𝑡 ∩ Fin) ⊆ 𝒫 𝑋)
84 fvex 6239 . . . . . . . . . . . . 13 (mrCls‘𝐶) ∈ V
85 imaexg 7145 . . . . . . . . . . . . 13 ((mrCls‘𝐶) ∈ V → ((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin)) ∈ V)
8684, 85ax-mp 5 . . . . . . . . . . . 12 ((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin)) ∈ V
8786a1i 11 . . . . . . . . . . 11 ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑡𝐶) → ((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin)) ∈ V)
8873, 76, 79, 83, 87ipodrsima 17212 . . . . . . . . . 10 ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑡𝐶) → (toInc‘((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin))) ∈ Dirset)
8988adantlr 751 . . . . . . . . 9 (((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → 𝑠𝑠)) ∧ 𝑡𝐶) → (toInc‘((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin))) ∈ Dirset)
90 imassrn 5512 . . . . . . . . . . . . . 14 ((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin)) ⊆ ran (mrCls‘𝐶)
91 frn 6091 . . . . . . . . . . . . . . 15 ((mrCls‘𝐶):𝒫 𝑋𝐶 → ran (mrCls‘𝐶) ⊆ 𝐶)
9270, 91syl 17 . . . . . . . . . . . . . 14 (𝐶 ∈ (Moore‘𝑋) → ran (mrCls‘𝐶) ⊆ 𝐶)
9390, 92syl5ss 3647 . . . . . . . . . . . . 13 (𝐶 ∈ (Moore‘𝑋) → ((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin)) ⊆ 𝐶)
9493adantr 480 . . . . . . . . . . . 12 ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑡𝐶) → ((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin)) ⊆ 𝐶)
9586elpw 4197 . . . . . . . . . . . 12 (((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin)) ∈ 𝒫 𝐶 ↔ ((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin)) ⊆ 𝐶)
9694, 95sylibr 224 . . . . . . . . . . 11 ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑡𝐶) → ((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin)) ∈ 𝒫 𝐶)
9796adantlr 751 . . . . . . . . . 10 (((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → 𝑠𝑠)) ∧ 𝑡𝐶) → ((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin)) ∈ 𝒫 𝐶)
98 simplr 807 . . . . . . . . . 10 (((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → 𝑠𝑠)) ∧ 𝑡𝐶) → ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → 𝑠𝑠))
99 fveq2 6229 . . . . . . . . . . . . 13 (𝑠 = ((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin)) → (toInc‘𝑠) = (toInc‘((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin))))
10099eleq1d 2715 . . . . . . . . . . . 12 (𝑠 = ((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin)) → ((toInc‘𝑠) ∈ Dirset ↔ (toInc‘((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin))) ∈ Dirset))
101 unieq 4476 . . . . . . . . . . . . 13 (𝑠 = ((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin)) → 𝑠 = ((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin)))
102 id 22 . . . . . . . . . . . . 13 (𝑠 = ((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin)) → 𝑠 = ((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin)))
103101, 102eleq12d 2724 . . . . . . . . . . . 12 (𝑠 = ((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin)) → ( 𝑠𝑠 ((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin)) ∈ ((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin))))
104100, 103imbi12d 333 . . . . . . . . . . 11 (𝑠 = ((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin)) → (((toInc‘𝑠) ∈ Dirset → 𝑠𝑠) ↔ ((toInc‘((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin))) ∈ Dirset → ((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin)) ∈ ((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin)))))
105104rspcva 3338 . . . . . . . . . 10 ((((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin)) ∈ 𝒫 𝐶 ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → 𝑠𝑠)) → ((toInc‘((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin))) ∈ Dirset → ((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin)) ∈ ((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin))))
10697, 98, 105syl2anc 694 . . . . . . . . 9 (((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → 𝑠𝑠)) ∧ 𝑡𝐶) → ((toInc‘((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin))) ∈ Dirset → ((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin)) ∈ ((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin))))
10789, 106mpd 15 . . . . . . . 8 (((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → 𝑠𝑠)) ∧ 𝑡𝐶) → ((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin)) ∈ ((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin)))
10869, 107eqeltrd 2730 . . . . . . 7 (((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → 𝑠𝑠)) ∧ 𝑡𝐶) → 𝑡 ∈ ((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin)))
109 fvelimab 6292 . . . . . . . . 9 (((mrCls‘𝐶) Fn 𝒫 𝑋 ∧ (𝒫 𝑡 ∩ Fin) ⊆ 𝒫 𝑋) → (𝑡 ∈ ((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin)) ↔ ∃𝑔 ∈ (𝒫 𝑡 ∩ Fin)((mrCls‘𝐶)‘𝑔) = 𝑡))
11073, 83, 109syl2anc 694 . . . . . . . 8 ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑡𝐶) → (𝑡 ∈ ((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin)) ↔ ∃𝑔 ∈ (𝒫 𝑡 ∩ Fin)((mrCls‘𝐶)‘𝑔) = 𝑡))
111110adantlr 751 . . . . . . 7 (((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → 𝑠𝑠)) ∧ 𝑡𝐶) → (𝑡 ∈ ((mrCls‘𝐶) “ (𝒫 𝑡 ∩ Fin)) ↔ ∃𝑔 ∈ (𝒫 𝑡 ∩ Fin)((mrCls‘𝐶)‘𝑔) = 𝑡))
112108, 111mpbid 222 . . . . . 6 (((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → 𝑠𝑠)) ∧ 𝑡𝐶) → ∃𝑔 ∈ (𝒫 𝑡 ∩ Fin)((mrCls‘𝐶)‘𝑔) = 𝑡)
113 eqcom 2658 . . . . . . 7 (𝑡 = ((mrCls‘𝐶)‘𝑔) ↔ ((mrCls‘𝐶)‘𝑔) = 𝑡)
114113rexbii 3070 . . . . . 6 (∃𝑔 ∈ (𝒫 𝑡 ∩ Fin)𝑡 = ((mrCls‘𝐶)‘𝑔) ↔ ∃𝑔 ∈ (𝒫 𝑡 ∩ Fin)((mrCls‘𝐶)‘𝑔) = 𝑡)
115112, 114sylibr 224 . . . . 5 (((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → 𝑠𝑠)) ∧ 𝑡𝐶) → ∃𝑔 ∈ (𝒫 𝑡 ∩ Fin)𝑡 = ((mrCls‘𝐶)‘𝑔))
11610mrefg2 37587 . . . . . 6 (𝐶 ∈ (Moore‘𝑋) → (∃𝑔 ∈ (𝒫 𝑋 ∩ Fin)𝑡 = ((mrCls‘𝐶)‘𝑔) ↔ ∃𝑔 ∈ (𝒫 𝑡 ∩ Fin)𝑡 = ((mrCls‘𝐶)‘𝑔)))
117116ad2antrr 762 . . . . 5 (((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → 𝑠𝑠)) ∧ 𝑡𝐶) → (∃𝑔 ∈ (𝒫 𝑋 ∩ Fin)𝑡 = ((mrCls‘𝐶)‘𝑔) ↔ ∃𝑔 ∈ (𝒫 𝑡 ∩ Fin)𝑡 = ((mrCls‘𝐶)‘𝑔)))
118115, 117mpbird 247 . . . 4 (((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → 𝑠𝑠)) ∧ 𝑡𝐶) → ∃𝑔 ∈ (𝒫 𝑋 ∩ Fin)𝑡 = ((mrCls‘𝐶)‘𝑔))
119118ralrimiva 2995 . . 3 ((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → 𝑠𝑠)) → ∀𝑡𝐶𝑔 ∈ (𝒫 𝑋 ∩ Fin)𝑡 = ((mrCls‘𝐶)‘𝑔))
12010isnacs 37584 . . 3 (𝐶 ∈ (NoeACS‘𝑋) ↔ (𝐶 ∈ (ACS‘𝑋) ∧ ∀𝑡𝐶𝑔 ∈ (𝒫 𝑋 ∩ Fin)𝑡 = ((mrCls‘𝐶)‘𝑔)))
12162, 119, 120sylanbrc 699 . 2 ((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → 𝑠𝑠)) → 𝐶 ∈ (NoeACS‘𝑋))
12254, 121impbii 199 1 (𝐶 ∈ (NoeACS‘𝑋) ↔ (𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → 𝑠𝑠)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383   = wceq 1523  wcel 2030  wral 2941  wrex 2942  Vcvv 3231  cin 3606  wss 3607  𝒫 cpw 4191   cuni 4468  ran crn 5144  cima 5146   Fn wfn 5921  wf 5922  cfv 5926  Fincfn 7997  Moorecmre 16289  mrClscmrc 16290  ACScacs 16292  Dirsetcdrs 16974  toInccipo 17198  NoeACScnacs 37582
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-oadd 7609  df-er 7787  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-nn 11059  df-2 11117  df-3 11118  df-4 11119  df-5 11120  df-6 11121  df-7 11122  df-8 11123  df-9 11124  df-n0 11331  df-z 11416  df-dec 11532  df-uz 11726  df-fz 12365  df-struct 15906  df-ndx 15907  df-slot 15908  df-base 15910  df-tset 16007  df-ple 16008  df-ocomp 16010  df-mre 16293  df-mrc 16294  df-acs 16296  df-preset 16975  df-drs 16976  df-poset 16993  df-ipo 17199  df-nacs 37583
This theorem is referenced by:  nacsfix  37592
  Copyright terms: Public domain W3C validator