MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  isacs2 Structured version   Visualization version   GIF version

Theorem isacs2 17640
Description: In the definition of an algebraic closure system, we may always take the operation being closed over as the Moore closure. (Contributed by Stefan O'Rear, 2-Apr-2015.)
Hypothesis
Ref Expression
isacs2.f 𝐹 = (mrCls‘𝐶)
Assertion
Ref Expression
isacs2 (𝐶 ∈ (ACS‘𝑋) ↔ (𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝑋(𝑠𝐶 ↔ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠)))
Distinct variable groups:   𝐶,𝑠,𝑦   𝐹,𝑠,𝑦   𝑋,𝑠,𝑦

Proof of Theorem isacs2
Dummy variables 𝑓 𝑡 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 isacs 17638 . 2 (𝐶 ∈ (ACS‘𝑋) ↔ (𝐶 ∈ (Moore‘𝑋) ∧ ∃𝑓(𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 (𝑓 “ (𝒫 𝑡 ∩ Fin)) ⊆ 𝑡))))
2 ffun 6730 . . . . . . . . . . 11 (𝑓:𝒫 𝑋⟶𝒫 𝑋 → Fun 𝑓)
3 funiunfv 7264 . . . . . . . . . . 11 (Fun 𝑓 𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) = (𝑓 “ (𝒫 𝑡 ∩ Fin)))
42, 3syl 17 . . . . . . . . . 10 (𝑓:𝒫 𝑋⟶𝒫 𝑋 𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) = (𝑓 “ (𝒫 𝑡 ∩ Fin)))
54sseq1d 4013 . . . . . . . . 9 (𝑓:𝒫 𝑋⟶𝒫 𝑋 → ( 𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡 (𝑓 “ (𝒫 𝑡 ∩ Fin)) ⊆ 𝑡))
6 iunss 5052 . . . . . . . . 9 ( 𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡)
75, 6bitr3di 285 . . . . . . . 8 (𝑓:𝒫 𝑋⟶𝒫 𝑋 → ( (𝑓 “ (𝒫 𝑡 ∩ Fin)) ⊆ 𝑡 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))
87bibi2d 341 . . . . . . 7 (𝑓:𝒫 𝑋⟶𝒫 𝑋 → ((𝑡𝐶 (𝑓 “ (𝒫 𝑡 ∩ Fin)) ⊆ 𝑡) ↔ (𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡)))
98ralbidv 3175 . . . . . 6 (𝑓:𝒫 𝑋⟶𝒫 𝑋 → (∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 (𝑓 “ (𝒫 𝑡 ∩ Fin)) ⊆ 𝑡) ↔ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡)))
109pm5.32i 573 . . . . 5 ((𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 (𝑓 “ (𝒫 𝑡 ∩ Fin)) ⊆ 𝑡)) ↔ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡)))
1110exbii 1842 . . . 4 (∃𝑓(𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 (𝑓 “ (𝒫 𝑡 ∩ Fin)) ⊆ 𝑡)) ↔ ∃𝑓(𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡)))
12 simpll 765 . . . . . . . . . . . 12 (((𝐶 ∈ (Moore‘𝑋) ∧ 𝑠𝐶) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → 𝐶 ∈ (Moore‘𝑋))
13 elinel1 4197 . . . . . . . . . . . . . 14 (𝑦 ∈ (𝒫 𝑠 ∩ Fin) → 𝑦 ∈ 𝒫 𝑠)
1413elpwid 4615 . . . . . . . . . . . . 13 (𝑦 ∈ (𝒫 𝑠 ∩ Fin) → 𝑦𝑠)
1514adantl 480 . . . . . . . . . . . 12 (((𝐶 ∈ (Moore‘𝑋) ∧ 𝑠𝐶) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → 𝑦𝑠)
16 simplr 767 . . . . . . . . . . . 12 (((𝐶 ∈ (Moore‘𝑋) ∧ 𝑠𝐶) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → 𝑠𝐶)
17 isacs2.f . . . . . . . . . . . . 13 𝐹 = (mrCls‘𝐶)
1817mrcsscl 17607 . . . . . . . . . . . 12 ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑦𝑠𝑠𝐶) → (𝐹𝑦) ⊆ 𝑠)
1912, 15, 16, 18syl3anc 1368 . . . . . . . . . . 11 (((𝐶 ∈ (Moore‘𝑋) ∧ 𝑠𝐶) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → (𝐹𝑦) ⊆ 𝑠)
2019ralrimiva 3143 . . . . . . . . . 10 ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑠𝐶) → ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠)
2120ad4ant14 750 . . . . . . . . 9 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ 𝑠𝐶) → ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠)
22 fveq2 6902 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑦 → (𝑓𝑧) = (𝑓𝑦))
2322sseq1d 4013 . . . . . . . . . . . . . . 15 (𝑧 = 𝑦 → ((𝑓𝑧) ⊆ (𝐹𝑦) ↔ (𝑓𝑦) ⊆ (𝐹𝑦)))
24 simplll 773 . . . . . . . . . . . . . . . . 17 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → 𝐶 ∈ (Moore‘𝑋))
2514adantl 480 . . . . . . . . . . . . . . . . . 18 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → 𝑦𝑠)
26 elpwi 4613 . . . . . . . . . . . . . . . . . . 19 (𝑠 ∈ 𝒫 𝑋𝑠𝑋)
2726ad2antlr 725 . . . . . . . . . . . . . . . . . 18 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → 𝑠𝑋)
2825, 27sstrd 3992 . . . . . . . . . . . . . . . . 17 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → 𝑦𝑋)
2917mrccl 17598 . . . . . . . . . . . . . . . . 17 ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑦𝑋) → (𝐹𝑦) ∈ 𝐶)
3024, 28, 29syl2anc 582 . . . . . . . . . . . . . . . 16 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → (𝐹𝑦) ∈ 𝐶)
31 eleq1 2817 . . . . . . . . . . . . . . . . . 18 (𝑡 = (𝐹𝑦) → (𝑡𝐶 ↔ (𝐹𝑦) ∈ 𝐶))
32 pweq 4620 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = (𝐹𝑦) → 𝒫 𝑡 = 𝒫 (𝐹𝑦))
3332ineq1d 4213 . . . . . . . . . . . . . . . . . . 19 (𝑡 = (𝐹𝑦) → (𝒫 𝑡 ∩ Fin) = (𝒫 (𝐹𝑦) ∩ Fin))
34 sseq2 4008 . . . . . . . . . . . . . . . . . . 19 (𝑡 = (𝐹𝑦) → ((𝑓𝑧) ⊆ 𝑡 ↔ (𝑓𝑧) ⊆ (𝐹𝑦)))
3533, 34raleqbidv 3340 . . . . . . . . . . . . . . . . . 18 (𝑡 = (𝐹𝑦) → (∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡 ↔ ∀𝑧 ∈ (𝒫 (𝐹𝑦) ∩ Fin)(𝑓𝑧) ⊆ (𝐹𝑦)))
3631, 35bibi12d 344 . . . . . . . . . . . . . . . . 17 (𝑡 = (𝐹𝑦) → ((𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡) ↔ ((𝐹𝑦) ∈ 𝐶 ↔ ∀𝑧 ∈ (𝒫 (𝐹𝑦) ∩ Fin)(𝑓𝑧) ⊆ (𝐹𝑦))))
37 simprr 771 . . . . . . . . . . . . . . . . . 18 ((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) → ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))
3837ad2antrr 724 . . . . . . . . . . . . . . . . 17 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))
39 mresspw 17579 . . . . . . . . . . . . . . . . . . 19 (𝐶 ∈ (Moore‘𝑋) → 𝐶 ⊆ 𝒫 𝑋)
4039ad3antrrr 728 . . . . . . . . . . . . . . . . . 18 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → 𝐶 ⊆ 𝒫 𝑋)
4140, 30sseldd 3983 . . . . . . . . . . . . . . . . 17 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → (𝐹𝑦) ∈ 𝒫 𝑋)
4236, 38, 41rspcdva 3612 . . . . . . . . . . . . . . . 16 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → ((𝐹𝑦) ∈ 𝐶 ↔ ∀𝑧 ∈ (𝒫 (𝐹𝑦) ∩ Fin)(𝑓𝑧) ⊆ (𝐹𝑦)))
4330, 42mpbid 231 . . . . . . . . . . . . . . 15 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → ∀𝑧 ∈ (𝒫 (𝐹𝑦) ∩ Fin)(𝑓𝑧) ⊆ (𝐹𝑦))
4424, 17, 28mrcssidd 17612 . . . . . . . . . . . . . . . . 17 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → 𝑦 ⊆ (𝐹𝑦))
45 vex 3477 . . . . . . . . . . . . . . . . . 18 𝑦 ∈ V
4645elpw 4610 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ 𝒫 (𝐹𝑦) ↔ 𝑦 ⊆ (𝐹𝑦))
4744, 46sylibr 233 . . . . . . . . . . . . . . . 16 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → 𝑦 ∈ 𝒫 (𝐹𝑦))
48 elinel2 4198 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (𝒫 𝑠 ∩ Fin) → 𝑦 ∈ Fin)
4948adantl 480 . . . . . . . . . . . . . . . 16 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → 𝑦 ∈ Fin)
5047, 49elind 4196 . . . . . . . . . . . . . . 15 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → 𝑦 ∈ (𝒫 (𝐹𝑦) ∩ Fin))
5123, 43, 50rspcdva 3612 . . . . . . . . . . . . . 14 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → (𝑓𝑦) ⊆ (𝐹𝑦))
52 sstr2 3989 . . . . . . . . . . . . . 14 ((𝑓𝑦) ⊆ (𝐹𝑦) → ((𝐹𝑦) ⊆ 𝑠 → (𝑓𝑦) ⊆ 𝑠))
5351, 52syl 17 . . . . . . . . . . . . 13 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → ((𝐹𝑦) ⊆ 𝑠 → (𝑓𝑦) ⊆ 𝑠))
5453ralimdva 3164 . . . . . . . . . . . 12 (((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) → (∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠 → ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝑓𝑦) ⊆ 𝑠))
5554imp 405 . . . . . . . . . . 11 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠) → ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝑓𝑦) ⊆ 𝑠)
56 fveq2 6902 . . . . . . . . . . . . 13 (𝑦 = 𝑧 → (𝑓𝑦) = (𝑓𝑧))
5756sseq1d 4013 . . . . . . . . . . . 12 (𝑦 = 𝑧 → ((𝑓𝑦) ⊆ 𝑠 ↔ (𝑓𝑧) ⊆ 𝑠))
5857cbvralvw 3232 . . . . . . . . . . 11 (∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝑓𝑦) ⊆ 𝑠 ↔ ∀𝑧 ∈ (𝒫 𝑠 ∩ Fin)(𝑓𝑧) ⊆ 𝑠)
5955, 58sylib 217 . . . . . . . . . 10 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠) → ∀𝑧 ∈ (𝒫 𝑠 ∩ Fin)(𝑓𝑧) ⊆ 𝑠)
60 eleq1 2817 . . . . . . . . . . . 12 (𝑡 = 𝑠 → (𝑡𝐶𝑠𝐶))
61 pweq 4620 . . . . . . . . . . . . . 14 (𝑡 = 𝑠 → 𝒫 𝑡 = 𝒫 𝑠)
6261ineq1d 4213 . . . . . . . . . . . . 13 (𝑡 = 𝑠 → (𝒫 𝑡 ∩ Fin) = (𝒫 𝑠 ∩ Fin))
63 sseq2 4008 . . . . . . . . . . . . 13 (𝑡 = 𝑠 → ((𝑓𝑧) ⊆ 𝑡 ↔ (𝑓𝑧) ⊆ 𝑠))
6462, 63raleqbidv 3340 . . . . . . . . . . . 12 (𝑡 = 𝑠 → (∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡 ↔ ∀𝑧 ∈ (𝒫 𝑠 ∩ Fin)(𝑓𝑧) ⊆ 𝑠))
6560, 64bibi12d 344 . . . . . . . . . . 11 (𝑡 = 𝑠 → ((𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡) ↔ (𝑠𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑠 ∩ Fin)(𝑓𝑧) ⊆ 𝑠)))
6637ad2antrr 724 . . . . . . . . . . 11 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠) → ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))
67 simplr 767 . . . . . . . . . . 11 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠) → 𝑠 ∈ 𝒫 𝑋)
6865, 66, 67rspcdva 3612 . . . . . . . . . 10 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠) → (𝑠𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑠 ∩ Fin)(𝑓𝑧) ⊆ 𝑠))
6959, 68mpbird 256 . . . . . . . . 9 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠) → 𝑠𝐶)
7021, 69impbida 799 . . . . . . . 8 (((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) → (𝑠𝐶 ↔ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠))
7170ralrimiva 3143 . . . . . . 7 ((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) → ∀𝑠 ∈ 𝒫 𝑋(𝑠𝐶 ↔ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠))
7271ex 411 . . . . . 6 (𝐶 ∈ (Moore‘𝑋) → ((𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡)) → ∀𝑠 ∈ 𝒫 𝑋(𝑠𝐶 ↔ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠)))
7372exlimdv 1928 . . . . 5 (𝐶 ∈ (Moore‘𝑋) → (∃𝑓(𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡)) → ∀𝑠 ∈ 𝒫 𝑋(𝑠𝐶 ↔ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠)))
7417mrcf 17596 . . . . . . . 8 (𝐶 ∈ (Moore‘𝑋) → 𝐹:𝒫 𝑋𝐶)
7574, 39fssd 6745 . . . . . . 7 (𝐶 ∈ (Moore‘𝑋) → 𝐹:𝒫 𝑋⟶𝒫 𝑋)
7617fvexi 6916 . . . . . . . 8 𝐹 ∈ V
77 feq1 6708 . . . . . . . . 9 (𝑓 = 𝐹 → (𝑓:𝒫 𝑋⟶𝒫 𝑋𝐹:𝒫 𝑋⟶𝒫 𝑋))
78 fveq1 6901 . . . . . . . . . . . . . . 15 (𝑓 = 𝐹 → (𝑓𝑧) = (𝐹𝑧))
7978sseq1d 4013 . . . . . . . . . . . . . 14 (𝑓 = 𝐹 → ((𝑓𝑧) ⊆ 𝑡 ↔ (𝐹𝑧) ⊆ 𝑡))
8079ralbidv 3175 . . . . . . . . . . . . 13 (𝑓 = 𝐹 → (∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝐹𝑧) ⊆ 𝑡))
81 fveq2 6902 . . . . . . . . . . . . . . 15 (𝑧 = 𝑦 → (𝐹𝑧) = (𝐹𝑦))
8281sseq1d 4013 . . . . . . . . . . . . . 14 (𝑧 = 𝑦 → ((𝐹𝑧) ⊆ 𝑡 ↔ (𝐹𝑦) ⊆ 𝑡))
8382cbvralvw 3232 . . . . . . . . . . . . 13 (∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝐹𝑧) ⊆ 𝑡 ↔ ∀𝑦 ∈ (𝒫 𝑡 ∩ Fin)(𝐹𝑦) ⊆ 𝑡)
8480, 83bitrdi 286 . . . . . . . . . . . 12 (𝑓 = 𝐹 → (∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡 ↔ ∀𝑦 ∈ (𝒫 𝑡 ∩ Fin)(𝐹𝑦) ⊆ 𝑡))
8584bibi2d 341 . . . . . . . . . . 11 (𝑓 = 𝐹 → ((𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡) ↔ (𝑡𝐶 ↔ ∀𝑦 ∈ (𝒫 𝑡 ∩ Fin)(𝐹𝑦) ⊆ 𝑡)))
8685ralbidv 3175 . . . . . . . . . 10 (𝑓 = 𝐹 → (∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡) ↔ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑦 ∈ (𝒫 𝑡 ∩ Fin)(𝐹𝑦) ⊆ 𝑡)))
87 sseq2 4008 . . . . . . . . . . . . 13 (𝑡 = 𝑠 → ((𝐹𝑦) ⊆ 𝑡 ↔ (𝐹𝑦) ⊆ 𝑠))
8862, 87raleqbidv 3340 . . . . . . . . . . . 12 (𝑡 = 𝑠 → (∀𝑦 ∈ (𝒫 𝑡 ∩ Fin)(𝐹𝑦) ⊆ 𝑡 ↔ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠))
8960, 88bibi12d 344 . . . . . . . . . . 11 (𝑡 = 𝑠 → ((𝑡𝐶 ↔ ∀𝑦 ∈ (𝒫 𝑡 ∩ Fin)(𝐹𝑦) ⊆ 𝑡) ↔ (𝑠𝐶 ↔ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠)))
9089cbvralvw 3232 . . . . . . . . . 10 (∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑦 ∈ (𝒫 𝑡 ∩ Fin)(𝐹𝑦) ⊆ 𝑡) ↔ ∀𝑠 ∈ 𝒫 𝑋(𝑠𝐶 ↔ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠))
9186, 90bitrdi 286 . . . . . . . . 9 (𝑓 = 𝐹 → (∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡) ↔ ∀𝑠 ∈ 𝒫 𝑋(𝑠𝐶 ↔ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠)))
9277, 91anbi12d 630 . . . . . . . 8 (𝑓 = 𝐹 → ((𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡)) ↔ (𝐹:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑠 ∈ 𝒫 𝑋(𝑠𝐶 ↔ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠))))
9376, 92spcev 3595 . . . . . . 7 ((𝐹:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑠 ∈ 𝒫 𝑋(𝑠𝐶 ↔ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠)) → ∃𝑓(𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡)))
9475, 93sylan 578 . . . . . 6 ((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝑋(𝑠𝐶 ↔ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠)) → ∃𝑓(𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡)))
9594ex 411 . . . . 5 (𝐶 ∈ (Moore‘𝑋) → (∀𝑠 ∈ 𝒫 𝑋(𝑠𝐶 ↔ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠) → ∃𝑓(𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))))
9673, 95impbid 211 . . . 4 (𝐶 ∈ (Moore‘𝑋) → (∃𝑓(𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡)) ↔ ∀𝑠 ∈ 𝒫 𝑋(𝑠𝐶 ↔ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠)))
9711, 96bitrid 282 . . 3 (𝐶 ∈ (Moore‘𝑋) → (∃𝑓(𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 (𝑓 “ (𝒫 𝑡 ∩ Fin)) ⊆ 𝑡)) ↔ ∀𝑠 ∈ 𝒫 𝑋(𝑠𝐶 ↔ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠)))
9897pm5.32i 573 . 2 ((𝐶 ∈ (Moore‘𝑋) ∧ ∃𝑓(𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 (𝑓 “ (𝒫 𝑡 ∩ Fin)) ⊆ 𝑡))) ↔ (𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝑋(𝑠𝐶 ↔ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠)))
991, 98bitri 274 1 (𝐶 ∈ (ACS‘𝑋) ↔ (𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝑋(𝑠𝐶 ↔ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 394   = wceq 1533  wex 1773  wcel 2098  wral 3058  cin 3948  wss 3949  𝒫 cpw 4606   cuni 4912   ciun 5000  cima 5685  Fun wfun 6547  wf 6549  cfv 6553  Fincfn 8970  Moorecmre 17569  mrClscmrc 17570  ACScacs 17572
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2699  ax-sep 5303  ax-nul 5310  ax-pow 5369  ax-pr 5433  ax-un 7746
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2529  df-eu 2558  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-ral 3059  df-rex 3068  df-rab 3431  df-v 3475  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4327  df-if 4533  df-pw 4608  df-sn 4633  df-pr 4635  df-op 4639  df-uni 4913  df-int 4954  df-iun 5002  df-br 5153  df-opab 5215  df-mpt 5236  df-id 5580  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-iota 6505  df-fun 6555  df-fn 6556  df-f 6557  df-fv 6561  df-mre 17573  df-mrc 17574  df-acs 17576
This theorem is referenced by:  acsfiel  17641  isacs5  18547
  Copyright terms: Public domain W3C validator