Metamath Proof Explorer

Theorem ismrcd1

Description: Any function from the subsets of a set to itself, which is extensive (satisfies mrcssid ), isotone (satisfies mrcss ), and idempotent (satisfies mrcidm ) has a collection of fixed points which is a Moore collection, and itself is the closure operator for that collection. This can be taken as an alternate definition for the closure operators. This is the first half, ismrcd2 is the second. (Contributed by Stefan O'Rear, 1-Feb-2015)

Ref Expression
Hypotheses ismrcd.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
ismrcd.f ⊢ ( 𝜑 → 𝐹 : 𝒫 𝐵 ⟶ 𝒫 𝐵 )
ismrcd.e ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ 𝐵 ) → 𝑥 ⊆ ( 𝐹 ‘ 𝑥 ) )
ismrcd.m ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥 ) → ( 𝐹 ‘ 𝑦 ) ⊆ ( 𝐹 ‘ 𝑥 ) )
ismrcd.i ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ 𝐵 ) → ( 𝐹 ‘ ( 𝐹 ‘ 𝑥 ) ) = ( 𝐹 ‘ 𝑥 ) )
Assertion ismrcd1 ( 𝜑 → dom ( 𝐹 ∩ I ) ∈ ( Moore ‘ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 ismrcd.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
2 ismrcd.f ⊢ ( 𝜑 → 𝐹 : 𝒫 𝐵 ⟶ 𝒫 𝐵 )
3 ismrcd.e ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ 𝐵 ) → 𝑥 ⊆ ( 𝐹 ‘ 𝑥 ) )
4 ismrcd.m ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥 ) → ( 𝐹 ‘ 𝑦 ) ⊆ ( 𝐹 ‘ 𝑥 ) )
5 ismrcd.i ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ 𝐵 ) → ( 𝐹 ‘ ( 𝐹 ‘ 𝑥 ) ) = ( 𝐹 ‘ 𝑥 ) )
6 inss1 ⊢ ( 𝐹 ∩ I ) ⊆ 𝐹
7 dmss ⊢ ( ( 𝐹 ∩ I ) ⊆ 𝐹 → dom ( 𝐹 ∩ I ) ⊆ dom 𝐹 )
8 6 7 ax-mp ⊢ dom ( 𝐹 ∩ I ) ⊆ dom 𝐹
9 8 2 fssdm ⊢ ( 𝜑 → dom ( 𝐹 ∩ I ) ⊆ 𝒫 𝐵 )
10 ssid ⊢ 𝐵 ⊆ 𝐵
11 elpwg ⊢ ( 𝐵 ∈ 𝑉 → ( 𝐵 ∈ 𝒫 𝐵 ↔ 𝐵 ⊆ 𝐵 ) )
12 1 11 syl ⊢ ( 𝜑 → ( 𝐵 ∈ 𝒫 𝐵 ↔ 𝐵 ⊆ 𝐵 ) )
13 10 12 mpbiri ⊢ ( 𝜑 → 𝐵 ∈ 𝒫 𝐵 )
14 2 13 ffvelrnd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐵 ) ∈ 𝒫 𝐵 )
15 14 elpwid ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐵 ) ⊆ 𝐵 )
16 velpw ⊢ ( 𝑥 ∈ 𝒫 𝐵 ↔ 𝑥 ⊆ 𝐵 )
17 16 3 sylan2b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 𝐵 ) → 𝑥 ⊆ ( 𝐹 ‘ 𝑥 ) )
18 17 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝒫 𝐵 𝑥 ⊆ ( 𝐹 ‘ 𝑥 ) )
19 id ⊢ ( 𝑥 = 𝐵 → 𝑥 = 𝐵 )
20 fveq2 ⊢ ( 𝑥 = 𝐵 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝐵 ) )
21 19 20 sseq12d ⊢ ( 𝑥 = 𝐵 → ( 𝑥 ⊆ ( 𝐹 ‘ 𝑥 ) ↔ 𝐵 ⊆ ( 𝐹 ‘ 𝐵 ) ) )
22 21 rspcva ⊢ ( ( 𝐵 ∈ 𝒫 𝐵 ∧ ∀ 𝑥 ∈ 𝒫 𝐵 𝑥 ⊆ ( 𝐹 ‘ 𝑥 ) ) → 𝐵 ⊆ ( 𝐹 ‘ 𝐵 ) )
23 13 18 22 syl2anc ⊢ ( 𝜑 → 𝐵 ⊆ ( 𝐹 ‘ 𝐵 ) )
24 15 23 eqssd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐵 ) = 𝐵 )
25 2 ffnd ⊢ ( 𝜑 → 𝐹 Fn 𝒫 𝐵 )
26 fnelfp ⊢ ( ( 𝐹 Fn 𝒫 𝐵 ∧ 𝐵 ∈ 𝒫 𝐵 ) → ( 𝐵 ∈ dom ( 𝐹 ∩ I ) ↔ ( 𝐹 ‘ 𝐵 ) = 𝐵 ) )
27 25 13 26 syl2anc ⊢ ( 𝜑 → ( 𝐵 ∈ dom ( 𝐹 ∩ I ) ↔ ( 𝐹 ‘ 𝐵 ) = 𝐵 ) )
28 24 27 mpbird ⊢ ( 𝜑 → 𝐵 ∈ dom ( 𝐹 ∩ I ) )
29 simp2 ⊢ ( ( 𝜑 ∧ 𝑧 ⊆ dom ( 𝐹 ∩ I ) ∧ 𝑧 ≠ ∅ ) → 𝑧 ⊆ dom ( 𝐹 ∩ I ) )
30 9 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑧 ⊆ dom ( 𝐹 ∩ I ) ∧ 𝑧 ≠ ∅ ) → dom ( 𝐹 ∩ I ) ⊆ 𝒫 𝐵 )
31 29 30 sstrd ⊢ ( ( 𝜑 ∧ 𝑧 ⊆ dom ( 𝐹 ∩ I ) ∧ 𝑧 ≠ ∅ ) → 𝑧 ⊆ 𝒫 𝐵 )
32 simp3 ⊢ ( ( 𝜑 ∧ 𝑧 ⊆ dom ( 𝐹 ∩ I ) ∧ 𝑧 ≠ ∅ ) → 𝑧 ≠ ∅ )
33 intssuni2 ⊢ ( ( 𝑧 ⊆ 𝒫 𝐵 ∧ 𝑧 ≠ ∅ ) → ∩ 𝑧 ⊆ ∪ 𝒫 𝐵 )
34 31 32 33 syl2anc ⊢ ( ( 𝜑 ∧ 𝑧 ⊆ dom ( 𝐹 ∩ I ) ∧ 𝑧 ≠ ∅ ) → ∩ 𝑧 ⊆ ∪ 𝒫 𝐵 )
35 unipw ⊢ ∪ 𝒫 𝐵 = 𝐵
36 34 35 sseqtrdi ⊢ ( ( 𝜑 ∧ 𝑧 ⊆ dom ( 𝐹 ∩ I ) ∧ 𝑧 ≠ ∅ ) → ∩ 𝑧 ⊆ 𝐵 )
37 intex ⊢ ( 𝑧 ≠ ∅ ↔ ∩ 𝑧 ∈ V )
38 elpwg ⊢ ( ∩ 𝑧 ∈ V → ( ∩ 𝑧 ∈ 𝒫 𝐵 ↔ ∩ 𝑧 ⊆ 𝐵 ) )
39 37 38 sylbi ⊢ ( 𝑧 ≠ ∅ → ( ∩ 𝑧 ∈ 𝒫 𝐵 ↔ ∩ 𝑧 ⊆ 𝐵 ) )
40 39 3ad2ant3 ⊢ ( ( 𝜑 ∧ 𝑧 ⊆ dom ( 𝐹 ∩ I ) ∧ 𝑧 ≠ ∅ ) → ( ∩ 𝑧 ∈ 𝒫 𝐵 ↔ ∩ 𝑧 ⊆ 𝐵 ) )
41 36 40 mpbird ⊢ ( ( 𝜑 ∧ 𝑧 ⊆ dom ( 𝐹 ∩ I ) ∧ 𝑧 ≠ ∅ ) → ∩ 𝑧 ∈ 𝒫 𝐵 )
42 41 adantr ⊢ ( ( ( 𝜑 ∧ 𝑧 ⊆ dom ( 𝐹 ∩ I ) ∧ 𝑧 ≠ ∅ ) ∧ 𝑥 ∈ 𝑧 ) → ∩ 𝑧 ∈ 𝒫 𝐵 )
43 4 3expib ⊢ ( 𝜑 → ( ( 𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥 ) → ( 𝐹 ‘ 𝑦 ) ⊆ ( 𝐹 ‘ 𝑥 ) ) )
44 43 alrimiv ⊢ ( 𝜑 → ∀ 𝑦 ( ( 𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥 ) → ( 𝐹 ‘ 𝑦 ) ⊆ ( 𝐹 ‘ 𝑥 ) ) )
45 44 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑧 ⊆ dom ( 𝐹 ∩ I ) ∧ 𝑧 ≠ ∅ ) → ∀ 𝑦 ( ( 𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥 ) → ( 𝐹 ‘ 𝑦 ) ⊆ ( 𝐹 ‘ 𝑥 ) ) )
46 45 adantr ⊢ ( ( ( 𝜑 ∧ 𝑧 ⊆ dom ( 𝐹 ∩ I ) ∧ 𝑧 ≠ ∅ ) ∧ 𝑥 ∈ 𝑧 ) → ∀ 𝑦 ( ( 𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥 ) → ( 𝐹 ‘ 𝑦 ) ⊆ ( 𝐹 ‘ 𝑥 ) ) )
47 31 sselda ⊢ ( ( ( 𝜑 ∧ 𝑧 ⊆ dom ( 𝐹 ∩ I ) ∧ 𝑧 ≠ ∅ ) ∧ 𝑥 ∈ 𝑧 ) → 𝑥 ∈ 𝒫 𝐵 )
48 47 elpwid ⊢ ( ( ( 𝜑 ∧ 𝑧 ⊆ dom ( 𝐹 ∩ I ) ∧ 𝑧 ≠ ∅ ) ∧ 𝑥 ∈ 𝑧 ) → 𝑥 ⊆ 𝐵 )
49 intss1 ⊢ ( 𝑥 ∈ 𝑧 → ∩ 𝑧 ⊆ 𝑥 )
50 49 adantl ⊢ ( ( ( 𝜑 ∧ 𝑧 ⊆ dom ( 𝐹 ∩ I ) ∧ 𝑧 ≠ ∅ ) ∧ 𝑥 ∈ 𝑧 ) → ∩ 𝑧 ⊆ 𝑥 )
51 48 50 jca ⊢ ( ( ( 𝜑 ∧ 𝑧 ⊆ dom ( 𝐹 ∩ I ) ∧ 𝑧 ≠ ∅ ) ∧ 𝑥 ∈ 𝑧 ) → ( 𝑥 ⊆ 𝐵 ∧ ∩ 𝑧 ⊆ 𝑥 ) )
52 sseq1 ⊢ ( 𝑦 = ∩ 𝑧 → ( 𝑦 ⊆ 𝑥 ↔ ∩ 𝑧 ⊆ 𝑥 ) )
53 52 anbi2d ⊢ ( 𝑦 = ∩ 𝑧 → ( ( 𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥 ) ↔ ( 𝑥 ⊆ 𝐵 ∧ ∩ 𝑧 ⊆ 𝑥 ) ) )
54 fveq2 ⊢ ( 𝑦 = ∩ 𝑧 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ ∩ 𝑧 ) )
55 54 sseq1d ⊢ ( 𝑦 = ∩ 𝑧 → ( ( 𝐹 ‘ 𝑦 ) ⊆ ( 𝐹 ‘ 𝑥 ) ↔ ( 𝐹 ‘ ∩ 𝑧 ) ⊆ ( 𝐹 ‘ 𝑥 ) ) )
56 53 55 imbi12d ⊢ ( 𝑦 = ∩ 𝑧 → ( ( ( 𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥 ) → ( 𝐹 ‘ 𝑦 ) ⊆ ( 𝐹 ‘ 𝑥 ) ) ↔ ( ( 𝑥 ⊆ 𝐵 ∧ ∩ 𝑧 ⊆ 𝑥 ) → ( 𝐹 ‘ ∩ 𝑧 ) ⊆ ( 𝐹 ‘ 𝑥 ) ) ) )
57 56 spcgv ⊢ ( ∩ 𝑧 ∈ 𝒫 𝐵 → ( ∀ 𝑦 ( ( 𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥 ) → ( 𝐹 ‘ 𝑦 ) ⊆ ( 𝐹 ‘ 𝑥 ) ) → ( ( 𝑥 ⊆ 𝐵 ∧ ∩ 𝑧 ⊆ 𝑥 ) → ( 𝐹 ‘ ∩ 𝑧 ) ⊆ ( 𝐹 ‘ 𝑥 ) ) ) )
58 42 46 51 57 syl3c ⊢ ( ( ( 𝜑 ∧ 𝑧 ⊆ dom ( 𝐹 ∩ I ) ∧ 𝑧 ≠ ∅ ) ∧ 𝑥 ∈ 𝑧 ) → ( 𝐹 ‘ ∩ 𝑧 ) ⊆ ( 𝐹 ‘ 𝑥 ) )
59 29 sselda ⊢ ( ( ( 𝜑 ∧ 𝑧 ⊆ dom ( 𝐹 ∩ I ) ∧ 𝑧 ≠ ∅ ) ∧ 𝑥 ∈ 𝑧 ) → 𝑥 ∈ dom ( 𝐹 ∩ I ) )
60 25 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑧 ⊆ dom ( 𝐹 ∩ I ) ∧ 𝑧 ≠ ∅ ) → 𝐹 Fn 𝒫 𝐵 )
61 60 adantr ⊢ ( ( ( 𝜑 ∧ 𝑧 ⊆ dom ( 𝐹 ∩ I ) ∧ 𝑧 ≠ ∅ ) ∧ 𝑥 ∈ 𝑧 ) → 𝐹 Fn 𝒫 𝐵 )
62 fnelfp ⊢ ( ( 𝐹 Fn 𝒫 𝐵 ∧ 𝑥 ∈ 𝒫 𝐵 ) → ( 𝑥 ∈ dom ( 𝐹 ∩ I ) ↔ ( 𝐹 ‘ 𝑥 ) = 𝑥 ) )
63 61 47 62 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑧 ⊆ dom ( 𝐹 ∩ I ) ∧ 𝑧 ≠ ∅ ) ∧ 𝑥 ∈ 𝑧 ) → ( 𝑥 ∈ dom ( 𝐹 ∩ I ) ↔ ( 𝐹 ‘ 𝑥 ) = 𝑥 ) )
64 59 63 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑧 ⊆ dom ( 𝐹 ∩ I ) ∧ 𝑧 ≠ ∅ ) ∧ 𝑥 ∈ 𝑧 ) → ( 𝐹 ‘ 𝑥 ) = 𝑥 )
65 58 64 sseqtrd ⊢ ( ( ( 𝜑 ∧ 𝑧 ⊆ dom ( 𝐹 ∩ I ) ∧ 𝑧 ≠ ∅ ) ∧ 𝑥 ∈ 𝑧 ) → ( 𝐹 ‘ ∩ 𝑧 ) ⊆ 𝑥 )
66 65 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑧 ⊆ dom ( 𝐹 ∩ I ) ∧ 𝑧 ≠ ∅ ) → ∀ 𝑥 ∈ 𝑧 ( 𝐹 ‘ ∩ 𝑧 ) ⊆ 𝑥 )
67 ssint ⊢ ( ( 𝐹 ‘ ∩ 𝑧 ) ⊆ ∩ 𝑧 ↔ ∀ 𝑥 ∈ 𝑧 ( 𝐹 ‘ ∩ 𝑧 ) ⊆ 𝑥 )
68 66 67 sylibr ⊢ ( ( 𝜑 ∧ 𝑧 ⊆ dom ( 𝐹 ∩ I ) ∧ 𝑧 ≠ ∅ ) → ( 𝐹 ‘ ∩ 𝑧 ) ⊆ ∩ 𝑧 )
69 18 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑧 ⊆ dom ( 𝐹 ∩ I ) ∧ 𝑧 ≠ ∅ ) → ∀ 𝑥 ∈ 𝒫 𝐵 𝑥 ⊆ ( 𝐹 ‘ 𝑥 ) )
70 id ⊢ ( 𝑥 = ∩ 𝑧 → 𝑥 = ∩ 𝑧 )
71 fveq2 ⊢ ( 𝑥 = ∩ 𝑧 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ ∩ 𝑧 ) )
72 70 71 sseq12d ⊢ ( 𝑥 = ∩ 𝑧 → ( 𝑥 ⊆ ( 𝐹 ‘ 𝑥 ) ↔ ∩ 𝑧 ⊆ ( 𝐹 ‘ ∩ 𝑧 ) ) )
73 72 rspcva ⊢ ( ( ∩ 𝑧 ∈ 𝒫 𝐵 ∧ ∀ 𝑥 ∈ 𝒫 𝐵 𝑥 ⊆ ( 𝐹 ‘ 𝑥 ) ) → ∩ 𝑧 ⊆ ( 𝐹 ‘ ∩ 𝑧 ) )
74 41 69 73 syl2anc ⊢ ( ( 𝜑 ∧ 𝑧 ⊆ dom ( 𝐹 ∩ I ) ∧ 𝑧 ≠ ∅ ) → ∩ 𝑧 ⊆ ( 𝐹 ‘ ∩ 𝑧 ) )
75 68 74 eqssd ⊢ ( ( 𝜑 ∧ 𝑧 ⊆ dom ( 𝐹 ∩ I ) ∧ 𝑧 ≠ ∅ ) → ( 𝐹 ‘ ∩ 𝑧 ) = ∩ 𝑧 )
76 fnelfp ⊢ ( ( 𝐹 Fn 𝒫 𝐵 ∧ ∩ 𝑧 ∈ 𝒫 𝐵 ) → ( ∩ 𝑧 ∈ dom ( 𝐹 ∩ I ) ↔ ( 𝐹 ‘ ∩ 𝑧 ) = ∩ 𝑧 ) )
77 60 41 76 syl2anc ⊢ ( ( 𝜑 ∧ 𝑧 ⊆ dom ( 𝐹 ∩ I ) ∧ 𝑧 ≠ ∅ ) → ( ∩ 𝑧 ∈ dom ( 𝐹 ∩ I ) ↔ ( 𝐹 ‘ ∩ 𝑧 ) = ∩ 𝑧 ) )
78 75 77 mpbird ⊢ ( ( 𝜑 ∧ 𝑧 ⊆ dom ( 𝐹 ∩ I ) ∧ 𝑧 ≠ ∅ ) → ∩ 𝑧 ∈ dom ( 𝐹 ∩ I ) )
79 9 28 78 ismred ⊢ ( 𝜑 → dom ( 𝐹 ∩ I ) ∈ ( Moore ‘ 𝐵 ) )