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 36169
Description: Any function from the subsets of a set to itself, which is extensive (satisfies mrcssid 15990), isotone (satisfies mrcss 15989), and idempotent (satisfies mrcidm 15992) 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 36170 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 3698 . . . 4 (𝐹 ∩ I ) ⊆ 𝐹
2 dmss 5136 . . . 4 ((𝐹 ∩ I ) ⊆ 𝐹 → dom (𝐹 ∩ I ) ⊆ dom 𝐹)
31, 2ax-mp 5 . . 3 dom (𝐹 ∩ I ) ⊆ dom 𝐹
4 ismrcd.f . . . 4 (𝜑𝐹:𝒫 𝐵⟶𝒫 𝐵)
5 fdm 5849 . . . 4 (𝐹:𝒫 𝐵⟶𝒫 𝐵 → dom 𝐹 = 𝒫 𝐵)
64, 5syl 17 . . 3 (𝜑 → dom 𝐹 = 𝒫 𝐵)
73, 6syl5sseq 3520 . 2 (𝜑 → dom (𝐹 ∩ I ) ⊆ 𝒫 𝐵)
8 ssid 3491 . . . . . . 7 𝐵𝐵
9 ismrcd.b . . . . . . . 8 (𝜑𝐵𝑉)
10 elpwg 4019 . . . . . . . 8 (𝐵𝑉 → (𝐵 ∈ 𝒫 𝐵𝐵𝐵))
119, 10syl 17 . . . . . . 7 (𝜑 → (𝐵 ∈ 𝒫 𝐵𝐵𝐵))
128, 11mpbiri 246 . . . . . 6 (𝜑𝐵 ∈ 𝒫 𝐵)
134, 12ffvelrnd 6151 . . . . 5 (𝜑 → (𝐹𝐵) ∈ 𝒫 𝐵)
1413elpwid 4021 . . . 4 (𝜑 → (𝐹𝐵) ⊆ 𝐵)
15 selpw 4018 . . . . . . 7 (𝑥 ∈ 𝒫 𝐵𝑥𝐵)
16 ismrcd.e . . . . . . 7 ((𝜑𝑥𝐵) → 𝑥 ⊆ (𝐹𝑥))
1715, 16sylan2b 490 . . . . . 6 ((𝜑𝑥 ∈ 𝒫 𝐵) → 𝑥 ⊆ (𝐹𝑥))
1817ralrimiva 2853 . . . . 5 (𝜑 → ∀𝑥 ∈ 𝒫 𝐵𝑥 ⊆ (𝐹𝑥))
19 id 22 . . . . . . 7 (𝑥 = 𝐵𝑥 = 𝐵)
20 fveq2 5986 . . . . . . 7 (𝑥 = 𝐵 → (𝐹𝑥) = (𝐹𝐵))
2119, 20sseq12d 3501 . . . . . 6 (𝑥 = 𝐵 → (𝑥 ⊆ (𝐹𝑥) ↔ 𝐵 ⊆ (𝐹𝐵)))
2221rspcva 3184 . . . . 5 ((𝐵 ∈ 𝒫 𝐵 ∧ ∀𝑥 ∈ 𝒫 𝐵𝑥 ⊆ (𝐹𝑥)) → 𝐵 ⊆ (𝐹𝐵))
2312, 18, 22syl2anc 690 . . . 4 (𝜑𝐵 ⊆ (𝐹𝐵))
2414, 23eqssd 3489 . . 3 (𝜑 → (𝐹𝐵) = 𝐵)
25 ffn 5843 . . . . 5 (𝐹:𝒫 𝐵⟶𝒫 𝐵𝐹 Fn 𝒫 𝐵)
264, 25syl 17 . . . 4 (𝜑𝐹 Fn 𝒫 𝐵)
27 fnelfp 6222 . . . 4 ((𝐹 Fn 𝒫 𝐵𝐵 ∈ 𝒫 𝐵) → (𝐵 ∈ dom (𝐹 ∩ I ) ↔ (𝐹𝐵) = 𝐵))
2826, 12, 27syl2anc 690 . . 3 (𝜑 → (𝐵 ∈ dom (𝐹 ∩ I ) ↔ (𝐹𝐵) = 𝐵))
2924, 28mpbird 245 . 2 (𝜑𝐵 ∈ dom (𝐹 ∩ I ))
30 simp2 1054 . . . . . . . . . . . . 13 ((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → 𝑧 ⊆ dom (𝐹 ∩ I ))
3173ad2ant1 1074 . . . . . . . . . . . . 13 ((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → dom (𝐹 ∩ I ) ⊆ 𝒫 𝐵)
3230, 31sstrd 3482 . . . . . . . . . . . 12 ((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → 𝑧 ⊆ 𝒫 𝐵)
33 simp3 1055 . . . . . . . . . . . 12 ((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → 𝑧 ≠ ∅)
34 intssuni2 4335 . . . . . . . . . . . 12 ((𝑧 ⊆ 𝒫 𝐵𝑧 ≠ ∅) → 𝑧 𝒫 𝐵)
3532, 33, 34syl2anc 690 . . . . . . . . . . 11 ((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → 𝑧 𝒫 𝐵)
36 unipw 4743 . . . . . . . . . . 11 𝒫 𝐵 = 𝐵
3735, 36syl6sseq 3518 . . . . . . . . . 10 ((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → 𝑧𝐵)
38 intex 4646 . . . . . . . . . . . 12 (𝑧 ≠ ∅ ↔ 𝑧 ∈ V)
39 elpwg 4019 . . . . . . . . . . . 12 ( 𝑧 ∈ V → ( 𝑧 ∈ 𝒫 𝐵 𝑧𝐵))
4038, 39sylbi 205 . . . . . . . . . . 11 (𝑧 ≠ ∅ → ( 𝑧 ∈ 𝒫 𝐵 𝑧𝐵))
41403ad2ant3 1076 . . . . . . . . . 10 ((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → ( 𝑧 ∈ 𝒫 𝐵 𝑧𝐵))
4237, 41mpbird 245 . . . . . . . . 9 ((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → 𝑧 ∈ 𝒫 𝐵)
4342adantr 479 . . . . . . . 8 (((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥𝑧) → 𝑧 ∈ 𝒫 𝐵)
44 ismrcd.m . . . . . . . . . . . 12 ((𝜑𝑥𝐵𝑦𝑥) → (𝐹𝑦) ⊆ (𝐹𝑥))
45443expib 1259 . . . . . . . . . . 11 (𝜑 → ((𝑥𝐵𝑦𝑥) → (𝐹𝑦) ⊆ (𝐹𝑥)))
4645alrimiv 1808 . . . . . . . . . 10 (𝜑 → ∀𝑦((𝑥𝐵𝑦𝑥) → (𝐹𝑦) ⊆ (𝐹𝑥)))
47463ad2ant1 1074 . . . . . . . . 9 ((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → ∀𝑦((𝑥𝐵𝑦𝑥) → (𝐹𝑦) ⊆ (𝐹𝑥)))
4847adantr 479 . . . . . . . 8 (((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥𝑧) → ∀𝑦((𝑥𝐵𝑦𝑥) → (𝐹𝑦) ⊆ (𝐹𝑥)))
4932sselda 3472 . . . . . . . . . 10 (((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥𝑧) → 𝑥 ∈ 𝒫 𝐵)
5049elpwid 4021 . . . . . . . . 9 (((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥𝑧) → 𝑥𝐵)
51 intss1 4325 . . . . . . . . . 10 (𝑥𝑧 𝑧𝑥)
5251adantl 480 . . . . . . . . 9 (((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥𝑧) → 𝑧𝑥)
5350, 52jca 552 . . . . . . . 8 (((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥𝑧) → (𝑥𝐵 𝑧𝑥))
54 sseq1 3493 . . . . . . . . . . 11 (𝑦 = 𝑧 → (𝑦𝑥 𝑧𝑥))
5554anbi2d 735 . . . . . . . . . 10 (𝑦 = 𝑧 → ((𝑥𝐵𝑦𝑥) ↔ (𝑥𝐵 𝑧𝑥)))
56 fveq2 5986 . . . . . . . . . . 11 (𝑦 = 𝑧 → (𝐹𝑦) = (𝐹 𝑧))
5756sseq1d 3499 . . . . . . . . . 10 (𝑦 = 𝑧 → ((𝐹𝑦) ⊆ (𝐹𝑥) ↔ (𝐹 𝑧) ⊆ (𝐹𝑥)))
5855, 57imbi12d 332 . . . . . . . . 9 (𝑦 = 𝑧 → (((𝑥𝐵𝑦𝑥) → (𝐹𝑦) ⊆ (𝐹𝑥)) ↔ ((𝑥𝐵 𝑧𝑥) → (𝐹 𝑧) ⊆ (𝐹𝑥))))
5958spcgv 3170 . . . . . . . 8 ( 𝑧 ∈ 𝒫 𝐵 → (∀𝑦((𝑥𝐵𝑦𝑥) → (𝐹𝑦) ⊆ (𝐹𝑥)) → ((𝑥𝐵 𝑧𝑥) → (𝐹 𝑧) ⊆ (𝐹𝑥))))
6043, 48, 53, 59syl3c 63 . . . . . . 7 (((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥𝑧) → (𝐹 𝑧) ⊆ (𝐹𝑥))
6130sselda 3472 . . . . . . . 8 (((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥𝑧) → 𝑥 ∈ dom (𝐹 ∩ I ))
62263ad2ant1 1074 . . . . . . . . . 10 ((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → 𝐹 Fn 𝒫 𝐵)
6362adantr 479 . . . . . . . . 9 (((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥𝑧) → 𝐹 Fn 𝒫 𝐵)
64 fnelfp 6222 . . . . . . . . 9 ((𝐹 Fn 𝒫 𝐵𝑥 ∈ 𝒫 𝐵) → (𝑥 ∈ dom (𝐹 ∩ I ) ↔ (𝐹𝑥) = 𝑥))
6563, 49, 64syl2anc 690 . . . . . . . 8 (((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥𝑧) → (𝑥 ∈ dom (𝐹 ∩ I ) ↔ (𝐹𝑥) = 𝑥))
6661, 65mpbid 220 . . . . . . 7 (((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥𝑧) → (𝐹𝑥) = 𝑥)
6760, 66sseqtrd 3508 . . . . . 6 (((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥𝑧) → (𝐹 𝑧) ⊆ 𝑥)
6867ralrimiva 2853 . . . . 5 ((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → ∀𝑥𝑧 (𝐹 𝑧) ⊆ 𝑥)
69 ssint 4326 . . . . 5 ((𝐹 𝑧) ⊆ 𝑧 ↔ ∀𝑥𝑧 (𝐹 𝑧) ⊆ 𝑥)
7068, 69sylibr 222 . . . 4 ((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → (𝐹 𝑧) ⊆ 𝑧)
71183ad2ant1 1074 . . . . 5 ((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → ∀𝑥 ∈ 𝒫 𝐵𝑥 ⊆ (𝐹𝑥))
72 id 22 . . . . . . 7 (𝑥 = 𝑧𝑥 = 𝑧)
73 fveq2 5986 . . . . . . 7 (𝑥 = 𝑧 → (𝐹𝑥) = (𝐹 𝑧))
7472, 73sseq12d 3501 . . . . . 6 (𝑥 = 𝑧 → (𝑥 ⊆ (𝐹𝑥) ↔ 𝑧 ⊆ (𝐹 𝑧)))
7574rspcva 3184 . . . . 5 (( 𝑧 ∈ 𝒫 𝐵 ∧ ∀𝑥 ∈ 𝒫 𝐵𝑥 ⊆ (𝐹𝑥)) → 𝑧 ⊆ (𝐹 𝑧))
7642, 71, 75syl2anc 690 . . . 4 ((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → 𝑧 ⊆ (𝐹 𝑧))
7770, 76eqssd 3489 . . 3 ((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → (𝐹 𝑧) = 𝑧)
78 fnelfp 6222 . . . 4 ((𝐹 Fn 𝒫 𝐵 𝑧 ∈ 𝒫 𝐵) → ( 𝑧 ∈ dom (𝐹 ∩ I ) ↔ (𝐹 𝑧) = 𝑧))
7962, 42, 78syl2anc 690 . . 3 ((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → ( 𝑧 ∈ dom (𝐹 ∩ I ) ↔ (𝐹 𝑧) = 𝑧))
8077, 79mpbird 245 . 2 ((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → 𝑧 ∈ dom (𝐹 ∩ I ))
817, 29, 80ismred 15975 1 (𝜑 → dom (𝐹 ∩ I ) ∈ (Moore‘𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382  w3a 1030  wal 1472   = wceq 1474  wcel 1938  wne 2684  wral 2800  Vcvv 3077  cin 3443  wss 3444  c0 3777  𝒫 cpw 4011   cuni 4270   cint 4308   I cid 4842  dom cdm 4932   Fn wfn 5684  wf 5685  cfv 5689  Moorecmre 15955
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885  ax-8 1940  ax-9 1947  ax-10 1966  ax-11 1971  ax-12 1983  ax-13 2137  ax-ext 2494  ax-sep 4607  ax-nul 4616  ax-pow 4668  ax-pr 4732
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1699  df-sb 1831  df-eu 2366  df-mo 2367  df-clab 2501  df-cleq 2507  df-clel 2510  df-nfc 2644  df-ne 2686  df-ral 2805  df-rex 2806  df-rab 2809  df-v 3079  df-sbc 3307  df-dif 3447  df-un 3449  df-in 3451  df-ss 3458  df-nul 3778  df-if 3940  df-pw 4013  df-sn 4029  df-pr 4031  df-op 4035  df-uni 4271  df-int 4309  df-br 4482  df-opab 4542  df-mpt 4543  df-id 4847  df-xp 4938  df-rel 4939  df-cnv 4940  df-co 4941  df-dm 4942  df-rn 4943  df-res 4944  df-iota 5653  df-fun 5691  df-fn 5692  df-f 5693  df-fv 5697  df-mre 15959
This theorem is referenced by:  ismrcd2  36170  istopclsd  36171  ismrc  36172
  Copyright terms: Public domain W3C validator