Theorem mreacs 17032

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 6674	. . 3 ⊢ (𝑥 = 𝑋 → (ACS‘𝑥) = (ACS‘𝑋))
2		pweq 4504	. . . 4 ⊢ (𝑥 = 𝑋 → 𝒫 𝑥 = 𝒫 𝑋)
3	2	fveq2d 6678	. . 3 ⊢ (𝑥 = 𝑋 → (Moore‘𝒫 𝑥) = (Moore‘𝒫 𝑋))
4	1, 3	eleq12d 2827	. 2 ⊢ (𝑥 = 𝑋 → ((ACS‘𝑥) ∈ (Moore‘𝒫 𝑥) ↔ (ACS‘𝑋) ∈ (Moore‘𝒫 𝑋)))
5		acsmre 17026	. . . . . . 7 ⊢ (𝑎 ∈ (ACS‘𝑥) → 𝑎 ∈ (Moore‘𝑥))
6		mresspw 16966	. . . . . . . 8 ⊢ (𝑎 ∈ (Moore‘𝑥) → 𝑎 ⊆ 𝒫 𝑥)
7	5, 6	syl 17	. . . . . . 7 ⊢ (𝑎 ∈ (ACS‘𝑥) → 𝑎 ⊆ 𝒫 𝑥)
8	5, 7	elpwd 4496	. . . . . 6 ⊢ (𝑎 ∈ (ACS‘𝑥) → 𝑎 ∈ 𝒫 𝒫 𝑥)
9	8	ssriv 3881	. . . . 5 ⊢ (ACS‘𝑥) ⊆ 𝒫 𝒫 𝑥
10	9	a1i 11	. . . 4 ⊢ (⊤ → (ACS‘𝑥) ⊆ 𝒫 𝒫 𝑥)
11		vex 3402	. . . . . . . 8 ⊢ 𝑥 ∈ V
12		mremre 16978	. . . . . . . 8 ⊢ (𝑥 ∈ V → (Moore‘𝑥) ∈ (Moore‘𝒫 𝑥))
13	11, 12	mp1i 13	. . . . . . 7 ⊢ (𝑎 ⊆ (ACS‘𝑥) → (Moore‘𝑥) ∈ (Moore‘𝒫 𝑥))
14	5	ssriv 3881	. . . . . . . 8 ⊢ (ACS‘𝑥) ⊆ (Moore‘𝑥)
15		sstr 3885	. . . . . . . 8 ⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ (ACS‘𝑥) ⊆ (Moore‘𝑥)) → 𝑎 ⊆ (Moore‘𝑥))
16	14, 15	mpan2 691	. . . . . . 7 ⊢ (𝑎 ⊆ (ACS‘𝑥) → 𝑎 ⊆ (Moore‘𝑥))
17		mrerintcl 16971	. . . . . . 7 ⊢ (((Moore‘𝑥) ∈ (Moore‘𝒫 𝑥) ∧ 𝑎 ⊆ (Moore‘𝑥)) → (𝒫 𝑥 ∩ ∩ 𝑎) ∈ (Moore‘𝑥))
18	13, 16, 17	syl2anc 587	. . . . . 6 ⊢ (𝑎 ⊆ (ACS‘𝑥) → (𝒫 𝑥 ∩ ∩ 𝑎) ∈ (Moore‘𝑥))
19		ssel2 3872	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑑 ∈ 𝑎) → 𝑑 ∈ (ACS‘𝑥))
20	19	acsmred 17030	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑑 ∈ 𝑎) → 𝑑 ∈ (Moore‘𝑥))
21		eqid 2738	. . . . . . . . . . . . . . 15 ⊢ (mrCls‘𝑑) = (mrCls‘𝑑)
22	20, 21	mrcssvd 16997	. . . . . . . . . . . . . 14 ⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑑 ∈ 𝑎) → ((mrCls‘𝑑)‘𝑐) ⊆ 𝑥)
23	22	ralrimiva 3096	. . . . . . . . . . . . 13 ⊢ (𝑎 ⊆ (ACS‘𝑥) → ∀𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐) ⊆ 𝑥)
24	23	adantr 484	. . . . . . . . . . . 12 ⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑐 ∈ 𝒫 𝑥) → ∀𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐) ⊆ 𝑥)
25		iunss 4931	. . . . . . . . . . . 12 ⊢ (∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐) ⊆ 𝑥 ↔ ∀𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐) ⊆ 𝑥)
26	24, 25	sylibr 237	. . . . . . . . . . 11 ⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑐 ∈ 𝒫 𝑥) → ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐) ⊆ 𝑥)
27	11	elpw2 5213	. . . . . . . . . . 11 ⊢ (∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐) ∈ 𝒫 𝑥 ↔ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐) ⊆ 𝑥)
28	26, 27	sylibr 237	. . . . . . . . . 10 ⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑐 ∈ 𝒫 𝑥) → ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐) ∈ 𝒫 𝑥)
29	28	fmpttd 6889	. . . . . . . . 9 ⊢ (𝑎 ⊆ (ACS‘𝑥) → (𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)):𝒫 𝑥⟶𝒫 𝑥)
30		fssxp 6532	. . . . . . . . 9 ⊢ ((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)):𝒫 𝑥⟶𝒫 𝑥 → (𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) ⊆ (𝒫 𝑥 × 𝒫 𝑥))
31	29, 30	syl 17	. . . . . . . 8 ⊢ (𝑎 ⊆ (ACS‘𝑥) → (𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) ⊆ (𝒫 𝑥 × 𝒫 𝑥))
32		vpwex 5244	. . . . . . . . 9 ⊢ 𝒫 𝑥 ∈ V
33	32, 32	xpex 7494	. . . . . . . 8 ⊢ (𝒫 𝑥 × 𝒫 𝑥) ∈ V
34		ssexg 5191	. . . . . . . 8 ⊢ (((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) ⊆ (𝒫 𝑥 × 𝒫 𝑥) ∧ (𝒫 𝑥 × 𝒫 𝑥) ∈ V) → (𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) ∈ V)
35	31, 33, 34	sylancl 589	. . . . . . 7 ⊢ (𝑎 ⊆ (ACS‘𝑥) → (𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) ∈ V)
36	19	adantlr 715	. . . . . . . . . . . . 13 ⊢ (((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) ∧ 𝑑 ∈ 𝑎) → 𝑑 ∈ (ACS‘𝑥))
37		elpwi 4497	. . . . . . . . . . . . . 14 ⊢ (𝑏 ∈ 𝒫 𝑥 → 𝑏 ⊆ 𝑥)
38	37	ad2antlr 727	. . . . . . . . . . . . 13 ⊢ (((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) ∧ 𝑑 ∈ 𝑎) → 𝑏 ⊆ 𝑥)
39	21	acsfiel2 17029	. . . . . . . . . . . . 13 ⊢ ((𝑑 ∈ (ACS‘𝑥) ∧ 𝑏 ⊆ 𝑥) → (𝑏 ∈ 𝑑 ↔ ∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)((mrCls‘𝑑)‘𝑒) ⊆ 𝑏))
40	36, 38, 39	syl2anc 587	. . . . . . . . . . . 12 ⊢ (((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) ∧ 𝑑 ∈ 𝑎) → (𝑏 ∈ 𝑑 ↔ ∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)((mrCls‘𝑑)‘𝑒) ⊆ 𝑏))
41	40	ralbidva 3108	. . . . . . . . . . 11 ⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) → (∀𝑑 ∈ 𝑎 𝑏 ∈ 𝑑 ↔ ∀𝑑 ∈ 𝑎 ∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)((mrCls‘𝑑)‘𝑒) ⊆ 𝑏))
42		iunss 4931	. . . . . . . . . . . . 13 ⊢ (∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏 ↔ ∀𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏)
43	42	ralbii 3080	. . . . . . . . . . . 12 ⊢ (∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏 ↔ ∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)∀𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏)
44		ralcom 3258	. . . . . . . . . . . 12 ⊢ (∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)∀𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏 ↔ ∀𝑑 ∈ 𝑎 ∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)((mrCls‘𝑑)‘𝑒) ⊆ 𝑏)
45	43, 44	bitri 278	. . . . . . . . . . 11 ⊢ (∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏 ↔ ∀𝑑 ∈ 𝑎 ∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)((mrCls‘𝑑)‘𝑒) ⊆ 𝑏)
46	41, 45	bitr4di 292	. . . . . . . . . 10 ⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) → (∀𝑑 ∈ 𝑎 𝑏 ∈ 𝑑 ↔ ∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏))
47		elrint2 4880	. . . . . . . . . . 11 ⊢ (𝑏 ∈ 𝒫 𝑥 → (𝑏 ∈ (𝒫 𝑥 ∩ ∩ 𝑎) ↔ ∀𝑑 ∈ 𝑎 𝑏 ∈ 𝑑))
48	47	adantl 485	. . . . . . . . . 10 ⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) → (𝑏 ∈ (𝒫 𝑥 ∩ ∩ 𝑎) ↔ ∀𝑑 ∈ 𝑎 𝑏 ∈ 𝑑))
49		funmpt 6377	. . . . . . . . . . . . 13 ⊢ Fun (𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐))
50		funiunfv 7018	. . . . . . . . . . . . 13 ⊢ (Fun (𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) → ∪ 𝑒 ∈ (𝒫 𝑏 ∩ Fin)((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐))‘𝑒) = ∪ ((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)))
51	49, 50	ax-mp 5	. . . . . . . . . . . 12 ⊢ ∪ 𝑒 ∈ (𝒫 𝑏 ∩ Fin)((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐))‘𝑒) = ∪ ((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin))
52	51	sseq1i 3905	. . . . . . . . . . 11 ⊢ (∪ 𝑒 ∈ (𝒫 𝑏 ∩ Fin)((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐))‘𝑒) ⊆ 𝑏 ↔ ∪ ((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏)
53		iunss 4931	. . . . . . . . . . . 12 ⊢ (∪ 𝑒 ∈ (𝒫 𝑏 ∩ Fin)((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐))‘𝑒) ⊆ 𝑏 ↔ ∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐))‘𝑒) ⊆ 𝑏)
54		eqid 2738	. . . . . . . . . . . . . . 15 ⊢ (𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) = (𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐))
55		fveq2 6674	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 = 𝑒 → ((mrCls‘𝑑)‘𝑐) = ((mrCls‘𝑑)‘𝑒))
56	55	iuneq2d 4910	. . . . . . . . . . . . . . 15 ⊢ (𝑐 = 𝑒 → ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐) = ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒))
57		inss1 4119	. . . . . . . . . . . . . . . . 17 ⊢ (𝒫 𝑏 ∩ Fin) ⊆ 𝒫 𝑏
58	37	sspwd 4503	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 ∈ 𝒫 𝑥 → 𝒫 𝑏 ⊆ 𝒫 𝑥)
59	58	adantl 485	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) → 𝒫 𝑏 ⊆ 𝒫 𝑥)
60	57, 59	sstrid 3888	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) → (𝒫 𝑏 ∩ Fin) ⊆ 𝒫 𝑥)
61	60	sselda 3877	. . . . . . . . . . . . . . 15 ⊢ (((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) ∧ 𝑒 ∈ (𝒫 𝑏 ∩ Fin)) → 𝑒 ∈ 𝒫 𝑥)
62	20, 21	mrcssvd 16997	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑑 ∈ 𝑎) → ((mrCls‘𝑑)‘𝑒) ⊆ 𝑥)
63	62	ralrimiva 3096	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 ⊆ (ACS‘𝑥) → ∀𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑥)
64	63	ad2antrr 726	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) ∧ 𝑒 ∈ (𝒫 𝑏 ∩ Fin)) → ∀𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑥)
65		iunss 4931	. . . . . . . . . . . . . . . . 17 ⊢ (∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑥 ↔ ∀𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑥)
66	64, 65	sylibr 237	. . . . . . . . . . . . . . . 16 ⊢ (((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) ∧ 𝑒 ∈ (𝒫 𝑏 ∩ Fin)) → ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑥)
67		ssexg 5191	. . . . . . . . . . . . . . . 16 ⊢ ((∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑥 ∧ 𝑥 ∈ V) → ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ∈ V)
68	66, 11, 67	sylancl 589	. . . . . . . . . . . . . . 15 ⊢ (((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) ∧ 𝑒 ∈ (𝒫 𝑏 ∩ Fin)) → ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ∈ V)
69	54, 56, 61, 68	fvmptd3 6798	. . . . . . . . . . . . . 14 ⊢ (((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) ∧ 𝑒 ∈ (𝒫 𝑏 ∩ Fin)) → ((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐))‘𝑒) = ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒))
70	69	sseq1d 3908	. . . . . . . . . . . . 13 ⊢ (((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) ∧ 𝑒 ∈ (𝒫 𝑏 ∩ Fin)) → (((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐))‘𝑒) ⊆ 𝑏 ↔ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏))
71	70	ralbidva 3108	. . . . . . . . . . . 12 ⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) → (∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐))‘𝑒) ⊆ 𝑏 ↔ ∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏))
72	53, 71	syl5bb 286	. . . . . . . . . . 11 ⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) → (∪ 𝑒 ∈ (𝒫 𝑏 ∩ Fin)((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐))‘𝑒) ⊆ 𝑏 ↔ ∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏))
73	52, 72	bitr3id 288	. . . . . . . . . 10 ⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) → (∪ ((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏 ↔ ∀𝑒 ∈ (𝒫 𝑏 ∩ Fin)∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑒) ⊆ 𝑏))
74	46, 48, 73	3bitr4d 314	. . . . . . . . 9 ⊢ ((𝑎 ⊆ (ACS‘𝑥) ∧ 𝑏 ∈ 𝒫 𝑥) → (𝑏 ∈ (𝒫 𝑥 ∩ ∩ 𝑎) ↔ ∪ ((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏))
75	74	ralrimiva 3096	. . . . . . . 8 ⊢ (𝑎 ⊆ (ACS‘𝑥) → ∀𝑏 ∈ 𝒫 𝑥(𝑏 ∈ (𝒫 𝑥 ∩ ∩ 𝑎) ↔ ∪ ((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏))
76	29, 75	jca 515	. . . . . . 7 ⊢ (𝑎 ⊆ (ACS‘𝑥) → ((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)):𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑏 ∈ 𝒫 𝑥(𝑏 ∈ (𝒫 𝑥 ∩ ∩ 𝑎) ↔ ∪ ((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏)))
77		feq1 6485	. . . . . . . 8 ⊢ (𝑓 = (𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) → (𝑓:𝒫 𝑥⟶𝒫 𝑥 ↔ (𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)):𝒫 𝑥⟶𝒫 𝑥))
78		imaeq1 5898	. . . . . . . . . . . 12 ⊢ (𝑓 = (𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) → (𝑓 “ (𝒫 𝑏 ∩ Fin)) = ((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)))
79	78	unieqd 4810	. . . . . . . . . . 11 ⊢ (𝑓 = (𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) → ∪ (𝑓 “ (𝒫 𝑏 ∩ Fin)) = ∪ ((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)))
80	79	sseq1d 3908	. . . . . . . . . 10 ⊢ (𝑓 = (𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) → (∪ (𝑓 “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏 ↔ ∪ ((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏))
81	80	bibi2d 346	. . . . . . . . 9 ⊢ (𝑓 = (𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) → ((𝑏 ∈ (𝒫 𝑥 ∩ ∩ 𝑎) ↔ ∪ (𝑓 “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏) ↔ (𝑏 ∈ (𝒫 𝑥 ∩ ∩ 𝑎) ↔ ∪ ((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏)))
82	81	ralbidv 3109	. . . . . . . 8 ⊢ (𝑓 = (𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) → (∀𝑏 ∈ 𝒫 𝑥(𝑏 ∈ (𝒫 𝑥 ∩ ∩ 𝑎) ↔ ∪ (𝑓 “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏) ↔ ∀𝑏 ∈ 𝒫 𝑥(𝑏 ∈ (𝒫 𝑥 ∩ ∩ 𝑎) ↔ ∪ ((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏)))
83	77, 82	anbi12d 634	. . . . . . 7 ⊢ (𝑓 = (𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) → ((𝑓:𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑏 ∈ 𝒫 𝑥(𝑏 ∈ (𝒫 𝑥 ∩ ∩ 𝑎) ↔ ∪ (𝑓 “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏)) ↔ ((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)):𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑏 ∈ 𝒫 𝑥(𝑏 ∈ (𝒫 𝑥 ∩ ∩ 𝑎) ↔ ∪ ((𝑐 ∈ 𝒫 𝑥 ↦ ∪ 𝑑 ∈ 𝑎 ((mrCls‘𝑑)‘𝑐)) “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏))))
84	35, 76, 83	spcedv 3502	. . . . . 6 ⊢ (𝑎 ⊆ (ACS‘𝑥) → ∃𝑓(𝑓:𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑏 ∈ 𝒫 𝑥(𝑏 ∈ (𝒫 𝑥 ∩ ∩ 𝑎) ↔ ∪ (𝑓 “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏)))
85		isacs 17025	. . . . . 6 ⊢ ((𝒫 𝑥 ∩ ∩ 𝑎) ∈ (ACS‘𝑥) ↔ ((𝒫 𝑥 ∩ ∩ 𝑎) ∈ (Moore‘𝑥) ∧ ∃𝑓(𝑓:𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑏 ∈ 𝒫 𝑥(𝑏 ∈ (𝒫 𝑥 ∩ ∩ 𝑎) ↔ ∪ (𝑓 “ (𝒫 𝑏 ∩ Fin)) ⊆ 𝑏))))
86	18, 84, 85	sylanbrc 586	. . . . 5 ⊢ (𝑎 ⊆ (ACS‘𝑥) → (𝒫 𝑥 ∩ ∩ 𝑎) ∈ (ACS‘𝑥))
87	86	adantl 485	. . . 4 ⊢ ((⊤ ∧ 𝑎 ⊆ (ACS‘𝑥)) → (𝒫 𝑥 ∩ ∩ 𝑎) ∈ (ACS‘𝑥))
88	10, 87	ismred2 16977	. . 3 ⊢ (⊤ → (ACS‘𝑥) ∈ (Moore‘𝒫 𝑥))
89	88	mptru 1549	. 2 ⊢ (ACS‘𝑥) ∈ (Moore‘𝒫 𝑥)
90	4, 89	vtoclg 3470	1 ⊢ (𝑋 ∈ 𝑉 → (ACS‘𝑋) ∈ (Moore‘𝒫 𝑋))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1542  ⊤wtru 1543  ∃wex 1786   ∈ wcel 2114  ∀wral 3053  Vcvv 3398   ∩ cin 3842   ⊆ wss 3843  𝒫 cpw 4488  ∪ cuni 4796  ∩ cint 4836  ∪ ciun 4881   ↦ cmpt 5110   × cxp 5523   “ cima 5528  Fun wfun 6333  ⟶wf 6335  ‘cfv 6339  Fincfn 8555  Moorecmre 16956  mrClscmrc 16957  ACScacs 16959

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2162  ax-12 2179  ax-ext 2710  ax-sep 5167  ax-nul 5174  ax-pow 5232  ax-pr 5296  ax-un 7479

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2075  df-mo 2540  df-eu 2570  df-clab 2717  df-cleq 2730  df-clel 2811  df-nfc 2881  df-ne 2935  df-ral 3058  df-rex 3059  df-rab 3062  df-v 3400  df-sbc 3681  df-csb 3791  df-dif 3846  df-un 3848  df-in 3850  df-ss 3860  df-nul 4212  df-if 4415  df-pw 4490  df-sn 4517  df-pr 4519  df-op 4523  df-uni 4797  df-int 4837  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-id 5429  df-xp 5531  df-rel 5532  df-cnv 5533  df-co 5534  df-dm 5535  df-rn 5536  df-res 5537  df-ima 5538  df-iota 6297  df-fun 6341  df-fn 6342  df-f 6343  df-fv 6347  df-mre 16960  df-mrc 16961  df-acs 16963

This theorem is referenced by:  acsfn1  17035  acsfn1c  17036  acsfn2  17037  submacs  18107  subgacs  18431  nsgacs  18432  acsfn1p  19697  subrgacs  19698  sdrgacs  19699  lssacs  19858