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

Theorem isacs2 16582
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 16580 . 2 (𝐶 ∈ (ACS‘𝑋) ↔ (𝐶 ∈ (Moore‘𝑋) ∧ ∃𝑓(𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 (𝑓 “ (𝒫 𝑡 ∩ Fin)) ⊆ 𝑡))))
2 iunss 4719 . . . . . . . . 9 ( 𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡)
3 ffun 6228 . . . . . . . . . . 11 (𝑓:𝒫 𝑋⟶𝒫 𝑋 → Fun 𝑓)
4 funiunfv 6700 . . . . . . . . . . 11 (Fun 𝑓 𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) = (𝑓 “ (𝒫 𝑡 ∩ Fin)))
53, 4syl 17 . . . . . . . . . 10 (𝑓:𝒫 𝑋⟶𝒫 𝑋 𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) = (𝑓 “ (𝒫 𝑡 ∩ Fin)))
65sseq1d 3794 . . . . . . . . 9 (𝑓:𝒫 𝑋⟶𝒫 𝑋 → ( 𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡 (𝑓 “ (𝒫 𝑡 ∩ Fin)) ⊆ 𝑡))
72, 6syl5rbbr 277 . . . . . . . 8 (𝑓:𝒫 𝑋⟶𝒫 𝑋 → ( (𝑓 “ (𝒫 𝑡 ∩ Fin)) ⊆ 𝑡 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))
87bibi2d 333 . . . . . . 7 (𝑓:𝒫 𝑋⟶𝒫 𝑋 → ((𝑡𝐶 (𝑓 “ (𝒫 𝑡 ∩ Fin)) ⊆ 𝑡) ↔ (𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡)))
98ralbidv 3133 . . . . . 6 (𝑓:𝒫 𝑋⟶𝒫 𝑋 → (∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 (𝑓 “ (𝒫 𝑡 ∩ Fin)) ⊆ 𝑡) ↔ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡)))
109pm5.32i 570 . . . . 5 ((𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 (𝑓 “ (𝒫 𝑡 ∩ Fin)) ⊆ 𝑡)) ↔ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡)))
1110exbii 1943 . . . 4 (∃𝑓(𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 (𝑓 “ (𝒫 𝑡 ∩ Fin)) ⊆ 𝑡)) ↔ ∃𝑓(𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡)))
12 simpll 783 . . . . . . . . . . . . 13 (((𝐶 ∈ (Moore‘𝑋) ∧ 𝑠𝐶) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → 𝐶 ∈ (Moore‘𝑋))
13 inss1 3994 . . . . . . . . . . . . . . . 16 (𝒫 𝑠 ∩ Fin) ⊆ 𝒫 𝑠
1413sseli 3759 . . . . . . . . . . . . . . 15 (𝑦 ∈ (𝒫 𝑠 ∩ Fin) → 𝑦 ∈ 𝒫 𝑠)
15 elpwi 4327 . . . . . . . . . . . . . . 15 (𝑦 ∈ 𝒫 𝑠𝑦𝑠)
1614, 15syl 17 . . . . . . . . . . . . . 14 (𝑦 ∈ (𝒫 𝑠 ∩ Fin) → 𝑦𝑠)
1716adantl 473 . . . . . . . . . . . . 13 (((𝐶 ∈ (Moore‘𝑋) ∧ 𝑠𝐶) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → 𝑦𝑠)
18 simplr 785 . . . . . . . . . . . . 13 (((𝐶 ∈ (Moore‘𝑋) ∧ 𝑠𝐶) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → 𝑠𝐶)
19 isacs2.f . . . . . . . . . . . . . 14 𝐹 = (mrCls‘𝐶)
2019mrcsscl 16549 . . . . . . . . . . . . 13 ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑦𝑠𝑠𝐶) → (𝐹𝑦) ⊆ 𝑠)
2112, 17, 18, 20syl3anc 1490 . . . . . . . . . . . 12 (((𝐶 ∈ (Moore‘𝑋) ∧ 𝑠𝐶) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → (𝐹𝑦) ⊆ 𝑠)
2221ralrimiva 3113 . . . . . . . . . . 11 ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑠𝐶) → ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠)
2322adantlr 706 . . . . . . . . . 10 (((𝐶 ∈ (Moore‘𝑋) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ 𝑠𝐶) → ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠)
2423adantllr 710 . . . . . . . . 9 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ 𝑠𝐶) → ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠)
25 fveq2 6377 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑦 → (𝑓𝑧) = (𝑓𝑦))
2625sseq1d 3794 . . . . . . . . . . . . . . 15 (𝑧 = 𝑦 → ((𝑓𝑧) ⊆ (𝐹𝑦) ↔ (𝑓𝑦) ⊆ (𝐹𝑦)))
27 simplll 791 . . . . . . . . . . . . . . . . 17 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → 𝐶 ∈ (Moore‘𝑋))
2816adantl 473 . . . . . . . . . . . . . . . . . 18 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → 𝑦𝑠)
29 elpwi 4327 . . . . . . . . . . . . . . . . . . 19 (𝑠 ∈ 𝒫 𝑋𝑠𝑋)
3029ad2antlr 718 . . . . . . . . . . . . . . . . . 18 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → 𝑠𝑋)
3128, 30sstrd 3773 . . . . . . . . . . . . . . . . 17 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → 𝑦𝑋)
3219mrccl 16540 . . . . . . . . . . . . . . . . 17 ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑦𝑋) → (𝐹𝑦) ∈ 𝐶)
3327, 31, 32syl2anc 579 . . . . . . . . . . . . . . . 16 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → (𝐹𝑦) ∈ 𝐶)
34 eleq1 2832 . . . . . . . . . . . . . . . . . 18 (𝑡 = (𝐹𝑦) → (𝑡𝐶 ↔ (𝐹𝑦) ∈ 𝐶))
35 pweq 4320 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = (𝐹𝑦) → 𝒫 𝑡 = 𝒫 (𝐹𝑦))
3635ineq1d 3977 . . . . . . . . . . . . . . . . . . 19 (𝑡 = (𝐹𝑦) → (𝒫 𝑡 ∩ Fin) = (𝒫 (𝐹𝑦) ∩ Fin))
37 sseq2 3789 . . . . . . . . . . . . . . . . . . 19 (𝑡 = (𝐹𝑦) → ((𝑓𝑧) ⊆ 𝑡 ↔ (𝑓𝑧) ⊆ (𝐹𝑦)))
3836, 37raleqbidv 3300 . . . . . . . . . . . . . . . . . 18 (𝑡 = (𝐹𝑦) → (∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡 ↔ ∀𝑧 ∈ (𝒫 (𝐹𝑦) ∩ Fin)(𝑓𝑧) ⊆ (𝐹𝑦)))
3934, 38bibi12d 336 . . . . . . . . . . . . . . . . 17 (𝑡 = (𝐹𝑦) → ((𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡) ↔ ((𝐹𝑦) ∈ 𝐶 ↔ ∀𝑧 ∈ (𝒫 (𝐹𝑦) ∩ Fin)(𝑓𝑧) ⊆ (𝐹𝑦))))
40 simprr 789 . . . . . . . . . . . . . . . . . 18 ((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) → ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))
4140ad2antrr 717 . . . . . . . . . . . . . . . . 17 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))
42 mresspw 16521 . . . . . . . . . . . . . . . . . . 19 (𝐶 ∈ (Moore‘𝑋) → 𝐶 ⊆ 𝒫 𝑋)
4342ad3antrrr 721 . . . . . . . . . . . . . . . . . 18 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → 𝐶 ⊆ 𝒫 𝑋)
4443, 33sseldd 3764 . . . . . . . . . . . . . . . . 17 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → (𝐹𝑦) ∈ 𝒫 𝑋)
4539, 41, 44rspcdva 3468 . . . . . . . . . . . . . . . 16 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → ((𝐹𝑦) ∈ 𝐶 ↔ ∀𝑧 ∈ (𝒫 (𝐹𝑦) ∩ Fin)(𝑓𝑧) ⊆ (𝐹𝑦)))
4633, 45mpbid 223 . . . . . . . . . . . . . . 15 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → ∀𝑧 ∈ (𝒫 (𝐹𝑦) ∩ Fin)(𝑓𝑧) ⊆ (𝐹𝑦))
4727, 19, 31mrcssidd 16554 . . . . . . . . . . . . . . . . 17 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → 𝑦 ⊆ (𝐹𝑦))
48 vex 3353 . . . . . . . . . . . . . . . . . 18 𝑦 ∈ V
4948elpw 4323 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ 𝒫 (𝐹𝑦) ↔ 𝑦 ⊆ (𝐹𝑦))
5047, 49sylibr 225 . . . . . . . . . . . . . . . 16 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → 𝑦 ∈ 𝒫 (𝐹𝑦))
51 inss2 3995 . . . . . . . . . . . . . . . . . 18 (𝒫 𝑠 ∩ Fin) ⊆ Fin
5251sseli 3759 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (𝒫 𝑠 ∩ Fin) → 𝑦 ∈ Fin)
5352adantl 473 . . . . . . . . . . . . . . . 16 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → 𝑦 ∈ Fin)
5450, 53elind 3962 . . . . . . . . . . . . . . 15 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → 𝑦 ∈ (𝒫 (𝐹𝑦) ∩ Fin))
5526, 46, 54rspcdva 3468 . . . . . . . . . . . . . 14 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → (𝑓𝑦) ⊆ (𝐹𝑦))
56 sstr2 3770 . . . . . . . . . . . . . 14 ((𝑓𝑦) ⊆ (𝐹𝑦) → ((𝐹𝑦) ⊆ 𝑠 → (𝑓𝑦) ⊆ 𝑠))
5755, 56syl 17 . . . . . . . . . . . . 13 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → ((𝐹𝑦) ⊆ 𝑠 → (𝑓𝑦) ⊆ 𝑠))
5857ralimdva 3109 . . . . . . . . . . . 12 (((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) → (∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠 → ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝑓𝑦) ⊆ 𝑠))
5958imp 395 . . . . . . . . . . 11 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠) → ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝑓𝑦) ⊆ 𝑠)
60 fveq2 6377 . . . . . . . . . . . . 13 (𝑦 = 𝑧 → (𝑓𝑦) = (𝑓𝑧))
6160sseq1d 3794 . . . . . . . . . . . 12 (𝑦 = 𝑧 → ((𝑓𝑦) ⊆ 𝑠 ↔ (𝑓𝑧) ⊆ 𝑠))
6261cbvralv 3319 . . . . . . . . . . 11 (∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝑓𝑦) ⊆ 𝑠 ↔ ∀𝑧 ∈ (𝒫 𝑠 ∩ Fin)(𝑓𝑧) ⊆ 𝑠)
6359, 62sylib 209 . . . . . . . . . 10 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠) → ∀𝑧 ∈ (𝒫 𝑠 ∩ Fin)(𝑓𝑧) ⊆ 𝑠)
64 eleq1 2832 . . . . . . . . . . . 12 (𝑡 = 𝑠 → (𝑡𝐶𝑠𝐶))
65 pweq 4320 . . . . . . . . . . . . . 14 (𝑡 = 𝑠 → 𝒫 𝑡 = 𝒫 𝑠)
6665ineq1d 3977 . . . . . . . . . . . . 13 (𝑡 = 𝑠 → (𝒫 𝑡 ∩ Fin) = (𝒫 𝑠 ∩ Fin))
67 sseq2 3789 . . . . . . . . . . . . 13 (𝑡 = 𝑠 → ((𝑓𝑧) ⊆ 𝑡 ↔ (𝑓𝑧) ⊆ 𝑠))
6866, 67raleqbidv 3300 . . . . . . . . . . . 12 (𝑡 = 𝑠 → (∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡 ↔ ∀𝑧 ∈ (𝒫 𝑠 ∩ Fin)(𝑓𝑧) ⊆ 𝑠))
6964, 68bibi12d 336 . . . . . . . . . . 11 (𝑡 = 𝑠 → ((𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡) ↔ (𝑠𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑠 ∩ Fin)(𝑓𝑧) ⊆ 𝑠)))
7040ad2antrr 717 . . . . . . . . . . 11 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠) → ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))
71 simplr 785 . . . . . . . . . . 11 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠) → 𝑠 ∈ 𝒫 𝑋)
7269, 70, 71rspcdva 3468 . . . . . . . . . 10 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠) → (𝑠𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑠 ∩ Fin)(𝑓𝑧) ⊆ 𝑠))
7363, 72mpbird 248 . . . . . . . . 9 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠) → 𝑠𝐶)
7424, 73impbida 835 . . . . . . . 8 (((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) → (𝑠𝐶 ↔ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠))
7574ralrimiva 3113 . . . . . . 7 ((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) → ∀𝑠 ∈ 𝒫 𝑋(𝑠𝐶 ↔ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠))
7675ex 401 . . . . . 6 (𝐶 ∈ (Moore‘𝑋) → ((𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡)) → ∀𝑠 ∈ 𝒫 𝑋(𝑠𝐶 ↔ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠)))
7776exlimdv 2028 . . . . 5 (𝐶 ∈ (Moore‘𝑋) → (∃𝑓(𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡)) → ∀𝑠 ∈ 𝒫 𝑋(𝑠𝐶 ↔ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠)))
7819mrcf 16538 . . . . . . . 8 (𝐶 ∈ (Moore‘𝑋) → 𝐹:𝒫 𝑋𝐶)
7978, 42fssd 6239 . . . . . . 7 (𝐶 ∈ (Moore‘𝑋) → 𝐹:𝒫 𝑋⟶𝒫 𝑋)
8019fvexi 6391 . . . . . . . 8 𝐹 ∈ V
81 feq1 6206 . . . . . . . . 9 (𝑓 = 𝐹 → (𝑓:𝒫 𝑋⟶𝒫 𝑋𝐹:𝒫 𝑋⟶𝒫 𝑋))
82 fveq1 6376 . . . . . . . . . . . . . . 15 (𝑓 = 𝐹 → (𝑓𝑧) = (𝐹𝑧))
8382sseq1d 3794 . . . . . . . . . . . . . 14 (𝑓 = 𝐹 → ((𝑓𝑧) ⊆ 𝑡 ↔ (𝐹𝑧) ⊆ 𝑡))
8483ralbidv 3133 . . . . . . . . . . . . 13 (𝑓 = 𝐹 → (∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝐹𝑧) ⊆ 𝑡))
85 fveq2 6377 . . . . . . . . . . . . . . 15 (𝑧 = 𝑦 → (𝐹𝑧) = (𝐹𝑦))
8685sseq1d 3794 . . . . . . . . . . . . . 14 (𝑧 = 𝑦 → ((𝐹𝑧) ⊆ 𝑡 ↔ (𝐹𝑦) ⊆ 𝑡))
8786cbvralv 3319 . . . . . . . . . . . . 13 (∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝐹𝑧) ⊆ 𝑡 ↔ ∀𝑦 ∈ (𝒫 𝑡 ∩ Fin)(𝐹𝑦) ⊆ 𝑡)
8884, 87syl6bb 278 . . . . . . . . . . . 12 (𝑓 = 𝐹 → (∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡 ↔ ∀𝑦 ∈ (𝒫 𝑡 ∩ Fin)(𝐹𝑦) ⊆ 𝑡))
8988bibi2d 333 . . . . . . . . . . 11 (𝑓 = 𝐹 → ((𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡) ↔ (𝑡𝐶 ↔ ∀𝑦 ∈ (𝒫 𝑡 ∩ Fin)(𝐹𝑦) ⊆ 𝑡)))
9089ralbidv 3133 . . . . . . . . . 10 (𝑓 = 𝐹 → (∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡) ↔ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑦 ∈ (𝒫 𝑡 ∩ Fin)(𝐹𝑦) ⊆ 𝑡)))
91 sseq2 3789 . . . . . . . . . . . . 13 (𝑡 = 𝑠 → ((𝐹𝑦) ⊆ 𝑡 ↔ (𝐹𝑦) ⊆ 𝑠))
9266, 91raleqbidv 3300 . . . . . . . . . . . 12 (𝑡 = 𝑠 → (∀𝑦 ∈ (𝒫 𝑡 ∩ Fin)(𝐹𝑦) ⊆ 𝑡 ↔ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠))
9364, 92bibi12d 336 . . . . . . . . . . 11 (𝑡 = 𝑠 → ((𝑡𝐶 ↔ ∀𝑦 ∈ (𝒫 𝑡 ∩ Fin)(𝐹𝑦) ⊆ 𝑡) ↔ (𝑠𝐶 ↔ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠)))
9493cbvralv 3319 . . . . . . . . . 10 (∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑦 ∈ (𝒫 𝑡 ∩ Fin)(𝐹𝑦) ⊆ 𝑡) ↔ ∀𝑠 ∈ 𝒫 𝑋(𝑠𝐶 ↔ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠))
9590, 94syl6bb 278 . . . . . . . . 9 (𝑓 = 𝐹 → (∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡) ↔ ∀𝑠 ∈ 𝒫 𝑋(𝑠𝐶 ↔ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠)))
9681, 95anbi12d 624 . . . . . . . 8 (𝑓 = 𝐹 → ((𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡)) ↔ (𝐹:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑠 ∈ 𝒫 𝑋(𝑠𝐶 ↔ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠))))
9780, 96spcev 3453 . . . . . . 7 ((𝐹:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑠 ∈ 𝒫 𝑋(𝑠𝐶 ↔ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠)) → ∃𝑓(𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡)))
9879, 97sylan 575 . . . . . 6 ((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝑋(𝑠𝐶 ↔ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠)) → ∃𝑓(𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡)))
9998ex 401 . . . . 5 (𝐶 ∈ (Moore‘𝑋) → (∀𝑠 ∈ 𝒫 𝑋(𝑠𝐶 ↔ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠) → ∃𝑓(𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))))
10077, 99impbid 203 . . . 4 (𝐶 ∈ (Moore‘𝑋) → (∃𝑓(𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡)) ↔ ∀𝑠 ∈ 𝒫 𝑋(𝑠𝐶 ↔ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠)))
10111, 100syl5bb 274 . . 3 (𝐶 ∈ (Moore‘𝑋) → (∃𝑓(𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 (𝑓 “ (𝒫 𝑡 ∩ Fin)) ⊆ 𝑡)) ↔ ∀𝑠 ∈ 𝒫 𝑋(𝑠𝐶 ↔ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠)))
102101pm5.32i 570 . 2 ((𝐶 ∈ (Moore‘𝑋) ∧ ∃𝑓(𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 (𝑓 “ (𝒫 𝑡 ∩ Fin)) ⊆ 𝑡))) ↔ (𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝑋(𝑠𝐶 ↔ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠)))
1031, 102bitri 266 1 (𝐶 ∈ (ACS‘𝑋) ↔ (𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝑋(𝑠𝐶 ↔ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384   = wceq 1652  wex 1874  wcel 2155  wral 3055  cin 3733  wss 3734  𝒫 cpw 4317   cuni 4596   ciun 4678  cima 5282  Fun wfun 6064  wf 6066  cfv 6070  Fincfn 8162  Moorecmre 16511  mrClscmrc 16512  ACScacs 16514
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-sep 4943  ax-nul 4951  ax-pow 5003  ax-pr 5064  ax-un 7149
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-ral 3060  df-rex 3061  df-rab 3064  df-v 3352  df-sbc 3599  df-csb 3694  df-dif 3737  df-un 3739  df-in 3741  df-ss 3748  df-nul 4082  df-if 4246  df-pw 4319  df-sn 4337  df-pr 4339  df-op 4343  df-uni 4597  df-int 4636  df-iun 4680  df-br 4812  df-opab 4874  df-mpt 4891  df-id 5187  df-xp 5285  df-rel 5286  df-cnv 5287  df-co 5288  df-dm 5289  df-rn 5290  df-res 5291  df-ima 5292  df-iota 6033  df-fun 6072  df-fn 6073  df-f 6074  df-fv 6078  df-mre 16515  df-mrc 16516  df-acs 16518
This theorem is referenced by:  acsfiel  16583  isacs5  17441
  Copyright terms: Public domain W3C validator