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

Theorem isacs2 17533
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 17531 . 2 (𝐶 ∈ (ACS‘𝑋) ↔ (𝐶 ∈ (Moore‘𝑋) ∧ ∃𝑓(𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 (𝑓 “ (𝒫 𝑡 ∩ Fin)) ⊆ 𝑡))))
2 ffun 6671 . . . . . . . . . . 11 (𝑓:𝒫 𝑋⟶𝒫 𝑋 → Fun 𝑓)
3 funiunfv 7195 . . . . . . . . . . 11 (Fun 𝑓 𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) = (𝑓 “ (𝒫 𝑡 ∩ Fin)))
42, 3syl 17 . . . . . . . . . 10 (𝑓:𝒫 𝑋⟶𝒫 𝑋 𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) = (𝑓 “ (𝒫 𝑡 ∩ Fin)))
54sseq1d 3975 . . . . . . . . 9 (𝑓:𝒫 𝑋⟶𝒫 𝑋 → ( 𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡 (𝑓 “ (𝒫 𝑡 ∩ Fin)) ⊆ 𝑡))
6 iunss 5005 . . . . . . . . 9 ( 𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡)
75, 6bitr3di 285 . . . . . . . 8 (𝑓:𝒫 𝑋⟶𝒫 𝑋 → ( (𝑓 “ (𝒫 𝑡 ∩ Fin)) ⊆ 𝑡 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))
87bibi2d 342 . . . . . . 7 (𝑓:𝒫 𝑋⟶𝒫 𝑋 → ((𝑡𝐶 (𝑓 “ (𝒫 𝑡 ∩ Fin)) ⊆ 𝑡) ↔ (𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡)))
98ralbidv 3174 . . . . . 6 (𝑓:𝒫 𝑋⟶𝒫 𝑋 → (∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 (𝑓 “ (𝒫 𝑡 ∩ Fin)) ⊆ 𝑡) ↔ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡)))
109pm5.32i 575 . . . . 5 ((𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 (𝑓 “ (𝒫 𝑡 ∩ Fin)) ⊆ 𝑡)) ↔ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡)))
1110exbii 1850 . . . 4 (∃𝑓(𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 (𝑓 “ (𝒫 𝑡 ∩ Fin)) ⊆ 𝑡)) ↔ ∃𝑓(𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡)))
12 simpll 765 . . . . . . . . . . . 12 (((𝐶 ∈ (Moore‘𝑋) ∧ 𝑠𝐶) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → 𝐶 ∈ (Moore‘𝑋))
13 elinel1 4155 . . . . . . . . . . . . . 14 (𝑦 ∈ (𝒫 𝑠 ∩ Fin) → 𝑦 ∈ 𝒫 𝑠)
1413elpwid 4569 . . . . . . . . . . . . 13 (𝑦 ∈ (𝒫 𝑠 ∩ Fin) → 𝑦𝑠)
1514adantl 482 . . . . . . . . . . . 12 (((𝐶 ∈ (Moore‘𝑋) ∧ 𝑠𝐶) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → 𝑦𝑠)
16 simplr 767 . . . . . . . . . . . 12 (((𝐶 ∈ (Moore‘𝑋) ∧ 𝑠𝐶) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → 𝑠𝐶)
17 isacs2.f . . . . . . . . . . . . 13 𝐹 = (mrCls‘𝐶)
1817mrcsscl 17500 . . . . . . . . . . . 12 ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑦𝑠𝑠𝐶) → (𝐹𝑦) ⊆ 𝑠)
1912, 15, 16, 18syl3anc 1371 . . . . . . . . . . 11 (((𝐶 ∈ (Moore‘𝑋) ∧ 𝑠𝐶) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → (𝐹𝑦) ⊆ 𝑠)
2019ralrimiva 3143 . . . . . . . . . 10 ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑠𝐶) → ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠)
2120ad4ant14 750 . . . . . . . . 9 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ 𝑠𝐶) → ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠)
22 fveq2 6842 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑦 → (𝑓𝑧) = (𝑓𝑦))
2322sseq1d 3975 . . . . . . . . . . . . . . 15 (𝑧 = 𝑦 → ((𝑓𝑧) ⊆ (𝐹𝑦) ↔ (𝑓𝑦) ⊆ (𝐹𝑦)))
24 simplll 773 . . . . . . . . . . . . . . . . 17 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → 𝐶 ∈ (Moore‘𝑋))
2514adantl 482 . . . . . . . . . . . . . . . . . 18 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → 𝑦𝑠)
26 elpwi 4567 . . . . . . . . . . . . . . . . . . 19 (𝑠 ∈ 𝒫 𝑋𝑠𝑋)
2726ad2antlr 725 . . . . . . . . . . . . . . . . . 18 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → 𝑠𝑋)
2825, 27sstrd 3954 . . . . . . . . . . . . . . . . 17 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → 𝑦𝑋)
2917mrccl 17491 . . . . . . . . . . . . . . . . 17 ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑦𝑋) → (𝐹𝑦) ∈ 𝐶)
3024, 28, 29syl2anc 584 . . . . . . . . . . . . . . . 16 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → (𝐹𝑦) ∈ 𝐶)
31 eleq1 2825 . . . . . . . . . . . . . . . . . 18 (𝑡 = (𝐹𝑦) → (𝑡𝐶 ↔ (𝐹𝑦) ∈ 𝐶))
32 pweq 4574 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = (𝐹𝑦) → 𝒫 𝑡 = 𝒫 (𝐹𝑦))
3332ineq1d 4171 . . . . . . . . . . . . . . . . . . 19 (𝑡 = (𝐹𝑦) → (𝒫 𝑡 ∩ Fin) = (𝒫 (𝐹𝑦) ∩ Fin))
34 sseq2 3970 . . . . . . . . . . . . . . . . . . 19 (𝑡 = (𝐹𝑦) → ((𝑓𝑧) ⊆ 𝑡 ↔ (𝑓𝑧) ⊆ (𝐹𝑦)))
3533, 34raleqbidv 3319 . . . . . . . . . . . . . . . . . 18 (𝑡 = (𝐹𝑦) → (∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡 ↔ ∀𝑧 ∈ (𝒫 (𝐹𝑦) ∩ Fin)(𝑓𝑧) ⊆ (𝐹𝑦)))
3631, 35bibi12d 345 . . . . . . . . . . . . . . . . 17 (𝑡 = (𝐹𝑦) → ((𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡) ↔ ((𝐹𝑦) ∈ 𝐶 ↔ ∀𝑧 ∈ (𝒫 (𝐹𝑦) ∩ Fin)(𝑓𝑧) ⊆ (𝐹𝑦))))
37 simprr 771 . . . . . . . . . . . . . . . . . 18 ((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) → ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))
3837ad2antrr 724 . . . . . . . . . . . . . . . . 17 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))
39 mresspw 17472 . . . . . . . . . . . . . . . . . . 19 (𝐶 ∈ (Moore‘𝑋) → 𝐶 ⊆ 𝒫 𝑋)
4039ad3antrrr 728 . . . . . . . . . . . . . . . . . 18 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → 𝐶 ⊆ 𝒫 𝑋)
4140, 30sseldd 3945 . . . . . . . . . . . . . . . . 17 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → (𝐹𝑦) ∈ 𝒫 𝑋)
4236, 38, 41rspcdva 3582 . . . . . . . . . . . . . . . 16 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → ((𝐹𝑦) ∈ 𝐶 ↔ ∀𝑧 ∈ (𝒫 (𝐹𝑦) ∩ Fin)(𝑓𝑧) ⊆ (𝐹𝑦)))
4330, 42mpbid 231 . . . . . . . . . . . . . . 15 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → ∀𝑧 ∈ (𝒫 (𝐹𝑦) ∩ Fin)(𝑓𝑧) ⊆ (𝐹𝑦))
4424, 17, 28mrcssidd 17505 . . . . . . . . . . . . . . . . 17 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → 𝑦 ⊆ (𝐹𝑦))
45 vex 3449 . . . . . . . . . . . . . . . . . 18 𝑦 ∈ V
4645elpw 4564 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ 𝒫 (𝐹𝑦) ↔ 𝑦 ⊆ (𝐹𝑦))
4744, 46sylibr 233 . . . . . . . . . . . . . . . 16 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → 𝑦 ∈ 𝒫 (𝐹𝑦))
48 elinel2 4156 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (𝒫 𝑠 ∩ Fin) → 𝑦 ∈ Fin)
4948adantl 482 . . . . . . . . . . . . . . . 16 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → 𝑦 ∈ Fin)
5047, 49elind 4154 . . . . . . . . . . . . . . 15 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → 𝑦 ∈ (𝒫 (𝐹𝑦) ∩ Fin))
5123, 43, 50rspcdva 3582 . . . . . . . . . . . . . 14 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → (𝑓𝑦) ⊆ (𝐹𝑦))
52 sstr2 3951 . . . . . . . . . . . . . 14 ((𝑓𝑦) ⊆ (𝐹𝑦) → ((𝐹𝑦) ⊆ 𝑠 → (𝑓𝑦) ⊆ 𝑠))
5351, 52syl 17 . . . . . . . . . . . . 13 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → ((𝐹𝑦) ⊆ 𝑠 → (𝑓𝑦) ⊆ 𝑠))
5453ralimdva 3164 . . . . . . . . . . . 12 (((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) → (∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠 → ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝑓𝑦) ⊆ 𝑠))
5554imp 407 . . . . . . . . . . 11 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠) → ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝑓𝑦) ⊆ 𝑠)
56 fveq2 6842 . . . . . . . . . . . . 13 (𝑦 = 𝑧 → (𝑓𝑦) = (𝑓𝑧))
5756sseq1d 3975 . . . . . . . . . . . 12 (𝑦 = 𝑧 → ((𝑓𝑦) ⊆ 𝑠 ↔ (𝑓𝑧) ⊆ 𝑠))
5857cbvralvw 3225 . . . . . . . . . . 11 (∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝑓𝑦) ⊆ 𝑠 ↔ ∀𝑧 ∈ (𝒫 𝑠 ∩ Fin)(𝑓𝑧) ⊆ 𝑠)
5955, 58sylib 217 . . . . . . . . . 10 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠) → ∀𝑧 ∈ (𝒫 𝑠 ∩ Fin)(𝑓𝑧) ⊆ 𝑠)
60 eleq1 2825 . . . . . . . . . . . 12 (𝑡 = 𝑠 → (𝑡𝐶𝑠𝐶))
61 pweq 4574 . . . . . . . . . . . . . 14 (𝑡 = 𝑠 → 𝒫 𝑡 = 𝒫 𝑠)
6261ineq1d 4171 . . . . . . . . . . . . 13 (𝑡 = 𝑠 → (𝒫 𝑡 ∩ Fin) = (𝒫 𝑠 ∩ Fin))
63 sseq2 3970 . . . . . . . . . . . . 13 (𝑡 = 𝑠 → ((𝑓𝑧) ⊆ 𝑡 ↔ (𝑓𝑧) ⊆ 𝑠))
6462, 63raleqbidv 3319 . . . . . . . . . . . 12 (𝑡 = 𝑠 → (∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡 ↔ ∀𝑧 ∈ (𝒫 𝑠 ∩ Fin)(𝑓𝑧) ⊆ 𝑠))
6560, 64bibi12d 345 . . . . . . . . . . 11 (𝑡 = 𝑠 → ((𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡) ↔ (𝑠𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑠 ∩ Fin)(𝑓𝑧) ⊆ 𝑠)))
6637ad2antrr 724 . . . . . . . . . . 11 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠) → ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))
67 simplr 767 . . . . . . . . . . 11 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠) → 𝑠 ∈ 𝒫 𝑋)
6865, 66, 67rspcdva 3582 . . . . . . . . . 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 413 . . . . . 6 (𝐶 ∈ (Moore‘𝑋) → ((𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡)) → ∀𝑠 ∈ 𝒫 𝑋(𝑠𝐶 ↔ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠)))
7372exlimdv 1936 . . . . 5 (𝐶 ∈ (Moore‘𝑋) → (∃𝑓(𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡)) → ∀𝑠 ∈ 𝒫 𝑋(𝑠𝐶 ↔ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠)))
7417mrcf 17489 . . . . . . . 8 (𝐶 ∈ (Moore‘𝑋) → 𝐹:𝒫 𝑋𝐶)
7574, 39fssd 6686 . . . . . . 7 (𝐶 ∈ (Moore‘𝑋) → 𝐹:𝒫 𝑋⟶𝒫 𝑋)
7617fvexi 6856 . . . . . . . 8 𝐹 ∈ V
77 feq1 6649 . . . . . . . . 9 (𝑓 = 𝐹 → (𝑓:𝒫 𝑋⟶𝒫 𝑋𝐹:𝒫 𝑋⟶𝒫 𝑋))
78 fveq1 6841 . . . . . . . . . . . . . . 15 (𝑓 = 𝐹 → (𝑓𝑧) = (𝐹𝑧))
7978sseq1d 3975 . . . . . . . . . . . . . 14 (𝑓 = 𝐹 → ((𝑓𝑧) ⊆ 𝑡 ↔ (𝐹𝑧) ⊆ 𝑡))
8079ralbidv 3174 . . . . . . . . . . . . 13 (𝑓 = 𝐹 → (∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝐹𝑧) ⊆ 𝑡))
81 fveq2 6842 . . . . . . . . . . . . . . 15 (𝑧 = 𝑦 → (𝐹𝑧) = (𝐹𝑦))
8281sseq1d 3975 . . . . . . . . . . . . . 14 (𝑧 = 𝑦 → ((𝐹𝑧) ⊆ 𝑡 ↔ (𝐹𝑦) ⊆ 𝑡))
8382cbvralvw 3225 . . . . . . . . . . . . 13 (∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝐹𝑧) ⊆ 𝑡 ↔ ∀𝑦 ∈ (𝒫 𝑡 ∩ Fin)(𝐹𝑦) ⊆ 𝑡)
8480, 83bitrdi 286 . . . . . . . . . . . 12 (𝑓 = 𝐹 → (∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡 ↔ ∀𝑦 ∈ (𝒫 𝑡 ∩ Fin)(𝐹𝑦) ⊆ 𝑡))
8584bibi2d 342 . . . . . . . . . . 11 (𝑓 = 𝐹 → ((𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡) ↔ (𝑡𝐶 ↔ ∀𝑦 ∈ (𝒫 𝑡 ∩ Fin)(𝐹𝑦) ⊆ 𝑡)))
8685ralbidv 3174 . . . . . . . . . 10 (𝑓 = 𝐹 → (∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡) ↔ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑦 ∈ (𝒫 𝑡 ∩ Fin)(𝐹𝑦) ⊆ 𝑡)))
87 sseq2 3970 . . . . . . . . . . . . 13 (𝑡 = 𝑠 → ((𝐹𝑦) ⊆ 𝑡 ↔ (𝐹𝑦) ⊆ 𝑠))
8862, 87raleqbidv 3319 . . . . . . . . . . . 12 (𝑡 = 𝑠 → (∀𝑦 ∈ (𝒫 𝑡 ∩ Fin)(𝐹𝑦) ⊆ 𝑡 ↔ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠))
8960, 88bibi12d 345 . . . . . . . . . . 11 (𝑡 = 𝑠 → ((𝑡𝐶 ↔ ∀𝑦 ∈ (𝒫 𝑡 ∩ Fin)(𝐹𝑦) ⊆ 𝑡) ↔ (𝑠𝐶 ↔ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠)))
9089cbvralvw 3225 . . . . . . . . . 10 (∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑦 ∈ (𝒫 𝑡 ∩ Fin)(𝐹𝑦) ⊆ 𝑡) ↔ ∀𝑠 ∈ 𝒫 𝑋(𝑠𝐶 ↔ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠))
9186, 90bitrdi 286 . . . . . . . . 9 (𝑓 = 𝐹 → (∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡) ↔ ∀𝑠 ∈ 𝒫 𝑋(𝑠𝐶 ↔ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠)))
9277, 91anbi12d 631 . . . . . . . 8 (𝑓 = 𝐹 → ((𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡)) ↔ (𝐹:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑠 ∈ 𝒫 𝑋(𝑠𝐶 ↔ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠))))
9376, 92spcev 3565 . . . . . . 7 ((𝐹:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑠 ∈ 𝒫 𝑋(𝑠𝐶 ↔ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠)) → ∃𝑓(𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡)))
9475, 93sylan 580 . . . . . 6 ((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝑋(𝑠𝐶 ↔ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠)) → ∃𝑓(𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡)))
9594ex 413 . . . . 5 (𝐶 ∈ (Moore‘𝑋) → (∀𝑠 ∈ 𝒫 𝑋(𝑠𝐶 ↔ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠) → ∃𝑓(𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))))
9673, 95impbid 211 . . . 4 (𝐶 ∈ (Moore‘𝑋) → (∃𝑓(𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡)) ↔ ∀𝑠 ∈ 𝒫 𝑋(𝑠𝐶 ↔ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠)))
9711, 96bitrid 282 . . 3 (𝐶 ∈ (Moore‘𝑋) → (∃𝑓(𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 (𝑓 “ (𝒫 𝑡 ∩ Fin)) ⊆ 𝑡)) ↔ ∀𝑠 ∈ 𝒫 𝑋(𝑠𝐶 ↔ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠)))
9897pm5.32i 575 . 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 396   = wceq 1541  wex 1781  wcel 2106  wral 3064  cin 3909  wss 3910  𝒫 cpw 4560   cuni 4865   ciun 4954  cima 5636  Fun wfun 6490  wf 6492  cfv 6496  Fincfn 8883  Moorecmre 17462  mrClscmrc 17463  ACScacs 17465
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-id 5531  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-fv 6504  df-mre 17466  df-mrc 17467  df-acs 17469
This theorem is referenced by:  acsfiel  17534  isacs5  18437
  Copyright terms: Public domain W3C validator