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 39432
Description: Any function from the subsets of a set to itself, which is extensive (satisfies mrcssid 16867), isotone (satisfies mrcss 16866), and idempotent (satisfies mrcidm 16869) 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 39433 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 4183 . . . 4 (𝐹 ∩ I ) ⊆ 𝐹
2 dmss 5747 . . . 4 ((𝐹 ∩ I ) ⊆ 𝐹 → dom (𝐹 ∩ I ) ⊆ dom 𝐹)
31, 2ax-mp 5 . . 3 dom (𝐹 ∩ I ) ⊆ dom 𝐹
4 ismrcd.f . . 3 (𝜑𝐹:𝒫 𝐵⟶𝒫 𝐵)
53, 4fssdm 6506 . 2 (𝜑 → dom (𝐹 ∩ I ) ⊆ 𝒫 𝐵)
6 ssid 3968 . . . . . . 7 𝐵𝐵
7 ismrcd.b . . . . . . . 8 (𝜑𝐵𝑉)
8 elpwg 4518 . . . . . . . 8 (𝐵𝑉 → (𝐵 ∈ 𝒫 𝐵𝐵𝐵))
97, 8syl 17 . . . . . . 7 (𝜑 → (𝐵 ∈ 𝒫 𝐵𝐵𝐵))
106, 9mpbiri 260 . . . . . 6 (𝜑𝐵 ∈ 𝒫 𝐵)
114, 10ffvelrnd 6828 . . . . 5 (𝜑 → (𝐹𝐵) ∈ 𝒫 𝐵)
1211elpwid 4526 . . . 4 (𝜑 → (𝐹𝐵) ⊆ 𝐵)
13 velpw 4520 . . . . . . 7 (𝑥 ∈ 𝒫 𝐵𝑥𝐵)
14 ismrcd.e . . . . . . 7 ((𝜑𝑥𝐵) → 𝑥 ⊆ (𝐹𝑥))
1513, 14sylan2b 595 . . . . . 6 ((𝜑𝑥 ∈ 𝒫 𝐵) → 𝑥 ⊆ (𝐹𝑥))
1615ralrimiva 3169 . . . . 5 (𝜑 → ∀𝑥 ∈ 𝒫 𝐵𝑥 ⊆ (𝐹𝑥))
17 id 22 . . . . . . 7 (𝑥 = 𝐵𝑥 = 𝐵)
18 fveq2 6646 . . . . . . 7 (𝑥 = 𝐵 → (𝐹𝑥) = (𝐹𝐵))
1917, 18sseq12d 3979 . . . . . 6 (𝑥 = 𝐵 → (𝑥 ⊆ (𝐹𝑥) ↔ 𝐵 ⊆ (𝐹𝐵)))
2019rspcva 3600 . . . . 5 ((𝐵 ∈ 𝒫 𝐵 ∧ ∀𝑥 ∈ 𝒫 𝐵𝑥 ⊆ (𝐹𝑥)) → 𝐵 ⊆ (𝐹𝐵))
2110, 16, 20syl2anc 586 . . . 4 (𝜑𝐵 ⊆ (𝐹𝐵))
2212, 21eqssd 3963 . . 3 (𝜑 → (𝐹𝐵) = 𝐵)
234ffnd 6491 . . . 4 (𝜑𝐹 Fn 𝒫 𝐵)
24 fnelfp 6913 . . . 4 ((𝐹 Fn 𝒫 𝐵𝐵 ∈ 𝒫 𝐵) → (𝐵 ∈ dom (𝐹 ∩ I ) ↔ (𝐹𝐵) = 𝐵))
2523, 10, 24syl2anc 586 . . 3 (𝜑 → (𝐵 ∈ dom (𝐹 ∩ I ) ↔ (𝐹𝐵) = 𝐵))
2622, 25mpbird 259 . 2 (𝜑𝐵 ∈ dom (𝐹 ∩ I ))
27 simp2 1133 . . . . . . . . . . . . 13 ((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → 𝑧 ⊆ dom (𝐹 ∩ I ))
2853ad2ant1 1129 . . . . . . . . . . . . 13 ((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → dom (𝐹 ∩ I ) ⊆ 𝒫 𝐵)
2927, 28sstrd 3956 . . . . . . . . . . . 12 ((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → 𝑧 ⊆ 𝒫 𝐵)
30 simp3 1134 . . . . . . . . . . . 12 ((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → 𝑧 ≠ ∅)
31 intssuni2 4877 . . . . . . . . . . . 12 ((𝑧 ⊆ 𝒫 𝐵𝑧 ≠ ∅) → 𝑧 𝒫 𝐵)
3229, 30, 31syl2anc 586 . . . . . . . . . . 11 ((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → 𝑧 𝒫 𝐵)
33 unipw 5319 . . . . . . . . . . 11 𝒫 𝐵 = 𝐵
3432, 33sseqtrdi 3996 . . . . . . . . . 10 ((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → 𝑧𝐵)
35 intex 5216 . . . . . . . . . . . 12 (𝑧 ≠ ∅ ↔ 𝑧 ∈ V)
36 elpwg 4518 . . . . . . . . . . . 12 ( 𝑧 ∈ V → ( 𝑧 ∈ 𝒫 𝐵 𝑧𝐵))
3735, 36sylbi 219 . . . . . . . . . . 11 (𝑧 ≠ ∅ → ( 𝑧 ∈ 𝒫 𝐵 𝑧𝐵))
38373ad2ant3 1131 . . . . . . . . . 10 ((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → ( 𝑧 ∈ 𝒫 𝐵 𝑧𝐵))
3934, 38mpbird 259 . . . . . . . . 9 ((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → 𝑧 ∈ 𝒫 𝐵)
4039adantr 483 . . . . . . . 8 (((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥𝑧) → 𝑧 ∈ 𝒫 𝐵)
41 ismrcd.m . . . . . . . . . . . 12 ((𝜑𝑥𝐵𝑦𝑥) → (𝐹𝑦) ⊆ (𝐹𝑥))
42413expib 1118 . . . . . . . . . . 11 (𝜑 → ((𝑥𝐵𝑦𝑥) → (𝐹𝑦) ⊆ (𝐹𝑥)))
4342alrimiv 1928 . . . . . . . . . 10 (𝜑 → ∀𝑦((𝑥𝐵𝑦𝑥) → (𝐹𝑦) ⊆ (𝐹𝑥)))
44433ad2ant1 1129 . . . . . . . . 9 ((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → ∀𝑦((𝑥𝐵𝑦𝑥) → (𝐹𝑦) ⊆ (𝐹𝑥)))
4544adantr 483 . . . . . . . 8 (((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥𝑧) → ∀𝑦((𝑥𝐵𝑦𝑥) → (𝐹𝑦) ⊆ (𝐹𝑥)))
4629sselda 3946 . . . . . . . . . 10 (((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥𝑧) → 𝑥 ∈ 𝒫 𝐵)
4746elpwid 4526 . . . . . . . . 9 (((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥𝑧) → 𝑥𝐵)
48 intss1 4867 . . . . . . . . . 10 (𝑥𝑧 𝑧𝑥)
4948adantl 484 . . . . . . . . 9 (((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥𝑧) → 𝑧𝑥)
5047, 49jca 514 . . . . . . . 8 (((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥𝑧) → (𝑥𝐵 𝑧𝑥))
51 sseq1 3971 . . . . . . . . . . 11 (𝑦 = 𝑧 → (𝑦𝑥 𝑧𝑥))
5251anbi2d 630 . . . . . . . . . 10 (𝑦 = 𝑧 → ((𝑥𝐵𝑦𝑥) ↔ (𝑥𝐵 𝑧𝑥)))
53 fveq2 6646 . . . . . . . . . . 11 (𝑦 = 𝑧 → (𝐹𝑦) = (𝐹 𝑧))
5453sseq1d 3977 . . . . . . . . . 10 (𝑦 = 𝑧 → ((𝐹𝑦) ⊆ (𝐹𝑥) ↔ (𝐹 𝑧) ⊆ (𝐹𝑥)))
5552, 54imbi12d 347 . . . . . . . . 9 (𝑦 = 𝑧 → (((𝑥𝐵𝑦𝑥) → (𝐹𝑦) ⊆ (𝐹𝑥)) ↔ ((𝑥𝐵 𝑧𝑥) → (𝐹 𝑧) ⊆ (𝐹𝑥))))
5655spcgv 3574 . . . . . . . 8 ( 𝑧 ∈ 𝒫 𝐵 → (∀𝑦((𝑥𝐵𝑦𝑥) → (𝐹𝑦) ⊆ (𝐹𝑥)) → ((𝑥𝐵 𝑧𝑥) → (𝐹 𝑧) ⊆ (𝐹𝑥))))
5740, 45, 50, 56syl3c 66 . . . . . . 7 (((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥𝑧) → (𝐹 𝑧) ⊆ (𝐹𝑥))
5827sselda 3946 . . . . . . . 8 (((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥𝑧) → 𝑥 ∈ dom (𝐹 ∩ I ))
59233ad2ant1 1129 . . . . . . . . . 10 ((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → 𝐹 Fn 𝒫 𝐵)
6059adantr 483 . . . . . . . . 9 (((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥𝑧) → 𝐹 Fn 𝒫 𝐵)
61 fnelfp 6913 . . . . . . . . 9 ((𝐹 Fn 𝒫 𝐵𝑥 ∈ 𝒫 𝐵) → (𝑥 ∈ dom (𝐹 ∩ I ) ↔ (𝐹𝑥) = 𝑥))
6260, 46, 61syl2anc 586 . . . . . . . 8 (((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥𝑧) → (𝑥 ∈ dom (𝐹 ∩ I ) ↔ (𝐹𝑥) = 𝑥))
6358, 62mpbid 234 . . . . . . 7 (((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥𝑧) → (𝐹𝑥) = 𝑥)
6457, 63sseqtrd 3986 . . . . . 6 (((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥𝑧) → (𝐹 𝑧) ⊆ 𝑥)
6564ralrimiva 3169 . . . . 5 ((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → ∀𝑥𝑧 (𝐹 𝑧) ⊆ 𝑥)
66 ssint 4868 . . . . 5 ((𝐹 𝑧) ⊆ 𝑧 ↔ ∀𝑥𝑧 (𝐹 𝑧) ⊆ 𝑥)
6765, 66sylibr 236 . . . 4 ((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → (𝐹 𝑧) ⊆ 𝑧)
68163ad2ant1 1129 . . . . 5 ((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → ∀𝑥 ∈ 𝒫 𝐵𝑥 ⊆ (𝐹𝑥))
69 id 22 . . . . . . 7 (𝑥 = 𝑧𝑥 = 𝑧)
70 fveq2 6646 . . . . . . 7 (𝑥 = 𝑧 → (𝐹𝑥) = (𝐹 𝑧))
7169, 70sseq12d 3979 . . . . . 6 (𝑥 = 𝑧 → (𝑥 ⊆ (𝐹𝑥) ↔ 𝑧 ⊆ (𝐹 𝑧)))
7271rspcva 3600 . . . . 5 (( 𝑧 ∈ 𝒫 𝐵 ∧ ∀𝑥 ∈ 𝒫 𝐵𝑥 ⊆ (𝐹𝑥)) → 𝑧 ⊆ (𝐹 𝑧))
7339, 68, 72syl2anc 586 . . . 4 ((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → 𝑧 ⊆ (𝐹 𝑧))
7467, 73eqssd 3963 . . 3 ((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → (𝐹 𝑧) = 𝑧)
75 fnelfp 6913 . . . 4 ((𝐹 Fn 𝒫 𝐵 𝑧 ∈ 𝒫 𝐵) → ( 𝑧 ∈ dom (𝐹 ∩ I ) ↔ (𝐹 𝑧) = 𝑧))
7659, 39, 75syl2anc 586 . . 3 ((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → ( 𝑧 ∈ dom (𝐹 ∩ I ) ↔ (𝐹 𝑧) = 𝑧))
7774, 76mpbird 259 . 2 ((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → 𝑧 ∈ dom (𝐹 ∩ I ))
785, 26, 77ismred 16852 1 (𝜑 → dom (𝐹 ∩ I ) ∈ (Moore‘𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 208  wa 398  w3a 1083  wal 1535   = wceq 1537  wcel 2114  wne 3006  wral 3125  Vcvv 3473  cin 3912  wss 3913  c0 4269  𝒫 cpw 4515   cuni 4814   cint 4852   I cid 5435  dom cdm 5531   Fn wfn 6326  wf 6327  cfv 6331  Moorecmre 16832
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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2792  ax-sep 5179  ax-nul 5186  ax-pow 5242  ax-pr 5306
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2799  df-cleq 2813  df-clel 2891  df-nfc 2959  df-ne 3007  df-ral 3130  df-rex 3131  df-rab 3134  df-v 3475  df-sbc 3753  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4270  df-if 4444  df-pw 4517  df-sn 4544  df-pr 4546  df-op 4550  df-uni 4815  df-int 4853  df-br 5043  df-opab 5105  df-mpt 5123  df-id 5436  df-xp 5537  df-rel 5538  df-cnv 5539  df-co 5540  df-dm 5541  df-rn 5542  df-res 5543  df-iota 6290  df-fun 6333  df-fn 6334  df-f 6335  df-fv 6339  df-mre 16836
This theorem is referenced by:  ismrcd2  39433  istopclsd  39434  ismrc  39435
  Copyright terms: Public domain W3C validator