Theorem mreacs 17572

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 6831	. . 3 ⊢ (𝑥 = 𝑋 → (ACS‘𝑥) = (ACS‘𝑋))
2		pweq 4565	. . . 4 ⊢ (𝑥 = 𝑋 → 𝒫 𝑥 = 𝒫 𝑋)
3	2	fveq2d 6835	. . 3 ⊢ (𝑥 = 𝑋 → (Moore‘𝒫 𝑥) = (Moore‘𝒫 𝑋))
4	1, 3	eleq12d 2827	. 2 ⊢ (𝑥 = 𝑋 → ((ACS‘𝑥) ∈ (Moore‘𝒫 𝑥) ↔ (ACS‘𝑋) ∈ (Moore‘𝒫 𝑋)))
5		acsmre 17566	. . . . . . 7 ⊢ (𝑎 ∈ (ACS‘𝑥) → 𝑎 ∈ (Moore‘𝑥))
6		mresspw 17502	. . . . . . . 8 ⊢ (𝑎 ∈ (Moore‘𝑥) → 𝑎 ⊆ 𝒫 𝑥)
7	5, 6	syl 17	. . . . . . 7 ⊢ (𝑎 ∈ (ACS‘𝑥) → 𝑎 ⊆ 𝒫 𝑥)
8	5, 7	elpwd 4557	. . . . . 6 ⊢ (𝑎 ∈ (ACS‘𝑥) → 𝑎 ∈ 𝒫 𝒫 𝑥)
9	8	ssriv 3934	. . . . 5 ⊢ (ACS‘𝑥) ⊆ 𝒫 𝒫 𝑥
10	9	a1i 11	. . . 4 ⊢ (⊤ → (ACS‘𝑥) ⊆ 𝒫 𝒫 𝑥)
11		vex 3441	. . . . . . . 8 ⊢ 𝑥 ∈ V
12		mremre 17514	. . . . . . . 8 ⊢ (𝑥 ∈ V → (Moore‘𝑥) ∈ (Moore‘𝒫 𝑥))
13	11, 12	mp1i 13	. . . . . . 7 ⊢ (𝑎 ⊆ (ACS‘𝑥) → (Moore‘𝑥) ∈ (Moore‘𝒫 𝑥))
14	5	ssriv 3934	. . . . . . . 8 ⊢ (ACS‘𝑥) ⊆ (Moore‘𝑥)
15		sstr 3939	. . . . . . . 8 ⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ (ACS‘𝑥) ⊆ (Moore‘𝑥)) → 𝑎 ⊆ (Moore‘𝑥))
16	14, 15	mpan2 691	. . . . . . 7 ⊢ (𝑎 ⊆ (ACS‘𝑥) → 𝑎 ⊆ (Moore‘𝑥))
17		mrerintcl 17507	. . . . . . 7 ⊢ (((Moore‘𝑥) ∈ (Moore‘𝒫 𝑥) ∧ 𝑎 ⊆ (Moore‘𝑥)) → (𝒫 𝑥 ∩ ∩ 𝑎) ∈ (Moore‘𝑥))
18	13, 16, 17	syl2anc 584	. . . . . 6 ⊢ (𝑎 ⊆ (ACS‘𝑥) → (𝒫 𝑥 ∩ ∩ 𝑎) ∈ (Moore‘𝑥))
19		ssel2 3925	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑑 ∈ 𝑎) → 𝑑 ∈ (ACS‘𝑥))
20	19	acsmred 17570	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑑 ∈ 𝑎) → 𝑑 ∈ (Moore‘𝑥))
21		eqid 2733	. . . . . . . . . . . . . . 15 ⊢ (mrCls‘𝑑) = (mrCls‘𝑑)
22	20, 21	mrcssvd 17537	. . . . . . . . . . . . . 14 ⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑑 ∈ 𝑎) → ((mrCls‘𝑑)‘𝑐) ⊆ 𝑥)
23	22	ralrimiva 3125	. . . . . . . . . . . . 13 ⊢ (𝑎 ⊆ (ACS‘𝑥) → ∀𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐) ⊆ 𝑥)
24	23	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑐 ∈ 𝒫 𝑥) → ∀𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐) ⊆ 𝑥)
25		iunss 4997	. . . . . . . . . . . 12 ⊢ (∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐) ⊆ 𝑥 ↔ ∀𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐) ⊆ 𝑥)
26	24, 25	sylibr 234	. . . . . . . . . . 11 ⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑐 ∈ 𝒫 𝑥) → ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐) ⊆ 𝑥)
27	11	elpw2 5276	. . . . . . . . . . 11 ⊢ (∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐) ∈ 𝒫 𝑥 ↔ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐) ⊆ 𝑥)
28	26, 27	sylibr 234	. . . . . . . . . 10 ⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑐 ∈ 𝒫 𝑥) → ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐) ∈ 𝒫 𝑥)
29	28	fmpttd 7057	. . . . . . . . 9 ⊢ (𝑎 ⊆ (ACS‘𝑥) → (𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)):𝒫 𝑥⟶𝒫 𝑥)
30		fssxp 6686	. . . . . . . . 9 ⊢ ((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)):𝒫 𝑥⟶𝒫 𝑥 → (𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) ⊆ (𝒫 𝑥 × 𝒫 𝑥))
31	29, 30	syl 17	. . . . . . . 8 ⊢ (𝑎 ⊆ (ACS‘𝑥) → (𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) ⊆ (𝒫 𝑥 × 𝒫 𝑥))
32		vpwex 5319	. . . . . . . . 9 ⊢ 𝒫 𝑥 ∈ V
33	32, 32	xpex 7695	. . . . . . . 8 ⊢ (𝒫 𝑥 × 𝒫 𝑥) ∈ V
34		ssexg 5265	. . . . . . . 8 ⊢ (((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) ⊆ (𝒫 𝑥 × 𝒫 𝑥) ∧ (𝒫 𝑥 × 𝒫 𝑥) ∈ V) → (𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) ∈ V)
35	31, 33, 34	sylancl 586	. . . . . . 7 ⊢ (𝑎 ⊆ (ACS‘𝑥) → (𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) ∈ V)
36	19	adantlr 715	. . . . . . . . . . . . 13 ⊢ (((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) ∧ 𝑑 ∈ 𝑎) → 𝑑 ∈ (ACS‘𝑥))
37		elpwi 4558	. . . . . . . . . . . . . 14 ⊢ (𝑏 ∈ 𝒫 𝑥 → 𝑏 ⊆ 𝑥)
38	37	ad2antlr 727	. . . . . . . . . . . . 13 ⊢ (((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) ∧ 𝑑 ∈ 𝑎) → 𝑏 ⊆ 𝑥)
39	21	acsfiel2 17569	. . . . . . . . . . . . 13 ⊢ ((𝑑 ∈ (ACS‘𝑥) ∧ 𝑏 ⊆ 𝑥) → (𝑏 ∈ 𝑑 ↔ ∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)((mrCls‘𝑑)‘𝑒) ⊆ 𝑏))
40	36, 38, 39	syl2anc 584	. . . . . . . . . . . 12 ⊢ (((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) ∧ 𝑑 ∈ 𝑎) → (𝑏 ∈ 𝑑 ↔ ∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)((mrCls‘𝑑)‘𝑒) ⊆ 𝑏))
41	40	ralbidva 3154	. . . . . . . . . . 11 ⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) → (∀𝑑 ∈ 𝑎 𝑏 ∈ 𝑑 ↔ ∀𝑑 ∈ 𝑎 ∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)((mrCls‘𝑑)‘𝑒) ⊆ 𝑏))
42		iunss 4997	. . . . . . . . . . . . 13 ⊢ (∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏 ↔ ∀𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏)
43	42	ralbii 3079	. . . . . . . . . . . 12 ⊢ (∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏 ↔ ∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)∀𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏)
44		ralcom 3261	. . . . . . . . . . . 12 ⊢ (∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)∀𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏 ↔ ∀𝑑 ∈ 𝑎 ∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)((mrCls‘𝑑)‘𝑒) ⊆ 𝑏)
45	43, 44	bitri 275	. . . . . . . . . . 11 ⊢ (∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏 ↔ ∀𝑑 ∈ 𝑎 ∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)((mrCls‘𝑑)‘𝑒) ⊆ 𝑏)
46	41, 45	bitr4di 289	. . . . . . . . . 10 ⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) → (∀𝑑 ∈ 𝑎 𝑏 ∈ 𝑑 ↔ ∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏))
47		elrint2 4942	. . . . . . . . . . 11 ⊢ (𝑏 ∈ 𝒫 𝑥 → (𝑏 ∈ (𝒫 𝑥 ∩ ∩ 𝑎) ↔ ∀𝑑 ∈ 𝑎 𝑏 ∈ 𝑑))
48	47	adantl 481	. . . . . . . . . 10 ⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) → (𝑏 ∈ (𝒫 𝑥 ∩ ∩ 𝑎) ↔ ∀𝑑 ∈ 𝑎 𝑏 ∈ 𝑑))
49		funmpt 6527	. . . . . . . . . . . . 13 ⊢ Fun (𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐))
50		funiunfv 7191	. . . . . . . . . . . . 13 ⊢ (Fun (𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) → ∪ 𝑒 ∈ (𝒫 𝑏 ∩ Fin)((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐))‘𝑒) = ∪ ((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)))
51	49, 50	ax-mp 5	. . . . . . . . . . . 12 ⊢ ∪ 𝑒 ∈ (𝒫 𝑏 ∩ Fin)((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐))‘𝑒) = ∪ ((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin))
52	51	sseq1i 3959	. . . . . . . . . . 11 ⊢ (∪ 𝑒 ∈ (𝒫 𝑏 ∩ Fin)((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐))‘𝑒) ⊆ 𝑏 ↔ ∪ ((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏)
53		iunss 4997	. . . . . . . . . . . 12 ⊢ (∪ 𝑒 ∈ (𝒫 𝑏 ∩ Fin)((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐))‘𝑒) ⊆ 𝑏 ↔ ∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐))‘𝑒) ⊆ 𝑏)
54		eqid 2733	. . . . . . . . . . . . . . 15 ⊢ (𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) = (𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐))
55		fveq2 6831	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 = 𝑒 → ((mrCls‘𝑑)‘𝑐) = ((mrCls‘𝑑)‘𝑒))
56	55	iuneq2d 4974	. . . . . . . . . . . . . . 15 ⊢ (𝑐 = 𝑒 → ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐) = ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒))
57		inss1 4186	. . . . . . . . . . . . . . . . 17 ⊢ (𝒫 𝑏 ∩ Fin) ⊆ 𝒫 𝑏
58	37	sspwd 4564	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 ∈ 𝒫 𝑥 → 𝒫 𝑏 ⊆ 𝒫 𝑥)
59	58	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) → 𝒫 𝑏 ⊆ 𝒫 𝑥)
60	57, 59	sstrid 3942	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) → (𝒫 𝑏 ∩ Fin) ⊆ 𝒫 𝑥)
61	60	sselda 3930	. . . . . . . . . . . . . . 15 ⊢ (((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) ∧ 𝑒 ∈ (𝒫 𝑏 ∩ Fin)) → 𝑒 ∈ 𝒫 𝑥)
62	20, 21	mrcssvd 17537	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑑 ∈ 𝑎) → ((mrCls‘𝑑)‘𝑒) ⊆ 𝑥)
63	62	ralrimiva 3125	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 ⊆ (ACS‘𝑥) → ∀𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑥)
64	63	ad2antrr 726	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) ∧ 𝑒 ∈ (𝒫 𝑏 ∩ Fin)) → ∀𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑥)
65		iunss 4997	. . . . . . . . . . . . . . . . 17 ⊢ (∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑥 ↔ ∀𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑥)
66	64, 65	sylibr 234	. . . . . . . . . . . . . . . 16 ⊢ (((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) ∧ 𝑒 ∈ (𝒫 𝑏 ∩ Fin)) → ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑥)
67		ssexg 5265	. . . . . . . . . . . . . . . 16 ⊢ ((∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑥 ∧ 𝑥 ∈ V) → ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ∈ V)
68	66, 11, 67	sylancl 586	. . . . . . . . . . . . . . 15 ⊢ (((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) ∧ 𝑒 ∈ (𝒫 𝑏 ∩ Fin)) → ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ∈ V)
69	54, 56, 61, 68	fvmptd3 6961	. . . . . . . . . . . . . 14 ⊢ (((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) ∧ 𝑒 ∈ (𝒫 𝑏 ∩ Fin)) → ((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐))‘𝑒) = ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒))
70	69	sseq1d 3962	. . . . . . . . . . . . 13 ⊢ (((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) ∧ 𝑒 ∈ (𝒫 𝑏 ∩ Fin)) → (((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐))‘𝑒) ⊆ 𝑏 ↔ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏))
71	70	ralbidva 3154	. . . . . . . . . . . 12 ⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) → (∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐))‘𝑒) ⊆ 𝑏 ↔ ∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏))
72	53, 71	bitrid 283	. . . . . . . . . . 11 ⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) → (∪ 𝑒 ∈ (𝒫 𝑏 ∩ Fin)((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐))‘𝑒) ⊆ 𝑏 ↔ ∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏))
73	52, 72	bitr3id 285	. . . . . . . . . 10 ⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) → (∪ ((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏 ↔ ∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏))
74	46, 48, 73	3bitr4d 311	. . . . . . . . 9 ⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) → (𝑏 ∈ (𝒫 𝑥 ∩ ∩ 𝑎) ↔ ∪ ((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏))
75	74	ralrimiva 3125	. . . . . . . 8 ⊢ (𝑎 ⊆ (ACS‘𝑥) → ∀𝑏 ∈ 𝒫 𝑥(𝑏 ∈ (𝒫 𝑥 ∩ ∩ 𝑎) ↔ ∪ ((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏))
76	29, 75	jca 511	. . . . . . 7 ⊢ (𝑎 ⊆ (ACS‘𝑥) → ((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)):𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑏 ∈ 𝒫 𝑥(𝑏 ∈ (𝒫 𝑥 ∩ ∩ 𝑎) ↔ ∪ ((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏)))
77		feq1 6637	. . . . . . . 8 ⊢ (𝑓 = (𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) → (𝑓:𝒫 𝑥⟶𝒫 𝑥 ↔ (𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)):𝒫 𝑥⟶𝒫 𝑥))
78		imaeq1 6011	. . . . . . . . . . . 12 ⊢ (𝑓 = (𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) → (𝑓 “ (𝒫 𝑏 ∩ Fin)) = ((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)))
79	78	unieqd 4873	. . . . . . . . . . 11 ⊢ (𝑓 = (𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) → ∪ (𝑓 “ (𝒫 𝑏 ∩ Fin)) = ∪ ((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)))
80	79	sseq1d 3962	. . . . . . . . . 10 ⊢ (𝑓 = (𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) → (∪ (𝑓 “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏 ↔ ∪ ((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏))
81	80	bibi2d 342	. . . . . . . . 9 ⊢ (𝑓 = (𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) → ((𝑏 ∈ (𝒫 𝑥 ∩ ∩ 𝑎) ↔ ∪ (𝑓 “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏) ↔ (𝑏 ∈ (𝒫 𝑥 ∩ ∩ 𝑎) ↔ ∪ ((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏)))
82	81	ralbidv 3156	. . . . . . . 8 ⊢ (𝑓 = (𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) → (∀𝑏 ∈ 𝒫 𝑥(𝑏 ∈ (𝒫 𝑥 ∩ ∩ 𝑎) ↔ ∪ (𝑓 “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏) ↔ ∀𝑏 ∈ 𝒫 𝑥(𝑏 ∈ (𝒫 𝑥 ∩ ∩ 𝑎) ↔ ∪ ((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏)))
83	77, 82	anbi12d 632	. . . . . . 7 ⊢ (𝑓 = (𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) → ((𝑓:𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑏 ∈ 𝒫 𝑥(𝑏 ∈ (𝒫 𝑥 ∩ ∩ 𝑎) ↔ ∪ (𝑓 “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏)) ↔ ((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)):𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑏 ∈ 𝒫 𝑥(𝑏 ∈ (𝒫 𝑥 ∩ ∩ 𝑎) ↔ ∪ ((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏))))
84	35, 76, 83	spcedv 3549	. . . . . 6 ⊢ (𝑎 ⊆ (ACS‘𝑥) → ∃𝑓(𝑓:𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑏 ∈ 𝒫 𝑥(𝑏 ∈ (𝒫 𝑥 ∩ ∩ 𝑎) ↔ ∪ (𝑓 “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏)))
85		isacs 17565	. . . . . 6 ⊢ ((𝒫 𝑥 ∩ ∩ 𝑎) ∈ (ACS‘𝑥) ↔ ((𝒫 𝑥 ∩ ∩ 𝑎) ∈ (Moore‘𝑥) ∧ ∃𝑓(𝑓:𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑏 ∈ 𝒫 𝑥(𝑏 ∈ (𝒫 𝑥 ∩ ∩ 𝑎) ↔ ∪ (𝑓 “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏))))
86	18, 84, 85	sylanbrc 583	. . . . 5 ⊢ (𝑎 ⊆ (ACS‘𝑥) → (𝒫 𝑥 ∩ ∩ 𝑎) ∈ (ACS‘𝑥))
87	86	adantl 481	. . . 4 ⊢ ((⊤ ∧ 𝑎 ⊆ (ACS‘𝑥)) → (𝒫 𝑥 ∩ ∩ 𝑎) ∈ (ACS‘𝑥))
88	10, 87	ismred2 17513	. . 3 ⊢ (⊤ → (ACS‘𝑥) ∈ (Moore‘𝒫 𝑥))
89	88	mptru 1548	. 2 ⊢ (ACS‘𝑥) ∈ (Moore‘𝒫 𝑥)
90	4, 89	vtoclg 3508	1 ⊢ (𝑋 ∈ 𝑉 → (ACS‘𝑋) ∈ (Moore‘𝒫 𝑋))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541  ⊤wtru 1542  ∃wex 1780   ∈ wcel 2113  ∀wral 3048  Vcvv 3437   ∩ cin 3897   ⊆ wss 3898  𝒫 cpw 4551  ∪ cuni 4860  ∩ cint 4899  ∪ ciun 4943   ↦ cmpt 5176   × cxp 5619   “ cima 5624  Fun wfun 6483  ⟶wf 6485  ‘cfv 6489  Fincfn 8879  Moorecmre 17492  mrClscmrc 17493  ACScacs 17495

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7677

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-sbc 3738  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-int 4900  df-iun 4945  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5516  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-iota 6445  df-fun 6491  df-fn 6492  df-f 6493  df-fv 6497  df-mre 17496  df-mrc 17497  df-acs 17499

This theorem is referenced by:  acsfn1  17575  acsfn1c  17576  acsfn2  17577  submacs  18743  subgacs  19081  nsgacs  19082  acsfn1p  20723  subrgacs  20724  sdrgacs  20725  lssacs  20909