Proof of Theorem mreclatBAD
| Step | Hyp | Ref
| Expression |
| 1 | | mreclat.i |
. . . 4
⊢ 𝐼 = (toInc‘𝐶) |
| 2 | 1 | ipopos 18581 |
. . 3
⊢ 𝐼 ∈ Poset |
| 3 | 2 | a1i 11 |
. 2
⊢ (𝐶 ∈ (Moore‘𝑋) → 𝐼 ∈ Poset) |
| 4 | | eqid 2737 |
. . . . . . . 8
⊢
(mrCls‘𝐶) =
(mrCls‘𝐶) |
| 5 | | eqid 2737 |
. . . . . . . 8
⊢
(lub‘𝐼) =
(lub‘𝐼) |
| 6 | 1, 4, 5 | mrelatlub 18607 |
. . . . . . 7
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑥 ⊆ 𝐶) → ((lub‘𝐼)‘𝑥) = ((mrCls‘𝐶)‘∪ 𝑥)) |
| 7 | | uniss 4915 |
. . . . . . . . . 10
⊢ (𝑥 ⊆ 𝐶 → ∪ 𝑥 ⊆ ∪ 𝐶) |
| 8 | 7 | adantl 481 |
. . . . . . . . 9
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑥 ⊆ 𝐶) → ∪ 𝑥 ⊆ ∪ 𝐶) |
| 9 | | mreuni 17643 |
. . . . . . . . . 10
⊢ (𝐶 ∈ (Moore‘𝑋) → ∪ 𝐶 =
𝑋) |
| 10 | 9 | adantr 480 |
. . . . . . . . 9
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑥 ⊆ 𝐶) → ∪ 𝐶 = 𝑋) |
| 11 | 8, 10 | sseqtrd 4020 |
. . . . . . . 8
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑥 ⊆ 𝐶) → ∪ 𝑥 ⊆ 𝑋) |
| 12 | 4 | mrccl 17654 |
. . . . . . . 8
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ ∪ 𝑥
⊆ 𝑋) →
((mrCls‘𝐶)‘∪ 𝑥) ∈ 𝐶) |
| 13 | 11, 12 | syldan 591 |
. . . . . . 7
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑥 ⊆ 𝐶) → ((mrCls‘𝐶)‘∪ 𝑥) ∈ 𝐶) |
| 14 | 6, 13 | eqeltrd 2841 |
. . . . . 6
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑥 ⊆ 𝐶) → ((lub‘𝐼)‘𝑥) ∈ 𝐶) |
| 15 | | fveq2 6906 |
. . . . . . . . . 10
⊢ (𝑥 = ∅ →
((glb‘𝐼)‘𝑥) = ((glb‘𝐼)‘∅)) |
| 16 | 15 | adantl 481 |
. . . . . . . . 9
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ 𝑥 ⊆ 𝐶) ∧ 𝑥 = ∅) → ((glb‘𝐼)‘𝑥) = ((glb‘𝐼)‘∅)) |
| 17 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(glb‘𝐼) =
(glb‘𝐼) |
| 18 | 1, 17 | mrelatglb0 18606 |
. . . . . . . . . 10
⊢ (𝐶 ∈ (Moore‘𝑋) → ((glb‘𝐼)‘∅) = 𝑋) |
| 19 | 18 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ 𝑥 ⊆ 𝐶) ∧ 𝑥 = ∅) → ((glb‘𝐼)‘∅) = 𝑋) |
| 20 | 16, 19 | eqtrd 2777 |
. . . . . . . 8
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ 𝑥 ⊆ 𝐶) ∧ 𝑥 = ∅) → ((glb‘𝐼)‘𝑥) = 𝑋) |
| 21 | | mre1cl 17637 |
. . . . . . . . 9
⊢ (𝐶 ∈ (Moore‘𝑋) → 𝑋 ∈ 𝐶) |
| 22 | 21 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ 𝑥 ⊆ 𝐶) ∧ 𝑥 = ∅) → 𝑋 ∈ 𝐶) |
| 23 | 20, 22 | eqeltrd 2841 |
. . . . . . 7
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ 𝑥 ⊆ 𝐶) ∧ 𝑥 = ∅) → ((glb‘𝐼)‘𝑥) ∈ 𝐶) |
| 24 | 1, 17 | mrelatglb 18605 |
. . . . . . . . 9
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑥 ⊆ 𝐶 ∧ 𝑥 ≠ ∅) → ((glb‘𝐼)‘𝑥) = ∩ 𝑥) |
| 25 | | mreintcl 17638 |
. . . . . . . . 9
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑥 ⊆ 𝐶 ∧ 𝑥 ≠ ∅) → ∩ 𝑥
∈ 𝐶) |
| 26 | 24, 25 | eqeltrd 2841 |
. . . . . . . 8
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑥 ⊆ 𝐶 ∧ 𝑥 ≠ ∅) → ((glb‘𝐼)‘𝑥) ∈ 𝐶) |
| 27 | 26 | 3expa 1119 |
. . . . . . 7
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ 𝑥 ⊆ 𝐶) ∧ 𝑥 ≠ ∅) → ((glb‘𝐼)‘𝑥) ∈ 𝐶) |
| 28 | 23, 27 | pm2.61dane 3029 |
. . . . . 6
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑥 ⊆ 𝐶) → ((glb‘𝐼)‘𝑥) ∈ 𝐶) |
| 29 | 14, 28 | jca 511 |
. . . . 5
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑥 ⊆ 𝐶) → (((lub‘𝐼)‘𝑥) ∈ 𝐶 ∧ ((glb‘𝐼)‘𝑥) ∈ 𝐶)) |
| 30 | 29 | ex 412 |
. . . 4
⊢ (𝐶 ∈ (Moore‘𝑋) → (𝑥 ⊆ 𝐶 → (((lub‘𝐼)‘𝑥) ∈ 𝐶 ∧ ((glb‘𝐼)‘𝑥) ∈ 𝐶))) |
| 31 | 1 | ipobas 18576 |
. . . . 5
⊢ (𝐶 ∈ (Moore‘𝑋) → 𝐶 = (Base‘𝐼)) |
| 32 | | sseq2 4010 |
. . . . . 6
⊢ (𝐶 = (Base‘𝐼) → (𝑥 ⊆ 𝐶 ↔ 𝑥 ⊆ (Base‘𝐼))) |
| 33 | | eleq2 2830 |
. . . . . . 7
⊢ (𝐶 = (Base‘𝐼) → (((lub‘𝐼)‘𝑥) ∈ 𝐶 ↔ ((lub‘𝐼)‘𝑥) ∈ (Base‘𝐼))) |
| 34 | | eleq2 2830 |
. . . . . . 7
⊢ (𝐶 = (Base‘𝐼) → (((glb‘𝐼)‘𝑥) ∈ 𝐶 ↔ ((glb‘𝐼)‘𝑥) ∈ (Base‘𝐼))) |
| 35 | 33, 34 | anbi12d 632 |
. . . . . 6
⊢ (𝐶 = (Base‘𝐼) → ((((lub‘𝐼)‘𝑥) ∈ 𝐶 ∧ ((glb‘𝐼)‘𝑥) ∈ 𝐶) ↔ (((lub‘𝐼)‘𝑥) ∈ (Base‘𝐼) ∧ ((glb‘𝐼)‘𝑥) ∈ (Base‘𝐼)))) |
| 36 | 32, 35 | imbi12d 344 |
. . . . 5
⊢ (𝐶 = (Base‘𝐼) → ((𝑥 ⊆ 𝐶 → (((lub‘𝐼)‘𝑥) ∈ 𝐶 ∧ ((glb‘𝐼)‘𝑥) ∈ 𝐶)) ↔ (𝑥 ⊆ (Base‘𝐼) → (((lub‘𝐼)‘𝑥) ∈ (Base‘𝐼) ∧ ((glb‘𝐼)‘𝑥) ∈ (Base‘𝐼))))) |
| 37 | 31, 36 | syl 17 |
. . . 4
⊢ (𝐶 ∈ (Moore‘𝑋) → ((𝑥 ⊆ 𝐶 → (((lub‘𝐼)‘𝑥) ∈ 𝐶 ∧ ((glb‘𝐼)‘𝑥) ∈ 𝐶)) ↔ (𝑥 ⊆ (Base‘𝐼) → (((lub‘𝐼)‘𝑥) ∈ (Base‘𝐼) ∧ ((glb‘𝐼)‘𝑥) ∈ (Base‘𝐼))))) |
| 38 | 30, 37 | mpbid 232 |
. . 3
⊢ (𝐶 ∈ (Moore‘𝑋) → (𝑥 ⊆ (Base‘𝐼) → (((lub‘𝐼)‘𝑥) ∈ (Base‘𝐼) ∧ ((glb‘𝐼)‘𝑥) ∈ (Base‘𝐼)))) |
| 39 | 38 | alrimiv 1927 |
. 2
⊢ (𝐶 ∈ (Moore‘𝑋) → ∀𝑥(𝑥 ⊆ (Base‘𝐼) → (((lub‘𝐼)‘𝑥) ∈ (Base‘𝐼) ∧ ((glb‘𝐼)‘𝑥) ∈ (Base‘𝐼)))) |
| 40 | | isclatBAD. |
. 2
⊢ (𝐼 ∈ CLat ↔ (𝐼 ∈ Poset ∧
∀𝑥(𝑥 ⊆ (Base‘𝐼) → (((lub‘𝐼)‘𝑥) ∈ (Base‘𝐼) ∧ ((glb‘𝐼)‘𝑥) ∈ (Base‘𝐼))))) |
| 41 | 3, 39, 40 | sylanbrc 583 |
1
⊢ (𝐶 ∈ (Moore‘𝑋) → 𝐼 ∈ CLat) |