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

Theorem isacs2 16511
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 16509 . 2 (𝐶 ∈ (ACS‘𝑋) ↔ (𝐶 ∈ (Moore‘𝑋) ∧ ∃𝑓(𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 (𝑓 “ (𝒫 𝑡 ∩ Fin)) ⊆ 𝑡))))
2 iunss 4709 . . . . . . . . 9 ( 𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡)
3 ffun 6205 . . . . . . . . . . 11 (𝑓:𝒫 𝑋⟶𝒫 𝑋 → Fun 𝑓)
4 funiunfv 6665 . . . . . . . . . . 11 (Fun 𝑓 𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) = (𝑓 “ (𝒫 𝑡 ∩ Fin)))
53, 4syl 17 . . . . . . . . . 10 (𝑓:𝒫 𝑋⟶𝒫 𝑋 𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) = (𝑓 “ (𝒫 𝑡 ∩ Fin)))
65sseq1d 3769 . . . . . . . . 9 (𝑓:𝒫 𝑋⟶𝒫 𝑋 → ( 𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡 (𝑓 “ (𝒫 𝑡 ∩ Fin)) ⊆ 𝑡))
72, 6syl5rbbr 275 . . . . . . . 8 (𝑓:𝒫 𝑋⟶𝒫 𝑋 → ( (𝑓 “ (𝒫 𝑡 ∩ Fin)) ⊆ 𝑡 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))
87bibi2d 331 . . . . . . 7 (𝑓:𝒫 𝑋⟶𝒫 𝑋 → ((𝑡𝐶 (𝑓 “ (𝒫 𝑡 ∩ Fin)) ⊆ 𝑡) ↔ (𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡)))
98ralbidv 3120 . . . . . 6 (𝑓:𝒫 𝑋⟶𝒫 𝑋 → (∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 (𝑓 “ (𝒫 𝑡 ∩ Fin)) ⊆ 𝑡) ↔ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡)))
109pm5.32i 672 . . . . 5 ((𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 (𝑓 “ (𝒫 𝑡 ∩ Fin)) ⊆ 𝑡)) ↔ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡)))
1110exbii 1919 . . . 4 (∃𝑓(𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 (𝑓 “ (𝒫 𝑡 ∩ Fin)) ⊆ 𝑡)) ↔ ∃𝑓(𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡)))
12 simpll 807 . . . . . . . . . . . . 13 (((𝐶 ∈ (Moore‘𝑋) ∧ 𝑠𝐶) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → 𝐶 ∈ (Moore‘𝑋))
13 inss1 3972 . . . . . . . . . . . . . . . 16 (𝒫 𝑠 ∩ Fin) ⊆ 𝒫 𝑠
1413sseli 3736 . . . . . . . . . . . . . . 15 (𝑦 ∈ (𝒫 𝑠 ∩ Fin) → 𝑦 ∈ 𝒫 𝑠)
15 elpwi 4308 . . . . . . . . . . . . . . 15 (𝑦 ∈ 𝒫 𝑠𝑦𝑠)
1614, 15syl 17 . . . . . . . . . . . . . 14 (𝑦 ∈ (𝒫 𝑠 ∩ Fin) → 𝑦𝑠)
1716adantl 473 . . . . . . . . . . . . 13 (((𝐶 ∈ (Moore‘𝑋) ∧ 𝑠𝐶) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → 𝑦𝑠)
18 simplr 809 . . . . . . . . . . . . 13 (((𝐶 ∈ (Moore‘𝑋) ∧ 𝑠𝐶) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → 𝑠𝐶)
19 isacs2.f . . . . . . . . . . . . . 14 𝐹 = (mrCls‘𝐶)
2019mrcsscl 16478 . . . . . . . . . . . . 13 ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑦𝑠𝑠𝐶) → (𝐹𝑦) ⊆ 𝑠)
2112, 17, 18, 20syl3anc 1477 . . . . . . . . . . . 12 (((𝐶 ∈ (Moore‘𝑋) ∧ 𝑠𝐶) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → (𝐹𝑦) ⊆ 𝑠)
2221ralrimiva 3100 . . . . . . . . . . 11 ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑠𝐶) → ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠)
2322adantlr 753 . . . . . . . . . 10 (((𝐶 ∈ (Moore‘𝑋) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ 𝑠𝐶) → ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠)
2423adantllr 757 . . . . . . . . 9 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ 𝑠𝐶) → ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠)
25 simplll 815 . . . . . . . . . . . . . . . . . 18 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → 𝐶 ∈ (Moore‘𝑋))
2616adantl 473 . . . . . . . . . . . . . . . . . . 19 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → 𝑦𝑠)
27 elpwi 4308 . . . . . . . . . . . . . . . . . . . 20 (𝑠 ∈ 𝒫 𝑋𝑠𝑋)
2827ad2antlr 765 . . . . . . . . . . . . . . . . . . 19 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → 𝑠𝑋)
2926, 28sstrd 3750 . . . . . . . . . . . . . . . . . 18 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → 𝑦𝑋)
3025, 19, 29mrcssidd 16483 . . . . . . . . . . . . . . . . 17 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → 𝑦 ⊆ (𝐹𝑦))
31 vex 3339 . . . . . . . . . . . . . . . . . 18 𝑦 ∈ V
3231elpw 4304 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ 𝒫 (𝐹𝑦) ↔ 𝑦 ⊆ (𝐹𝑦))
3330, 32sylibr 224 . . . . . . . . . . . . . . . 16 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → 𝑦 ∈ 𝒫 (𝐹𝑦))
34 inss2 3973 . . . . . . . . . . . . . . . . . 18 (𝒫 𝑠 ∩ Fin) ⊆ Fin
3534sseli 3736 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (𝒫 𝑠 ∩ Fin) → 𝑦 ∈ Fin)
3635adantl 473 . . . . . . . . . . . . . . . 16 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → 𝑦 ∈ Fin)
3733, 36elind 3937 . . . . . . . . . . . . . . 15 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → 𝑦 ∈ (𝒫 (𝐹𝑦) ∩ Fin))
3819mrccl 16469 . . . . . . . . . . . . . . . . 17 ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑦𝑋) → (𝐹𝑦) ∈ 𝐶)
3925, 29, 38syl2anc 696 . . . . . . . . . . . . . . . 16 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → (𝐹𝑦) ∈ 𝐶)
40 mresspw 16450 . . . . . . . . . . . . . . . . . . 19 (𝐶 ∈ (Moore‘𝑋) → 𝐶 ⊆ 𝒫 𝑋)
4140ad3antrrr 768 . . . . . . . . . . . . . . . . . 18 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → 𝐶 ⊆ 𝒫 𝑋)
4241, 39sseldd 3741 . . . . . . . . . . . . . . . . 17 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → (𝐹𝑦) ∈ 𝒫 𝑋)
43 simprr 813 . . . . . . . . . . . . . . . . . 18 ((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) → ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))
4443ad2antrr 764 . . . . . . . . . . . . . . . . 17 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))
45 eleq1 2823 . . . . . . . . . . . . . . . . . . 19 (𝑡 = (𝐹𝑦) → (𝑡𝐶 ↔ (𝐹𝑦) ∈ 𝐶))
46 pweq 4301 . . . . . . . . . . . . . . . . . . . . 21 (𝑡 = (𝐹𝑦) → 𝒫 𝑡 = 𝒫 (𝐹𝑦))
4746ineq1d 3952 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = (𝐹𝑦) → (𝒫 𝑡 ∩ Fin) = (𝒫 (𝐹𝑦) ∩ Fin))
48 sseq2 3764 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = (𝐹𝑦) → ((𝑓𝑧) ⊆ 𝑡 ↔ (𝑓𝑧) ⊆ (𝐹𝑦)))
4947, 48raleqbidv 3287 . . . . . . . . . . . . . . . . . . 19 (𝑡 = (𝐹𝑦) → (∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡 ↔ ∀𝑧 ∈ (𝒫 (𝐹𝑦) ∩ Fin)(𝑓𝑧) ⊆ (𝐹𝑦)))
5045, 49bibi12d 334 . . . . . . . . . . . . . . . . . 18 (𝑡 = (𝐹𝑦) → ((𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡) ↔ ((𝐹𝑦) ∈ 𝐶 ↔ ∀𝑧 ∈ (𝒫 (𝐹𝑦) ∩ Fin)(𝑓𝑧) ⊆ (𝐹𝑦))))
5150rspcva 3443 . . . . . . . . . . . . . . . . 17 (((𝐹𝑦) ∈ 𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡)) → ((𝐹𝑦) ∈ 𝐶 ↔ ∀𝑧 ∈ (𝒫 (𝐹𝑦) ∩ Fin)(𝑓𝑧) ⊆ (𝐹𝑦)))
5242, 44, 51syl2anc 696 . . . . . . . . . . . . . . . 16 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → ((𝐹𝑦) ∈ 𝐶 ↔ ∀𝑧 ∈ (𝒫 (𝐹𝑦) ∩ Fin)(𝑓𝑧) ⊆ (𝐹𝑦)))
5339, 52mpbid 222 . . . . . . . . . . . . . . 15 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → ∀𝑧 ∈ (𝒫 (𝐹𝑦) ∩ Fin)(𝑓𝑧) ⊆ (𝐹𝑦))
54 fveq2 6348 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑦 → (𝑓𝑧) = (𝑓𝑦))
5554sseq1d 3769 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑦 → ((𝑓𝑧) ⊆ (𝐹𝑦) ↔ (𝑓𝑦) ⊆ (𝐹𝑦)))
5655rspcva 3443 . . . . . . . . . . . . . . 15 ((𝑦 ∈ (𝒫 (𝐹𝑦) ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 (𝐹𝑦) ∩ Fin)(𝑓𝑧) ⊆ (𝐹𝑦)) → (𝑓𝑦) ⊆ (𝐹𝑦))
5737, 53, 56syl2anc 696 . . . . . . . . . . . . . 14 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → (𝑓𝑦) ⊆ (𝐹𝑦))
58 sstr2 3747 . . . . . . . . . . . . . 14 ((𝑓𝑦) ⊆ (𝐹𝑦) → ((𝐹𝑦) ⊆ 𝑠 → (𝑓𝑦) ⊆ 𝑠))
5957, 58syl 17 . . . . . . . . . . . . 13 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ 𝑦 ∈ (𝒫 𝑠 ∩ Fin)) → ((𝐹𝑦) ⊆ 𝑠 → (𝑓𝑦) ⊆ 𝑠))
6059ralimdva 3096 . . . . . . . . . . . 12 (((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) → (∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠 → ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝑓𝑦) ⊆ 𝑠))
6160imp 444 . . . . . . . . . . 11 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠) → ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝑓𝑦) ⊆ 𝑠)
62 fveq2 6348 . . . . . . . . . . . . 13 (𝑦 = 𝑧 → (𝑓𝑦) = (𝑓𝑧))
6362sseq1d 3769 . . . . . . . . . . . 12 (𝑦 = 𝑧 → ((𝑓𝑦) ⊆ 𝑠 ↔ (𝑓𝑧) ⊆ 𝑠))
6463cbvralv 3306 . . . . . . . . . . 11 (∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝑓𝑦) ⊆ 𝑠 ↔ ∀𝑧 ∈ (𝒫 𝑠 ∩ Fin)(𝑓𝑧) ⊆ 𝑠)
6561, 64sylib 208 . . . . . . . . . 10 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠) → ∀𝑧 ∈ (𝒫 𝑠 ∩ Fin)(𝑓𝑧) ⊆ 𝑠)
66 simplr 809 . . . . . . . . . . 11 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠) → 𝑠 ∈ 𝒫 𝑋)
6743ad2antrr 764 . . . . . . . . . . 11 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠) → ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))
68 eleq1 2823 . . . . . . . . . . . . 13 (𝑡 = 𝑠 → (𝑡𝐶𝑠𝐶))
69 pweq 4301 . . . . . . . . . . . . . . 15 (𝑡 = 𝑠 → 𝒫 𝑡 = 𝒫 𝑠)
7069ineq1d 3952 . . . . . . . . . . . . . 14 (𝑡 = 𝑠 → (𝒫 𝑡 ∩ Fin) = (𝒫 𝑠 ∩ Fin))
71 sseq2 3764 . . . . . . . . . . . . . 14 (𝑡 = 𝑠 → ((𝑓𝑧) ⊆ 𝑡 ↔ (𝑓𝑧) ⊆ 𝑠))
7270, 71raleqbidv 3287 . . . . . . . . . . . . 13 (𝑡 = 𝑠 → (∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡 ↔ ∀𝑧 ∈ (𝒫 𝑠 ∩ Fin)(𝑓𝑧) ⊆ 𝑠))
7368, 72bibi12d 334 . . . . . . . . . . . 12 (𝑡 = 𝑠 → ((𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡) ↔ (𝑠𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑠 ∩ Fin)(𝑓𝑧) ⊆ 𝑠)))
7473rspcva 3443 . . . . . . . . . . 11 ((𝑠 ∈ 𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡)) → (𝑠𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑠 ∩ Fin)(𝑓𝑧) ⊆ 𝑠))
7566, 67, 74syl2anc 696 . . . . . . . . . 10 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠) → (𝑠𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑠 ∩ Fin)(𝑓𝑧) ⊆ 𝑠))
7665, 75mpbird 247 . . . . . . . . 9 ((((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) ∧ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠) → 𝑠𝐶)
7724, 76impbida 913 . . . . . . . 8 (((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) → (𝑠𝐶 ↔ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠))
7877ralrimiva 3100 . . . . . . 7 ((𝐶 ∈ (Moore‘𝑋) ∧ (𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))) → ∀𝑠 ∈ 𝒫 𝑋(𝑠𝐶 ↔ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠))
7978ex 449 . . . . . 6 (𝐶 ∈ (Moore‘𝑋) → ((𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡)) → ∀𝑠 ∈ 𝒫 𝑋(𝑠𝐶 ↔ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠)))
8079exlimdv 2006 . . . . 5 (𝐶 ∈ (Moore‘𝑋) → (∃𝑓(𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡)) → ∀𝑠 ∈ 𝒫 𝑋(𝑠𝐶 ↔ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠)))
8119mrcf 16467 . . . . . . . 8 (𝐶 ∈ (Moore‘𝑋) → 𝐹:𝒫 𝑋𝐶)
8281, 40fssd 6214 . . . . . . 7 (𝐶 ∈ (Moore‘𝑋) → 𝐹:𝒫 𝑋⟶𝒫 𝑋)
83 fvex 6358 . . . . . . . . 9 (mrCls‘𝐶) ∈ V
8419, 83eqeltri 2831 . . . . . . . 8 𝐹 ∈ V
85 feq1 6183 . . . . . . . . 9 (𝑓 = 𝐹 → (𝑓:𝒫 𝑋⟶𝒫 𝑋𝐹:𝒫 𝑋⟶𝒫 𝑋))
86 fveq1 6347 . . . . . . . . . . . . . . 15 (𝑓 = 𝐹 → (𝑓𝑧) = (𝐹𝑧))
8786sseq1d 3769 . . . . . . . . . . . . . 14 (𝑓 = 𝐹 → ((𝑓𝑧) ⊆ 𝑡 ↔ (𝐹𝑧) ⊆ 𝑡))
8887ralbidv 3120 . . . . . . . . . . . . 13 (𝑓 = 𝐹 → (∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝐹𝑧) ⊆ 𝑡))
89 fveq2 6348 . . . . . . . . . . . . . . 15 (𝑧 = 𝑦 → (𝐹𝑧) = (𝐹𝑦))
9089sseq1d 3769 . . . . . . . . . . . . . 14 (𝑧 = 𝑦 → ((𝐹𝑧) ⊆ 𝑡 ↔ (𝐹𝑦) ⊆ 𝑡))
9190cbvralv 3306 . . . . . . . . . . . . 13 (∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝐹𝑧) ⊆ 𝑡 ↔ ∀𝑦 ∈ (𝒫 𝑡 ∩ Fin)(𝐹𝑦) ⊆ 𝑡)
9288, 91syl6bb 276 . . . . . . . . . . . 12 (𝑓 = 𝐹 → (∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡 ↔ ∀𝑦 ∈ (𝒫 𝑡 ∩ Fin)(𝐹𝑦) ⊆ 𝑡))
9392bibi2d 331 . . . . . . . . . . 11 (𝑓 = 𝐹 → ((𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡) ↔ (𝑡𝐶 ↔ ∀𝑦 ∈ (𝒫 𝑡 ∩ Fin)(𝐹𝑦) ⊆ 𝑡)))
9493ralbidv 3120 . . . . . . . . . 10 (𝑓 = 𝐹 → (∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡) ↔ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑦 ∈ (𝒫 𝑡 ∩ Fin)(𝐹𝑦) ⊆ 𝑡)))
95 sseq2 3764 . . . . . . . . . . . . 13 (𝑡 = 𝑠 → ((𝐹𝑦) ⊆ 𝑡 ↔ (𝐹𝑦) ⊆ 𝑠))
9670, 95raleqbidv 3287 . . . . . . . . . . . 12 (𝑡 = 𝑠 → (∀𝑦 ∈ (𝒫 𝑡 ∩ Fin)(𝐹𝑦) ⊆ 𝑡 ↔ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠))
9768, 96bibi12d 334 . . . . . . . . . . 11 (𝑡 = 𝑠 → ((𝑡𝐶 ↔ ∀𝑦 ∈ (𝒫 𝑡 ∩ Fin)(𝐹𝑦) ⊆ 𝑡) ↔ (𝑠𝐶 ↔ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠)))
9897cbvralv 3306 . . . . . . . . . 10 (∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑦 ∈ (𝒫 𝑡 ∩ Fin)(𝐹𝑦) ⊆ 𝑡) ↔ ∀𝑠 ∈ 𝒫 𝑋(𝑠𝐶 ↔ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠))
9994, 98syl6bb 276 . . . . . . . . 9 (𝑓 = 𝐹 → (∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡) ↔ ∀𝑠 ∈ 𝒫 𝑋(𝑠𝐶 ↔ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠)))
10085, 99anbi12d 749 . . . . . . . 8 (𝑓 = 𝐹 → ((𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡)) ↔ (𝐹:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑠 ∈ 𝒫 𝑋(𝑠𝐶 ↔ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠))))
10184, 100spcev 3436 . . . . . . 7 ((𝐹:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑠 ∈ 𝒫 𝑋(𝑠𝐶 ↔ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠)) → ∃𝑓(𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡)))
10282, 101sylan 489 . . . . . 6 ((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝑋(𝑠𝐶 ↔ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠)) → ∃𝑓(𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡)))
103102ex 449 . . . . 5 (𝐶 ∈ (Moore‘𝑋) → (∀𝑠 ∈ 𝒫 𝑋(𝑠𝐶 ↔ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠) → ∃𝑓(𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡))))
10480, 103impbid 202 . . . 4 (𝐶 ∈ (Moore‘𝑋) → (∃𝑓(𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 ↔ ∀𝑧 ∈ (𝒫 𝑡 ∩ Fin)(𝑓𝑧) ⊆ 𝑡)) ↔ ∀𝑠 ∈ 𝒫 𝑋(𝑠𝐶 ↔ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠)))
10511, 104syl5bb 272 . . 3 (𝐶 ∈ (Moore‘𝑋) → (∃𝑓(𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡𝐶 (𝑓 “ (𝒫 𝑡 ∩ Fin)) ⊆ 𝑡)) ↔ ∀𝑠 ∈ 𝒫 𝑋(𝑠𝐶 ↔ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹𝑦) ⊆ 𝑠)))
106105pm5.32i 672 . 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 383   = wceq 1628  wex 1849  wcel 2135  wral 3046  Vcvv 3336  cin 3710  wss 3711  𝒫 cpw 4298   cuni 4584   ciun 4668  cima 5265  Fun wfun 6039  wf 6041  cfv 6045  Fincfn 8117  Moorecmre 16440  mrClscmrc 16441  ACScacs 16443
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1867  ax-4 1882  ax-5 1984  ax-6 2050  ax-7 2086  ax-8 2137  ax-9 2144  ax-10 2164  ax-11 2179  ax-12 2192  ax-13 2387  ax-ext 2736  ax-sep 4929  ax-nul 4937  ax-pow 4988  ax-pr 5051  ax-un 7110
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1631  df-ex 1850  df-nf 1855  df-sb 2043  df-eu 2607  df-mo 2608  df-clab 2743  df-cleq 2749  df-clel 2752  df-nfc 2887  df-ne 2929  df-ral 3051  df-rex 3052  df-rab 3055  df-v 3338  df-sbc 3573  df-csb 3671  df-dif 3714  df-un 3716  df-in 3718  df-ss 3725  df-nul 4055  df-if 4227  df-pw 4300  df-sn 4318  df-pr 4320  df-op 4324  df-uni 4585  df-int 4624  df-iun 4670  df-br 4801  df-opab 4861  df-mpt 4878  df-id 5170  df-xp 5268  df-rel 5269  df-cnv 5270  df-co 5271  df-dm 5272  df-rn 5273  df-res 5274  df-ima 5275  df-iota 6008  df-fun 6047  df-fn 6048  df-f 6049  df-fv 6053  df-mre 16444  df-mrc 16445  df-acs 16447
This theorem is referenced by:  acsfiel  16512  isacs5  17369
  Copyright terms: Public domain W3C validator