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

Theorem isacs2 16235
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 16233 . 2 (𝐶 ∈ (ACS‘𝑋) ↔ (𝐶 ∈ (Moore‘𝑋) ∧ ∃𝑓(𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 (𝑓 “ (𝒫 𝑡 ∩ Fin)) ⊆ 𝑡))))
2 iunss 4527 . . . . . . . . 9 ( 𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡)
3 ffun 6005 . . . . . . . . . . 11 (𝑓:𝒫 𝑋⟶𝒫 𝑋 → Fun 𝑓)
4 funiunfv 6460 . . . . . . . . . . 11 (Fun 𝑓 𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) = (𝑓 “ (𝒫 𝑡 ∩ Fin)))
53, 4syl 17 . . . . . . . . . 10 (𝑓:𝒫 𝑋⟶𝒫 𝑋 𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) = (𝑓 “ (𝒫 𝑡 ∩ Fin)))
65sseq1d 3611 . . . . . . . . 9 (𝑓:𝒫 𝑋⟶𝒫 𝑋 → ( 𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡 (𝑓 “ (𝒫 𝑡 ∩ Fin)) ⊆ 𝑡))
72, 6syl5rbbr 275 . . . . . . . 8 (𝑓:𝒫 𝑋⟶𝒫 𝑋 → ( (𝑓 “ (𝒫 𝑡 ∩ Fin)) ⊆ 𝑡 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))
87bibi2d 332 . . . . . . 7 (𝑓:𝒫 𝑋⟶𝒫 𝑋 → ((𝑡𝐶 (𝑓 “ (𝒫 𝑡 ∩ Fin)) ⊆ 𝑡) ↔ (𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡)))
98ralbidv 2980 . . . . . 6 (𝑓:𝒫 𝑋⟶𝒫 𝑋 → (∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 (𝑓 “ (𝒫 𝑡 ∩ Fin)) ⊆ 𝑡) ↔ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡)))
109pm5.32i 668 . . . . 5 ((𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 (𝑓 “ (𝒫 𝑡 ∩ Fin)) ⊆ 𝑡)) ↔ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡)))
1110exbii 1771 . . . 4 (∃𝑓(𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 (𝑓 “ (𝒫 𝑡 ∩ Fin)) ⊆ 𝑡)) ↔ ∃𝑓(𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡)))
12 simpll 789 . . . . . . . . . . . . 13 (((𝐶 ∈ (Moore‘𝑋) ∧ 𝑠𝐶) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → 𝐶 ∈ (Moore‘𝑋))
13 inss1 3811 . . . . . . . . . . . . . . . 16 (𝒫 𝑠 ∩ Fin) ⊆ 𝒫 𝑠
1413sseli 3579 . . . . . . . . . . . . . . 15 (𝑦 ∈ (𝒫 𝑠 ∩ Fin) → 𝑦 ∈ 𝒫 𝑠)
15 elpwi 4140 . . . . . . . . . . . . . . 15 (𝑦 ∈ 𝒫 𝑠𝑦𝑠)
1614, 15syl 17 . . . . . . . . . . . . . 14 (𝑦 ∈ (𝒫 𝑠 ∩ Fin) → 𝑦𝑠)
1716adantl 482 . . . . . . . . . . . . 13 (((𝐶 ∈ (Moore‘𝑋) ∧ 𝑠𝐶) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → 𝑦𝑠)
18 simplr 791 . . . . . . . . . . . . 13 (((𝐶 ∈ (Moore‘𝑋) ∧ 𝑠𝐶) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → 𝑠𝐶)
19 isacs2.f . . . . . . . . . . . . . 14 𝐹 = (mrCls‘𝐶)
2019mrcsscl 16201 . . . . . . . . . . . . 13 ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑦𝑠𝑠𝐶) → (𝐹𝑦) ⊆ 𝑠)
2112, 17, 18, 20syl3anc 1323 . . . . . . . . . . . 12 (((𝐶 ∈ (Moore‘𝑋) ∧ 𝑠𝐶) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → (𝐹𝑦) ⊆ 𝑠)
2221ralrimiva 2960 . . . . . . . . . . 11 ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑠𝐶) → ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠)
2322adantlr 750 . . . . . . . . . 10 (((𝐶 ∈ (Moore‘𝑋) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ 𝑠𝐶) → ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠)
2423adantllr 754 . . . . . . . . 9 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ 𝑠𝐶) → ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠)
25 simplll 797 . . . . . . . . . . . . . . . . . 18 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → 𝐶 ∈ (Moore‘𝑋))
2616adantl 482 . . . . . . . . . . . . . . . . . . 19 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → 𝑦𝑠)
27 elpwi 4140 . . . . . . . . . . . . . . . . . . . 20 (𝑠 ∈ 𝒫 𝑋𝑠𝑋)
2827ad2antlr 762 . . . . . . . . . . . . . . . . . . 19 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → 𝑠𝑋)
2926, 28sstrd 3593 . . . . . . . . . . . . . . . . . 18 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → 𝑦𝑋)
3025, 19, 29mrcssidd 16206 . . . . . . . . . . . . . . . . 17 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → 𝑦 ⊆ (𝐹𝑦))
31 vex 3189 . . . . . . . . . . . . . . . . . 18 𝑦 ∈ V
3231elpw 4136 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ 𝒫 (𝐹𝑦) ↔ 𝑦 ⊆ (𝐹𝑦))
3330, 32sylibr 224 . . . . . . . . . . . . . . . 16 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → 𝑦 ∈ 𝒫 (𝐹𝑦))
34 inss2 3812 . . . . . . . . . . . . . . . . . 18 (𝒫 𝑠 ∩ Fin) ⊆ Fin
3534sseli 3579 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (𝒫 𝑠 ∩ Fin) → 𝑦 ∈ Fin)
3635adantl 482 . . . . . . . . . . . . . . . 16 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → 𝑦 ∈ Fin)
3733, 36elind 3776 . . . . . . . . . . . . . . 15 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → 𝑦 ∈ (𝒫 (𝐹𝑦) ∩ Fin))
3819mrccl 16192 . . . . . . . . . . . . . . . . 17 ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑦𝑋) → (𝐹𝑦) ∈ 𝐶)
3925, 29, 38syl2anc 692 . . . . . . . . . . . . . . . 16 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → (𝐹𝑦) ∈ 𝐶)
40 mresspw 16173 . . . . . . . . . . . . . . . . . . 19 (𝐶 ∈ (Moore‘𝑋) → 𝐶 ⊆ 𝒫 𝑋)
4140ad3antrrr 765 . . . . . . . . . . . . . . . . . 18 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → 𝐶 ⊆ 𝒫 𝑋)
4241, 39sseldd 3584 . . . . . . . . . . . . . . . . 17 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → (𝐹𝑦) ∈ 𝒫 𝑋)
43 simprr 795 . . . . . . . . . . . . . . . . . 18 ((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) → ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))
4443ad2antrr 761 . . . . . . . . . . . . . . . . 17 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))
45 eleq1 2686 . . . . . . . . . . . . . . . . . . 19 (𝑡 = (𝐹𝑦) → (𝑡𝐶 ↔ (𝐹𝑦) ∈ 𝐶))
46 pweq 4133 . . . . . . . . . . . . . . . . . . . . 21 (𝑡 = (𝐹𝑦) → 𝒫 𝑡 = 𝒫 (𝐹𝑦))
4746ineq1d 3791 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = (𝐹𝑦) → (𝒫 𝑡 ∩ Fin) = (𝒫 (𝐹𝑦) ∩ Fin))
48 sseq2 3606 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = (𝐹𝑦) → ((𝑓𝑧) ⊆ 𝑡 ↔ (𝑓𝑧) ⊆ (𝐹𝑦)))
4947, 48raleqbidv 3141 . . . . . . . . . . . . . . . . . . 19 (𝑡 = (𝐹𝑦) → (∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡 ↔ ∀𝑧 ∈ (𝒫 (𝐹𝑦) ∩ Fin)(𝑓𝑧) ⊆ (𝐹𝑦)))
5045, 49bibi12d 335 . . . . . . . . . . . . . . . . . 18 (𝑡 = (𝐹𝑦) → ((𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡) ↔ ((𝐹𝑦) ∈ 𝐶 ↔ ∀𝑧 ∈ (𝒫 (𝐹𝑦) ∩ Fin)(𝑓𝑧) ⊆ (𝐹𝑦))))
5150rspcva 3293 . . . . . . . . . . . . . . . . 17 (((𝐹𝑦) ∈ 𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡)) → ((𝐹𝑦) ∈ 𝐶 ↔ ∀𝑧 ∈ (𝒫 (𝐹𝑦) ∩ Fin)(𝑓𝑧) ⊆ (𝐹𝑦)))
5242, 44, 51syl2anc 692 . . . . . . . . . . . . . . . 16 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → ((𝐹𝑦) ∈ 𝐶 ↔ ∀𝑧 ∈ (𝒫 (𝐹𝑦) ∩ Fin)(𝑓𝑧) ⊆ (𝐹𝑦)))
5339, 52mpbid 222 . . . . . . . . . . . . . . 15 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → ∀𝑧 ∈ (𝒫 (𝐹𝑦) ∩ Fin)(𝑓𝑧) ⊆ (𝐹𝑦))
54 fveq2 6148 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑦 → (𝑓𝑧) = (𝑓𝑦))
5554sseq1d 3611 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑦 → ((𝑓𝑧) ⊆ (𝐹𝑦) ↔ (𝑓𝑦) ⊆ (𝐹𝑦)))
5655rspcva 3293 . . . . . . . . . . . . . . 15 ((𝑦 ∈ (𝒫 (𝐹𝑦) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐹𝑦) ∩ Fin)(𝑓𝑧) ⊆ (𝐹𝑦)) → (𝑓𝑦) ⊆ (𝐹𝑦))
5737, 53, 56syl2anc 692 . . . . . . . . . . . . . 14 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → (𝑓𝑦) ⊆ (𝐹𝑦))
58 sstr2 3590 . . . . . . . . . . . . . 14 ((𝑓𝑦) ⊆ (𝐹𝑦) → ((𝐹𝑦) ⊆ 𝑠 → (𝑓𝑦) ⊆ 𝑠))
5957, 58syl 17 . . . . . . . . . . . . 13 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → ((𝐹𝑦) ⊆ 𝑠 → (𝑓𝑦) ⊆ 𝑠))
6059ralimdva 2956 . . . . . . . . . . . 12 (((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) → (∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠 → ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝑓𝑦) ⊆ 𝑠))
6160imp 445 . . . . . . . . . . 11 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠) → ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝑓𝑦) ⊆ 𝑠)
62 fveq2 6148 . . . . . . . . . . . . 13 (𝑦 = 𝑧 → (𝑓𝑦) = (𝑓𝑧))
6362sseq1d 3611 . . . . . . . . . . . 12 (𝑦 = 𝑧 → ((𝑓𝑦) ⊆ 𝑠 ↔ (𝑓𝑧) ⊆ 𝑠))
6463cbvralv 3159 . . . . . . . . . . 11 (∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝑓𝑦) ⊆ 𝑠 ↔ ∀𝑧 ∈ (𝒫 𝑠 ∩ Fin)(𝑓𝑧) ⊆ 𝑠)
6561, 64sylib 208 . . . . . . . . . 10 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠) → ∀𝑧 ∈ (𝒫 𝑠 ∩ Fin)(𝑓𝑧) ⊆ 𝑠)
66 simplr 791 . . . . . . . . . . 11 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠) → 𝑠 ∈ 𝒫 𝑋)
6743ad2antrr 761 . . . . . . . . . . 11 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠) → ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))
68 eleq1 2686 . . . . . . . . . . . . 13 (𝑡 = 𝑠 → (𝑡𝐶𝑠𝐶))
69 pweq 4133 . . . . . . . . . . . . . . 15 (𝑡 = 𝑠 → 𝒫 𝑡 = 𝒫 𝑠)
7069ineq1d 3791 . . . . . . . . . . . . . 14 (𝑡 = 𝑠 → (𝒫 𝑡 ∩ Fin) = (𝒫 𝑠 ∩ Fin))
71 sseq2 3606 . . . . . . . . . . . . . 14 (𝑡 = 𝑠 → ((𝑓𝑧) ⊆ 𝑡 ↔ (𝑓𝑧) ⊆ 𝑠))
7270, 71raleqbidv 3141 . . . . . . . . . . . . 13 (𝑡 = 𝑠 → (∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡 ↔ ∀𝑧 ∈ (𝒫 𝑠 ∩ Fin)(𝑓𝑧) ⊆ 𝑠))
7368, 72bibi12d 335 . . . . . . . . . . . 12 (𝑡 = 𝑠 → ((𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡) ↔ (𝑠𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑠 ∩ Fin)(𝑓𝑧) ⊆ 𝑠)))
7473rspcva 3293 . . . . . . . . . . 11 ((𝑠 ∈ 𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡)) → (𝑠𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑠 ∩ Fin)(𝑓𝑧) ⊆ 𝑠))
7566, 67, 74syl2anc 692 . . . . . . . . . 10 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠) → (𝑠𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑠 ∩ Fin)(𝑓𝑧) ⊆ 𝑠))
7665, 75mpbird 247 . . . . . . . . 9 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠) → 𝑠𝐶)
7724, 76impbida 876 . . . . . . . 8 (((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) → (𝑠𝐶 ↔ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠))
7877ralrimiva 2960 . . . . . . 7 ((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) → ∀𝑠 ∈ 𝒫 𝑋(𝑠𝐶 ↔ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠))
7978ex 450 . . . . . 6 (𝐶 ∈ (Moore‘𝑋) → ((𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡)) → ∀𝑠 ∈ 𝒫 𝑋(𝑠𝐶 ↔ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠)))
8079exlimdv 1858 . . . . 5 (𝐶 ∈ (Moore‘𝑋) → (∃𝑓(𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡)) → ∀𝑠 ∈ 𝒫 𝑋(𝑠𝐶 ↔ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠)))
8119mrcf 16190 . . . . . . . 8 (𝐶 ∈ (Moore‘𝑋) → 𝐹:𝒫 𝑋𝐶)
8281, 40fssd 6014 . . . . . . 7 (𝐶 ∈ (Moore‘𝑋) → 𝐹:𝒫 𝑋⟶𝒫 𝑋)
83 fvex 6158 . . . . . . . . 9 (mrCls‘𝐶) ∈ V
8419, 83eqeltri 2694 . . . . . . . 8 𝐹 ∈ V
85 feq1 5983 . . . . . . . . 9 (𝑓 = 𝐹 → (𝑓:𝒫 𝑋⟶𝒫 𝑋𝐹:𝒫 𝑋⟶𝒫 𝑋))
86 fveq1 6147 . . . . . . . . . . . . . . 15 (𝑓 = 𝐹 → (𝑓𝑧) = (𝐹𝑧))
8786sseq1d 3611 . . . . . . . . . . . . . 14 (𝑓 = 𝐹 → ((𝑓𝑧) ⊆ 𝑡 ↔ (𝐹𝑧) ⊆ 𝑡))
8887ralbidv 2980 . . . . . . . . . . . . 13 (𝑓 = 𝐹 → (∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝐹𝑧) ⊆ 𝑡))
89 fveq2 6148 . . . . . . . . . . . . . . 15 (𝑧 = 𝑦 → (𝐹𝑧) = (𝐹𝑦))
9089sseq1d 3611 . . . . . . . . . . . . . 14 (𝑧 = 𝑦 → ((𝐹𝑧) ⊆ 𝑡 ↔ (𝐹𝑦) ⊆ 𝑡))
9190cbvralv 3159 . . . . . . . . . . . . 13 (∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝐹𝑧) ⊆ 𝑡 ↔ ∀𝑦 ∈ (𝒫 𝑡 ∩ Fin)(𝐹𝑦) ⊆ 𝑡)
9288, 91syl6bb 276 . . . . . . . . . . . 12 (𝑓 = 𝐹 → (∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡 ↔ ∀𝑦 ∈ (𝒫 𝑡 ∩ Fin)(𝐹𝑦) ⊆ 𝑡))
9392bibi2d 332 . . . . . . . . . . 11 (𝑓 = 𝐹 → ((𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡) ↔ (𝑡𝐶 ↔ ∀𝑦 ∈ (𝒫 𝑡 ∩ Fin)(𝐹𝑦) ⊆ 𝑡)))
9493ralbidv 2980 . . . . . . . . . 10 (𝑓 = 𝐹 → (∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡) ↔ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑦 ∈ (𝒫 𝑡 ∩ Fin)(𝐹𝑦) ⊆ 𝑡)))
95 sseq2 3606 . . . . . . . . . . . . 13 (𝑡 = 𝑠 → ((𝐹𝑦) ⊆ 𝑡 ↔ (𝐹𝑦) ⊆ 𝑠))
9670, 95raleqbidv 3141 . . . . . . . . . . . 12 (𝑡 = 𝑠 → (∀𝑦 ∈ (𝒫 𝑡 ∩ Fin)(𝐹𝑦) ⊆ 𝑡 ↔ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠))
9768, 96bibi12d 335 . . . . . . . . . . 11 (𝑡 = 𝑠 → ((𝑡𝐶 ↔ ∀𝑦 ∈ (𝒫 𝑡 ∩ Fin)(𝐹𝑦) ⊆ 𝑡) ↔ (𝑠𝐶 ↔ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠)))
9897cbvralv 3159 . . . . . . . . . 10 (∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑦 ∈ (𝒫 𝑡 ∩ Fin)(𝐹𝑦) ⊆ 𝑡) ↔ ∀𝑠 ∈ 𝒫 𝑋(𝑠𝐶 ↔ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠))
9994, 98syl6bb 276 . . . . . . . . 9 (𝑓 = 𝐹 → (∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡) ↔ ∀𝑠 ∈ 𝒫 𝑋(𝑠𝐶 ↔ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠)))
10085, 99anbi12d 746 . . . . . . . 8 (𝑓 = 𝐹 → ((𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡)) ↔ (𝐹:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑠 ∈ 𝒫 𝑋(𝑠𝐶 ↔ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠))))
10184, 100spcev 3286 . . . . . . 7 ((𝐹:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑠 ∈ 𝒫 𝑋(𝑠𝐶 ↔ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠)) → ∃𝑓(𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡)))
10282, 101sylan 488 . . . . . 6 ((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝑋(𝑠𝐶 ↔ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠)) → ∃𝑓(𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡)))
103102ex 450 . . . . 5 (𝐶 ∈ (Moore‘𝑋) → (∀𝑠 ∈ 𝒫 𝑋(𝑠𝐶 ↔ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠) → ∃𝑓(𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))))
10480, 103impbid 202 . . . 4 (𝐶 ∈ (Moore‘𝑋) → (∃𝑓(𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡)) ↔ ∀𝑠 ∈ 𝒫 𝑋(𝑠𝐶 ↔ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠)))
10511, 104syl5bb 272 . . 3 (𝐶 ∈ (Moore‘𝑋) → (∃𝑓(𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 (𝑓 “ (𝒫 𝑡 ∩ Fin)) ⊆ 𝑡)) ↔ ∀𝑠 ∈ 𝒫 𝑋(𝑠𝐶 ↔ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠)))
106105pm5.32i 668 . 2 ((𝐶 ∈ (Moore‘𝑋) ∧ ∃𝑓(𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 (𝑓 “ (𝒫 𝑡 ∩ Fin)) ⊆ 𝑡))) ↔ (𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝑋(𝑠𝐶 ↔ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠)))
1071, 106bitri 264 1 (𝐶 ∈ (ACS‘𝑋) ↔ (𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝑋(𝑠𝐶 ↔ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384   = wceq 1480  wex 1701  wcel 1987  wral 2907  Vcvv 3186  cin 3554  wss 3555  𝒫 cpw 4130   cuni 4402   ciun 4485  cima 5077  Fun wfun 5841  wf 5843  cfv 5847  Fincfn 7899  Moorecmre 16163  mrClscmrc 16164  ACScacs 16166
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4741  ax-nul 4749  ax-pow 4803  ax-pr 4867  ax-un 6902
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-rab 2916  df-v 3188  df-sbc 3418  df-csb 3515  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-nul 3892  df-if 4059  df-pw 4132  df-sn 4149  df-pr 4151  df-op 4155  df-uni 4403  df-int 4441  df-iun 4487  df-br 4614  df-opab 4674  df-mpt 4675  df-id 4989  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-rn 5085  df-res 5086  df-ima 5087  df-iota 5810  df-fun 5849  df-fn 5850  df-f 5851  df-fv 5855  df-mre 16167  df-mrc 16168  df-acs 16170
This theorem is referenced by:  acsfiel  16236  isacs5  17093
  Copyright terms: Public domain W3C validator