Theorem mreacs 17284

Description: Algebraicity is a composable property; combining several algebraic closure properties gives another. (Contributed by Stefan O'Rear, 3-Apr-2015.)

Assertion

Ref	Expression
mreacs	⊢ (𝑋 ∈ 𝑉 → (ACS‘𝑋) ∈ (Moore‘𝒫 𝑋))

Proof of Theorem mreacs

Dummy variables 𝑎 𝑏 𝑐 𝑥 𝑑 𝑒 𝑓 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fveq2 6756	. . 3 ⊢ (𝑥 = 𝑋 → (ACS‘𝑥) = (ACS‘𝑋))
2		pweq 4546	. . . 4 ⊢ (𝑥 = 𝑋 → 𝒫 𝑥 = 𝒫 𝑋)
3	2	fveq2d 6760	. . 3 ⊢ (𝑥 = 𝑋 → (Moore‘𝒫 𝑥) = (Moore‘𝒫 𝑋))
4	1, 3	eleq12d 2833	. 2 ⊢ (𝑥 = 𝑋 → ((ACS‘𝑥) ∈ (Moore‘𝒫 𝑥) ↔ (ACS‘𝑋) ∈ (Moore‘𝒫 𝑋)))
5		acsmre 17278	. . . . . . 7 ⊢ (𝑎 ∈ (ACS‘𝑥) → 𝑎 ∈ (Moore‘𝑥))
6		mresspw 17218	. . . . . . . 8 ⊢ (𝑎 ∈ (Moore‘𝑥) → 𝑎 ⊆ 𝒫 𝑥)
7	5, 6	syl 17	. . . . . . 7 ⊢ (𝑎 ∈ (ACS‘𝑥) → 𝑎 ⊆ 𝒫 𝑥)
8	5, 7	elpwd 4538	. . . . . 6 ⊢ (𝑎 ∈ (ACS‘𝑥) → 𝑎 ∈ 𝒫 𝒫 𝑥)
9	8	ssriv 3921	. . . . 5 ⊢ (ACS‘𝑥) ⊆ 𝒫 𝒫 𝑥
10	9	a1i 11	. . . 4 ⊢ (⊤ → (ACS‘𝑥) ⊆ 𝒫 𝒫 𝑥)
11		vex 3426	. . . . . . . 8 ⊢ 𝑥 ∈ V
12		mremre 17230	. . . . . . . 8 ⊢ (𝑥 ∈ V → (Moore‘𝑥) ∈ (Moore‘𝒫 𝑥))
13	11, 12	mp1i 13	. . . . . . 7 ⊢ (𝑎 ⊆ (ACS‘𝑥) → (Moore‘𝑥) ∈ (Moore‘𝒫 𝑥))
14	5	ssriv 3921	. . . . . . . 8 ⊢ (ACS‘𝑥) ⊆ (Moore‘𝑥)
15		sstr 3925	. . . . . . . 8 ⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ (ACS‘𝑥) ⊆ (Moore‘𝑥)) → 𝑎 ⊆ (Moore‘𝑥))
16	14, 15	mpan2 687	. . . . . . 7 ⊢ (𝑎 ⊆ (ACS‘𝑥) → 𝑎 ⊆ (Moore‘𝑥))
17		mrerintcl 17223	. . . . . . 7 ⊢ (((Moore‘𝑥) ∈ (Moore‘𝒫 𝑥) ∧ 𝑎 ⊆ (Moore‘𝑥)) → (𝒫 𝑥 ∩ ∩ 𝑎) ∈ (Moore‘𝑥))
18	13, 16, 17	syl2anc 583	. . . . . 6 ⊢ (𝑎 ⊆ (ACS‘𝑥) → (𝒫 𝑥 ∩ ∩ 𝑎) ∈ (Moore‘𝑥))
19		ssel2 3912	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑑 ∈ 𝑎) → 𝑑 ∈ (ACS‘𝑥))
20	19	acsmred 17282	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑑 ∈ 𝑎) → 𝑑 ∈ (Moore‘𝑥))
21		eqid 2738	. . . . . . . . . . . . . . 15 ⊢ (mrCls‘𝑑) = (mrCls‘𝑑)
22	20, 21	mrcssvd 17249	. . . . . . . . . . . . . 14 ⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑑 ∈ 𝑎) → ((mrCls‘𝑑)‘𝑐) ⊆ 𝑥)
23	22	ralrimiva 3107	. . . . . . . . . . . . 13 ⊢ (𝑎 ⊆ (ACS‘𝑥) → ∀𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐) ⊆ 𝑥)
24	23	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑐 ∈ 𝒫 𝑥) → ∀𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐) ⊆ 𝑥)
25		iunss 4971	. . . . . . . . . . . 12 ⊢ (∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐) ⊆ 𝑥 ↔ ∀𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐) ⊆ 𝑥)
26	24, 25	sylibr 233	. . . . . . . . . . 11 ⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑐 ∈ 𝒫 𝑥) → ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐) ⊆ 𝑥)
27	11	elpw2 5264	. . . . . . . . . . 11 ⊢ (∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐) ∈ 𝒫 𝑥 ↔ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐) ⊆ 𝑥)
28	26, 27	sylibr 233	. . . . . . . . . 10 ⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑐 ∈ 𝒫 𝑥) → ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐) ∈ 𝒫 𝑥)
29	28	fmpttd 6971	. . . . . . . . 9 ⊢ (𝑎 ⊆ (ACS‘𝑥) → (𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)):𝒫 𝑥⟶𝒫 𝑥)
30		fssxp 6612	. . . . . . . . 9 ⊢ ((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)):𝒫 𝑥⟶𝒫 𝑥 → (𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) ⊆ (𝒫 𝑥 × 𝒫 𝑥))
31	29, 30	syl 17	. . . . . . . 8 ⊢ (𝑎 ⊆ (ACS‘𝑥) → (𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) ⊆ (𝒫 𝑥 × 𝒫 𝑥))
32		vpwex 5295	. . . . . . . . 9 ⊢ 𝒫 𝑥 ∈ V
33	32, 32	xpex 7581	. . . . . . . 8 ⊢ (𝒫 𝑥 × 𝒫 𝑥) ∈ V
34		ssexg 5242	. . . . . . . 8 ⊢ (((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) ⊆ (𝒫 𝑥 × 𝒫 𝑥) ∧ (𝒫 𝑥 × 𝒫 𝑥) ∈ V) → (𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) ∈ V)
35	31, 33, 34	sylancl 585	. . . . . . 7 ⊢ (𝑎 ⊆ (ACS‘𝑥) → (𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) ∈ V)
36	19	adantlr 711	. . . . . . . . . . . . 13 ⊢ (((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) ∧ 𝑑 ∈ 𝑎) → 𝑑 ∈ (ACS‘𝑥))
37		elpwi 4539	. . . . . . . . . . . . . 14 ⊢ (𝑏 ∈ 𝒫 𝑥 → 𝑏 ⊆ 𝑥)
38	37	ad2antlr 723	. . . . . . . . . . . . 13 ⊢ (((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) ∧ 𝑑 ∈ 𝑎) → 𝑏 ⊆ 𝑥)
39	21	acsfiel2 17281	. . . . . . . . . . . . 13 ⊢ ((𝑑 ∈ (ACS‘𝑥) ∧ 𝑏 ⊆ 𝑥) → (𝑏 ∈ 𝑑 ↔ ∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)((mrCls‘𝑑)‘𝑒) ⊆ 𝑏))
40	36, 38, 39	syl2anc 583	. . . . . . . . . . . 12 ⊢ (((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) ∧ 𝑑 ∈ 𝑎) → (𝑏 ∈ 𝑑 ↔ ∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)((mrCls‘𝑑)‘𝑒) ⊆ 𝑏))
41	40	ralbidva 3119	. . . . . . . . . . 11 ⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) → (∀𝑑 ∈ 𝑎 𝑏 ∈ 𝑑 ↔ ∀𝑑 ∈ 𝑎 ∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)((mrCls‘𝑑)‘𝑒) ⊆ 𝑏))
42		iunss 4971	. . . . . . . . . . . . 13 ⊢ (∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏 ↔ ∀𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏)
43	42	ralbii 3090	. . . . . . . . . . . 12 ⊢ (∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏 ↔ ∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)∀𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏)
44		ralcom 3280	. . . . . . . . . . . 12 ⊢ (∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)∀𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏 ↔ ∀𝑑 ∈ 𝑎 ∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)((mrCls‘𝑑)‘𝑒) ⊆ 𝑏)
45	43, 44	bitri 274	. . . . . . . . . . 11 ⊢ (∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏 ↔ ∀𝑑 ∈ 𝑎 ∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)((mrCls‘𝑑)‘𝑒) ⊆ 𝑏)
46	41, 45	bitr4di 288	. . . . . . . . . 10 ⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) → (∀𝑑 ∈ 𝑎 𝑏 ∈ 𝑑 ↔ ∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏))
47		elrint2 4920	. . . . . . . . . . 11 ⊢ (𝑏 ∈ 𝒫 𝑥 → (𝑏 ∈ (𝒫 𝑥 ∩ ∩ 𝑎) ↔ ∀𝑑 ∈ 𝑎 𝑏 ∈ 𝑑))
48	47	adantl 481	. . . . . . . . . 10 ⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) → (𝑏 ∈ (𝒫 𝑥 ∩ ∩ 𝑎) ↔ ∀𝑑 ∈ 𝑎 𝑏 ∈ 𝑑))
49		funmpt 6456	. . . . . . . . . . . . 13 ⊢ Fun (𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐))
50		funiunfv 7103	. . . . . . . . . . . . 13 ⊢ (Fun (𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) → ∪ 𝑒 ∈ (𝒫 𝑏 ∩ Fin)((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐))‘𝑒) = ∪ ((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)))
51	49, 50	ax-mp 5	. . . . . . . . . . . 12 ⊢ ∪ 𝑒 ∈ (𝒫 𝑏 ∩ Fin)((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐))‘𝑒) = ∪ ((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin))
52	51	sseq1i 3945	. . . . . . . . . . 11 ⊢ (∪ 𝑒 ∈ (𝒫 𝑏 ∩ Fin)((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐))‘𝑒) ⊆ 𝑏 ↔ ∪ ((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏)
53		iunss 4971	. . . . . . . . . . . 12 ⊢ (∪ 𝑒 ∈ (𝒫 𝑏 ∩ Fin)((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐))‘𝑒) ⊆ 𝑏 ↔ ∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐))‘𝑒) ⊆ 𝑏)
54		eqid 2738	. . . . . . . . . . . . . . 15 ⊢ (𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) = (𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐))
55		fveq2 6756	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 = 𝑒 → ((mrCls‘𝑑)‘𝑐) = ((mrCls‘𝑑)‘𝑒))
56	55	iuneq2d 4950	. . . . . . . . . . . . . . 15 ⊢ (𝑐 = 𝑒 → ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐) = ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒))
57		inss1 4159	. . . . . . . . . . . . . . . . 17 ⊢ (𝒫 𝑏 ∩ Fin) ⊆ 𝒫 𝑏
58	37	sspwd 4545	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 ∈ 𝒫 𝑥 → 𝒫 𝑏 ⊆ 𝒫 𝑥)
59	58	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) → 𝒫 𝑏 ⊆ 𝒫 𝑥)
60	57, 59	sstrid 3928	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) → (𝒫 𝑏 ∩ Fin) ⊆ 𝒫 𝑥)
61	60	sselda 3917	. . . . . . . . . . . . . . 15 ⊢ (((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) ∧ 𝑒 ∈ (𝒫 𝑏 ∩ Fin)) → 𝑒 ∈ 𝒫 𝑥)
62	20, 21	mrcssvd 17249	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑑 ∈ 𝑎) → ((mrCls‘𝑑)‘𝑒) ⊆ 𝑥)
63	62	ralrimiva 3107	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 ⊆ (ACS‘𝑥) → ∀𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑥)
64	63	ad2antrr 722	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) ∧ 𝑒 ∈ (𝒫 𝑏 ∩ Fin)) → ∀𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑥)
65		iunss 4971	. . . . . . . . . . . . . . . . 17 ⊢ (∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑥 ↔ ∀𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑥)
66	64, 65	sylibr 233	. . . . . . . . . . . . . . . 16 ⊢ (((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) ∧ 𝑒 ∈ (𝒫 𝑏 ∩ Fin)) → ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑥)
67		ssexg 5242	. . . . . . . . . . . . . . . 16 ⊢ ((∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑥 ∧ 𝑥 ∈ V) → ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ∈ V)
68	66, 11, 67	sylancl 585	. . . . . . . . . . . . . . 15 ⊢ (((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) ∧ 𝑒 ∈ (𝒫 𝑏 ∩ Fin)) → ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ∈ V)
69	54, 56, 61, 68	fvmptd3 6880	. . . . . . . . . . . . . 14 ⊢ (((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) ∧ 𝑒 ∈ (𝒫 𝑏 ∩ Fin)) → ((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐))‘𝑒) = ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒))
70	69	sseq1d 3948	. . . . . . . . . . . . 13 ⊢ (((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) ∧ 𝑒 ∈ (𝒫 𝑏 ∩ Fin)) → (((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐))‘𝑒) ⊆ 𝑏 ↔ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏))
71	70	ralbidva 3119	. . . . . . . . . . . 12 ⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) → (∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐))‘𝑒) ⊆ 𝑏 ↔ ∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏))
72	53, 71	syl5bb 282	. . . . . . . . . . 11 ⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) → (∪ 𝑒 ∈ (𝒫 𝑏 ∩ Fin)((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐))‘𝑒) ⊆ 𝑏 ↔ ∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏))
73	52, 72	bitr3id 284	. . . . . . . . . 10 ⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) → (∪ ((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏 ↔ ∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏))
74	46, 48, 73	3bitr4d 310	. . . . . . . . 9 ⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) → (𝑏 ∈ (𝒫 𝑥 ∩ ∩ 𝑎) ↔ ∪ ((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏))
75	74	ralrimiva 3107	. . . . . . . 8 ⊢ (𝑎 ⊆ (ACS‘𝑥) → ∀𝑏 ∈ 𝒫 𝑥(𝑏 ∈ (𝒫 𝑥 ∩ ∩ 𝑎) ↔ ∪ ((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏))
76	29, 75	jca 511	. . . . . . 7 ⊢ (𝑎 ⊆ (ACS‘𝑥) → ((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)):𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑏 ∈ 𝒫 𝑥(𝑏 ∈ (𝒫 𝑥 ∩ ∩ 𝑎) ↔ ∪ ((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏)))
77		feq1 6565	. . . . . . . 8 ⊢ (𝑓 = (𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) → (𝑓:𝒫 𝑥⟶𝒫 𝑥 ↔ (𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)):𝒫 𝑥⟶𝒫 𝑥))
78		imaeq1 5953	. . . . . . . . . . . 12 ⊢ (𝑓 = (𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) → (𝑓 “ (𝒫 𝑏 ∩ Fin)) = ((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)))
79	78	unieqd 4850	. . . . . . . . . . 11 ⊢ (𝑓 = (𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) → ∪ (𝑓 “ (𝒫 𝑏 ∩ Fin)) = ∪ ((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)))
80	79	sseq1d 3948	. . . . . . . . . 10 ⊢ (𝑓 = (𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) → (∪ (𝑓 “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏 ↔ ∪ ((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏))
81	80	bibi2d 342	. . . . . . . . 9 ⊢ (𝑓 = (𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) → ((𝑏 ∈ (𝒫 𝑥 ∩ ∩ 𝑎) ↔ ∪ (𝑓 “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏) ↔ (𝑏 ∈ (𝒫 𝑥 ∩ ∩ 𝑎) ↔ ∪ ((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏)))
82	81	ralbidv 3120	. . . . . . . 8 ⊢ (𝑓 = (𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) → (∀𝑏 ∈ 𝒫 𝑥(𝑏 ∈ (𝒫 𝑥 ∩ ∩ 𝑎) ↔ ∪ (𝑓 “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏) ↔ ∀𝑏 ∈ 𝒫 𝑥(𝑏 ∈ (𝒫 𝑥 ∩ ∩ 𝑎) ↔ ∪ ((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏)))
83	77, 82	anbi12d 630	. . . . . . 7 ⊢ (𝑓 = (𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) → ((𝑓:𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑏 ∈ 𝒫 𝑥(𝑏 ∈ (𝒫 𝑥 ∩ ∩ 𝑎) ↔ ∪ (𝑓 “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏)) ↔ ((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)):𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑏 ∈ 𝒫 𝑥(𝑏 ∈ (𝒫 𝑥 ∩ ∩ 𝑎) ↔ ∪ ((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏))))
84	35, 76, 83	spcedv 3527	. . . . . 6 ⊢ (𝑎 ⊆ (ACS‘𝑥) → ∃𝑓(𝑓:𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑏 ∈ 𝒫 𝑥(𝑏 ∈ (𝒫 𝑥 ∩ ∩ 𝑎) ↔ ∪ (𝑓 “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏)))
85		isacs 17277	. . . . . 6 ⊢ ((𝒫 𝑥 ∩ ∩ 𝑎) ∈ (ACS‘𝑥) ↔ ((𝒫 𝑥 ∩ ∩ 𝑎) ∈ (Moore‘𝑥) ∧ ∃𝑓(𝑓:𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑏 ∈ 𝒫 𝑥(𝑏 ∈ (𝒫 𝑥 ∩ ∩ 𝑎) ↔ ∪ (𝑓 “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏))))
86	18, 84, 85	sylanbrc 582	. . . . 5 ⊢ (𝑎 ⊆ (ACS‘𝑥) → (𝒫 𝑥 ∩ ∩ 𝑎) ∈ (ACS‘𝑥))
87	86	adantl 481	. . . 4 ⊢ ((⊤ ∧ 𝑎 ⊆ (ACS‘𝑥)) → (𝒫 𝑥 ∩ ∩ 𝑎) ∈ (ACS‘𝑥))
88	10, 87	ismred2 17229	. . 3 ⊢ (⊤ → (ACS‘𝑥) ∈ (Moore‘𝒫 𝑥))
89	88	mptru 1546	. 2 ⊢ (ACS‘𝑥) ∈ (Moore‘𝒫 𝑥)
90	4, 89	vtoclg 3495	1 ⊢ (𝑋 ∈ 𝑉 → (ACS‘𝑋) ∈ (Moore‘𝒫 𝑋))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   = wceq 1539  ⊤wtru 1540  ∃wex 1783   ∈ wcel 2108  ∀wral 3063  Vcvv 3422   ∩ cin 3882   ⊆ wss 3883  𝒫 cpw 4530  ∪ cuni 4836  ∩ cint 4876  ∪ ciun 4921   ↦ cmpt 5153   × cxp 5578   “ cima 5583  Fun wfun 6412  ⟶wf 6414  ‘cfv 6418  Fincfn 8691  Moorecmre 17208  mrClscmrc 17209  ACScacs 17211

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-int 4877  df-iun 4923  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-fv 6426  df-mre 17212  df-mrc 17213  df-acs 17215

This theorem is referenced by:  acsfn1  17287  acsfn1c  17288  acsfn2  17289  submacs  18380  subgacs  18704  nsgacs  18705  acsfn1p  19982  subrgacs  19983  sdrgacs  19984  lssacs  20144