Users' Mathboxes Mathbox for Stefan O'Rear < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ismrcd1 Structured version   Visualization version   GIF version

Theorem ismrcd1 38231
Description: Any function from the subsets of a set to itself, which is extensive (satisfies mrcssid 16667), isotone (satisfies mrcss 16666), and idempotent (satisfies mrcidm 16669) 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 38232 is the second. (Contributed by Stefan O'Rear, 1-Feb-2015.)
Hypotheses
Ref Expression
ismrcd.b (𝜑𝐵𝑉)
ismrcd.f (𝜑𝐹:𝒫 𝐵⟶𝒫 𝐵)
ismrcd.e ((𝜑𝑥𝐵) → 𝑥 ⊆ (𝐹𝑥))
ismrcd.m ((𝜑𝑥𝐵𝑦𝑥) → (𝐹𝑦) ⊆ (𝐹𝑥))
ismrcd.i ((𝜑𝑥𝐵) → (𝐹‘(𝐹𝑥)) = (𝐹𝑥))
Assertion
Ref Expression
ismrcd1 (𝜑 → dom (𝐹 ∩ I ) ∈ (Moore‘𝐵))
Distinct variable groups:   𝜑,𝑥,𝑦   𝑥,𝐵,𝑦   𝑥,𝐹,𝑦   𝑥,𝑉,𝑦

Proof of Theorem ismrcd1
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 inss1 4053 . . . 4 (𝐹 ∩ I ) ⊆ 𝐹
2 dmss 5570 . . . 4 ((𝐹 ∩ I ) ⊆ 𝐹 → dom (𝐹 ∩ I ) ⊆ dom 𝐹)
31, 2ax-mp 5 . . 3 dom (𝐹 ∩ I ) ⊆ dom 𝐹
4 ismrcd.f . . 3 (𝜑𝐹:𝒫 𝐵⟶𝒫 𝐵)
53, 4fssdm 6309 . 2 (𝜑 → dom (𝐹 ∩ I ) ⊆ 𝒫 𝐵)
6 ssid 3842 . . . . . . 7 𝐵𝐵
7 ismrcd.b . . . . . . . 8 (𝜑𝐵𝑉)
8 elpwg 4387 . . . . . . . 8 (𝐵𝑉 → (𝐵 ∈ 𝒫 𝐵𝐵𝐵))
97, 8syl 17 . . . . . . 7 (𝜑 → (𝐵 ∈ 𝒫 𝐵𝐵𝐵))
106, 9mpbiri 250 . . . . . 6 (𝜑𝐵 ∈ 𝒫 𝐵)
114, 10ffvelrnd 6626 . . . . 5 (𝜑 → (𝐹𝐵) ∈ 𝒫 𝐵)
1211elpwid 4391 . . . 4 (𝜑 → (𝐹𝐵) ⊆ 𝐵)
13 selpw 4386 . . . . . . 7 (𝑥 ∈ 𝒫 𝐵𝑥𝐵)
14 ismrcd.e . . . . . . 7 ((𝜑𝑥𝐵) → 𝑥 ⊆ (𝐹𝑥))
1513, 14sylan2b 587 . . . . . 6 ((𝜑𝑥 ∈ 𝒫 𝐵) → 𝑥 ⊆ (𝐹𝑥))
1615ralrimiva 3148 . . . . 5 (𝜑 → ∀𝑥 ∈ 𝒫 𝐵𝑥 ⊆ (𝐹𝑥))
17 id 22 . . . . . . 7 (𝑥 = 𝐵𝑥 = 𝐵)
18 fveq2 6448 . . . . . . 7 (𝑥 = 𝐵 → (𝐹𝑥) = (𝐹𝐵))
1917, 18sseq12d 3853 . . . . . 6 (𝑥 = 𝐵 → (𝑥 ⊆ (𝐹𝑥) ↔ 𝐵 ⊆ (𝐹𝐵)))
2019rspcva 3509 . . . . 5 ((𝐵 ∈ 𝒫 𝐵 ∧ ∀𝑥 ∈ 𝒫 𝐵𝑥 ⊆ (𝐹𝑥)) → 𝐵 ⊆ (𝐹𝐵))
2110, 16, 20syl2anc 579 . . . 4 (𝜑𝐵 ⊆ (𝐹𝐵))
2212, 21eqssd 3838 . . 3 (𝜑 → (𝐹𝐵) = 𝐵)
234ffnd 6294 . . . 4 (𝜑𝐹 Fn 𝒫 𝐵)
24 fnelfp 6710 . . . 4 ((𝐹 Fn 𝒫 𝐵𝐵 ∈ 𝒫 𝐵) → (𝐵 ∈ dom (𝐹 ∩ I ) ↔ (𝐹𝐵) = 𝐵))
2523, 10, 24syl2anc 579 . . 3 (𝜑 → (𝐵 ∈ dom (𝐹 ∩ I ) ↔ (𝐹𝐵) = 𝐵))
2622, 25mpbird 249 . 2 (𝜑𝐵 ∈ dom (𝐹 ∩ I ))
27 simp2 1128 . . . . . . . . . . . . 13 ((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → 𝑧 ⊆ dom (𝐹 ∩ I ))
2853ad2ant1 1124 . . . . . . . . . . . . 13 ((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → dom (𝐹 ∩ I ) ⊆ 𝒫 𝐵)
2927, 28sstrd 3831 . . . . . . . . . . . 12 ((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → 𝑧 ⊆ 𝒫 𝐵)
30 simp3 1129 . . . . . . . . . . . 12 ((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → 𝑧 ≠ ∅)
31 intssuni2 4737 . . . . . . . . . . . 12 ((𝑧 ⊆ 𝒫 𝐵𝑧 ≠ ∅) → 𝑧 𝒫 𝐵)
3229, 30, 31syl2anc 579 . . . . . . . . . . 11 ((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → 𝑧 𝒫 𝐵)
33 unipw 5152 . . . . . . . . . . 11 𝒫 𝐵 = 𝐵
3432, 33syl6sseq 3870 . . . . . . . . . 10 ((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → 𝑧𝐵)
35 intex 5056 . . . . . . . . . . . 12 (𝑧 ≠ ∅ ↔ 𝑧 ∈ V)
36 elpwg 4387 . . . . . . . . . . . 12 ( 𝑧 ∈ V → ( 𝑧 ∈ 𝒫 𝐵 𝑧𝐵))
3735, 36sylbi 209 . . . . . . . . . . 11 (𝑧 ≠ ∅ → ( 𝑧 ∈ 𝒫 𝐵 𝑧𝐵))
38373ad2ant3 1126 . . . . . . . . . 10 ((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → ( 𝑧 ∈ 𝒫 𝐵 𝑧𝐵))
3934, 38mpbird 249 . . . . . . . . 9 ((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → 𝑧 ∈ 𝒫 𝐵)
4039adantr 474 . . . . . . . 8 (((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥𝑧) → 𝑧 ∈ 𝒫 𝐵)
41 ismrcd.m . . . . . . . . . . . 12 ((𝜑𝑥𝐵𝑦𝑥) → (𝐹𝑦) ⊆ (𝐹𝑥))
42413expib 1113 . . . . . . . . . . 11 (𝜑 → ((𝑥𝐵𝑦𝑥) → (𝐹𝑦) ⊆ (𝐹𝑥)))
4342alrimiv 1970 . . . . . . . . . 10 (𝜑 → ∀𝑦((𝑥𝐵𝑦𝑥) → (𝐹𝑦) ⊆ (𝐹𝑥)))
44433ad2ant1 1124 . . . . . . . . 9 ((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → ∀𝑦((𝑥𝐵𝑦𝑥) → (𝐹𝑦) ⊆ (𝐹𝑥)))
4544adantr 474 . . . . . . . 8 (((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥𝑧) → ∀𝑦((𝑥𝐵𝑦𝑥) → (𝐹𝑦) ⊆ (𝐹𝑥)))
4629sselda 3821 . . . . . . . . . 10 (((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥𝑧) → 𝑥 ∈ 𝒫 𝐵)
4746elpwid 4391 . . . . . . . . 9 (((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥𝑧) → 𝑥𝐵)
48 intss1 4727 . . . . . . . . . 10 (𝑥𝑧 𝑧𝑥)
4948adantl 475 . . . . . . . . 9 (((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥𝑧) → 𝑧𝑥)
5047, 49jca 507 . . . . . . . 8 (((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥𝑧) → (𝑥𝐵 𝑧𝑥))
51 sseq1 3845 . . . . . . . . . . 11 (𝑦 = 𝑧 → (𝑦𝑥 𝑧𝑥))
5251anbi2d 622 . . . . . . . . . 10 (𝑦 = 𝑧 → ((𝑥𝐵𝑦𝑥) ↔ (𝑥𝐵 𝑧𝑥)))
53 fveq2 6448 . . . . . . . . . . 11 (𝑦 = 𝑧 → (𝐹𝑦) = (𝐹 𝑧))
5453sseq1d 3851 . . . . . . . . . 10 (𝑦 = 𝑧 → ((𝐹𝑦) ⊆ (𝐹𝑥) ↔ (𝐹 𝑧) ⊆ (𝐹𝑥)))
5552, 54imbi12d 336 . . . . . . . . 9 (𝑦 = 𝑧 → (((𝑥𝐵𝑦𝑥) → (𝐹𝑦) ⊆ (𝐹𝑥)) ↔ ((𝑥𝐵 𝑧𝑥) → (𝐹 𝑧) ⊆ (𝐹𝑥))))
5655spcgv 3495 . . . . . . . 8 ( 𝑧 ∈ 𝒫 𝐵 → (∀𝑦((𝑥𝐵𝑦𝑥) → (𝐹𝑦) ⊆ (𝐹𝑥)) → ((𝑥𝐵 𝑧𝑥) → (𝐹 𝑧) ⊆ (𝐹𝑥))))
5740, 45, 50, 56syl3c 66 . . . . . . 7 (((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥𝑧) → (𝐹 𝑧) ⊆ (𝐹𝑥))
5827sselda 3821 . . . . . . . 8 (((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥𝑧) → 𝑥 ∈ dom (𝐹 ∩ I ))
59233ad2ant1 1124 . . . . . . . . . 10 ((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → 𝐹 Fn 𝒫 𝐵)
6059adantr 474 . . . . . . . . 9 (((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥𝑧) → 𝐹 Fn 𝒫 𝐵)
61 fnelfp 6710 . . . . . . . . 9 ((𝐹 Fn 𝒫 𝐵𝑥 ∈ 𝒫 𝐵) → (𝑥 ∈ dom (𝐹 ∩ I ) ↔ (𝐹𝑥) = 𝑥))
6260, 46, 61syl2anc 579 . . . . . . . 8 (((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥𝑧) → (𝑥 ∈ dom (𝐹 ∩ I ) ↔ (𝐹𝑥) = 𝑥))
6358, 62mpbid 224 . . . . . . 7 (((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥𝑧) → (𝐹𝑥) = 𝑥)
6457, 63sseqtrd 3860 . . . . . 6 (((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥𝑧) → (𝐹 𝑧) ⊆ 𝑥)
6564ralrimiva 3148 . . . . 5 ((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → ∀𝑥𝑧 (𝐹 𝑧) ⊆ 𝑥)
66 ssint 4728 . . . . 5 ((𝐹 𝑧) ⊆ 𝑧 ↔ ∀𝑥𝑧 (𝐹 𝑧) ⊆ 𝑥)
6765, 66sylibr 226 . . . 4 ((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → (𝐹 𝑧) ⊆ 𝑧)
68163ad2ant1 1124 . . . . 5 ((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → ∀𝑥 ∈ 𝒫 𝐵𝑥 ⊆ (𝐹𝑥))
69 id 22 . . . . . . 7 (𝑥 = 𝑧𝑥 = 𝑧)
70 fveq2 6448 . . . . . . 7 (𝑥 = 𝑧 → (𝐹𝑥) = (𝐹 𝑧))
7169, 70sseq12d 3853 . . . . . 6 (𝑥 = 𝑧 → (𝑥 ⊆ (𝐹𝑥) ↔ 𝑧 ⊆ (𝐹 𝑧)))
7271rspcva 3509 . . . . 5 (( 𝑧 ∈ 𝒫 𝐵 ∧ ∀𝑥 ∈ 𝒫 𝐵𝑥 ⊆ (𝐹𝑥)) → 𝑧 ⊆ (𝐹 𝑧))
7339, 68, 72syl2anc 579 . . . 4 ((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → 𝑧 ⊆ (𝐹 𝑧))
7467, 73eqssd 3838 . . 3 ((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → (𝐹 𝑧) = 𝑧)
75 fnelfp 6710 . . . 4 ((𝐹 Fn 𝒫 𝐵 𝑧 ∈ 𝒫 𝐵) → ( 𝑧 ∈ dom (𝐹 ∩ I ) ↔ (𝐹 𝑧) = 𝑧))
7659, 39, 75syl2anc 579 . . 3 ((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → ( 𝑧 ∈ dom (𝐹 ∩ I ) ↔ (𝐹 𝑧) = 𝑧))
7774, 76mpbird 249 . 2 ((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → 𝑧 ∈ dom (𝐹 ∩ I ))
785, 26, 77ismred 16652 1 (𝜑 → dom (𝐹 ∩ I ) ∈ (Moore‘𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 386  w3a 1071  wal 1599   = wceq 1601  wcel 2107  wne 2969  wral 3090  Vcvv 3398  cin 3791  wss 3792  c0 4141  𝒫 cpw 4379   cuni 4673   cint 4712   I cid 5262  dom cdm 5357   Fn wfn 6132  wf 6133  cfv 6137  Moorecmre 16632
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-sep 5019  ax-nul 5027  ax-pow 5079  ax-pr 5140
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-ral 3095  df-rex 3096  df-rab 3099  df-v 3400  df-sbc 3653  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-nul 4142  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-op 4405  df-uni 4674  df-int 4713  df-br 4889  df-opab 4951  df-mpt 4968  df-id 5263  df-xp 5363  df-rel 5364  df-cnv 5365  df-co 5366  df-dm 5367  df-rn 5368  df-res 5369  df-iota 6101  df-fun 6139  df-fn 6140  df-f 6141  df-fv 6145  df-mre 16636
This theorem is referenced by:  ismrcd2  38232  istopclsd  38233  ismrc  38234
  Copyright terms: Public domain W3C validator