| Step | Hyp | Ref
| Expression |
| 1 | | inss1 4237 |
. . . 4
⊢ (𝐹 ∩ I ) ⊆ 𝐹 |
| 2 | | dmss 5913 |
. . . 4
⊢ ((𝐹 ∩ I ) ⊆ 𝐹 → dom (𝐹 ∩ I ) ⊆ dom 𝐹) |
| 3 | 1, 2 | ax-mp 5 |
. . 3
⊢ dom
(𝐹 ∩ I ) ⊆ dom
𝐹 |
| 4 | | ismrcd.f |
. . 3
⊢ (𝜑 → 𝐹:𝒫 𝐵⟶𝒫 𝐵) |
| 5 | 3, 4 | fssdm 6755 |
. 2
⊢ (𝜑 → dom (𝐹 ∩ I ) ⊆ 𝒫 𝐵) |
| 6 | | ssid 4006 |
. . . . . . 7
⊢ 𝐵 ⊆ 𝐵 |
| 7 | | ismrcd.b |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ 𝑉) |
| 8 | | elpwg 4603 |
. . . . . . . 8
⊢ (𝐵 ∈ 𝑉 → (𝐵 ∈ 𝒫 𝐵 ↔ 𝐵 ⊆ 𝐵)) |
| 9 | 7, 8 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝐵 ∈ 𝒫 𝐵 ↔ 𝐵 ⊆ 𝐵)) |
| 10 | 6, 9 | mpbiri 258 |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ 𝒫 𝐵) |
| 11 | 4, 10 | ffvelcdmd 7105 |
. . . . 5
⊢ (𝜑 → (𝐹‘𝐵) ∈ 𝒫 𝐵) |
| 12 | 11 | elpwid 4609 |
. . . 4
⊢ (𝜑 → (𝐹‘𝐵) ⊆ 𝐵) |
| 13 | | velpw 4605 |
. . . . . . 7
⊢ (𝑥 ∈ 𝒫 𝐵 ↔ 𝑥 ⊆ 𝐵) |
| 14 | | ismrcd.e |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵) → 𝑥 ⊆ (𝐹‘𝑥)) |
| 15 | 13, 14 | sylan2b 594 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 𝐵) → 𝑥 ⊆ (𝐹‘𝑥)) |
| 16 | 15 | ralrimiva 3146 |
. . . . 5
⊢ (𝜑 → ∀𝑥 ∈ 𝒫 𝐵𝑥 ⊆ (𝐹‘𝑥)) |
| 17 | | id 22 |
. . . . . . 7
⊢ (𝑥 = 𝐵 → 𝑥 = 𝐵) |
| 18 | | fveq2 6906 |
. . . . . . 7
⊢ (𝑥 = 𝐵 → (𝐹‘𝑥) = (𝐹‘𝐵)) |
| 19 | 17, 18 | sseq12d 4017 |
. . . . . 6
⊢ (𝑥 = 𝐵 → (𝑥 ⊆ (𝐹‘𝑥) ↔ 𝐵 ⊆ (𝐹‘𝐵))) |
| 20 | 19 | rspcva 3620 |
. . . . 5
⊢ ((𝐵 ∈ 𝒫 𝐵 ∧ ∀𝑥 ∈ 𝒫 𝐵𝑥 ⊆ (𝐹‘𝑥)) → 𝐵 ⊆ (𝐹‘𝐵)) |
| 21 | 10, 16, 20 | syl2anc 584 |
. . . 4
⊢ (𝜑 → 𝐵 ⊆ (𝐹‘𝐵)) |
| 22 | 12, 21 | eqssd 4001 |
. . 3
⊢ (𝜑 → (𝐹‘𝐵) = 𝐵) |
| 23 | 4 | ffnd 6737 |
. . . 4
⊢ (𝜑 → 𝐹 Fn 𝒫 𝐵) |
| 24 | | fnelfp 7195 |
. . . 4
⊢ ((𝐹 Fn 𝒫 𝐵 ∧ 𝐵 ∈ 𝒫 𝐵) → (𝐵 ∈ dom (𝐹 ∩ I ) ↔ (𝐹‘𝐵) = 𝐵)) |
| 25 | 23, 10, 24 | syl2anc 584 |
. . 3
⊢ (𝜑 → (𝐵 ∈ dom (𝐹 ∩ I ) ↔ (𝐹‘𝐵) = 𝐵)) |
| 26 | 22, 25 | mpbird 257 |
. 2
⊢ (𝜑 → 𝐵 ∈ dom (𝐹 ∩ I )) |
| 27 | | simp2 1138 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → 𝑧 ⊆ dom (𝐹 ∩ I )) |
| 28 | 5 | 3ad2ant1 1134 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → dom (𝐹 ∩ I ) ⊆ 𝒫 𝐵) |
| 29 | 27, 28 | sstrd 3994 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → 𝑧 ⊆ 𝒫 𝐵) |
| 30 | | simp3 1139 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → 𝑧 ≠ ∅) |
| 31 | | intssuni2 4973 |
. . . . . . . . . . . 12
⊢ ((𝑧 ⊆ 𝒫 𝐵 ∧ 𝑧 ≠ ∅) → ∩ 𝑧
⊆ ∪ 𝒫 𝐵) |
| 32 | 29, 30, 31 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → ∩ 𝑧
⊆ ∪ 𝒫 𝐵) |
| 33 | | unipw 5455 |
. . . . . . . . . . 11
⊢ ∪ 𝒫 𝐵 = 𝐵 |
| 34 | 32, 33 | sseqtrdi 4024 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → ∩ 𝑧
⊆ 𝐵) |
| 35 | | intex 5344 |
. . . . . . . . . . . 12
⊢ (𝑧 ≠ ∅ ↔ ∩ 𝑧
∈ V) |
| 36 | | elpwg 4603 |
. . . . . . . . . . . 12
⊢ (∩ 𝑧
∈ V → (∩ 𝑧 ∈ 𝒫 𝐵 ↔ ∩ 𝑧 ⊆ 𝐵)) |
| 37 | 35, 36 | sylbi 217 |
. . . . . . . . . . 11
⊢ (𝑧 ≠ ∅ → (∩ 𝑧
∈ 𝒫 𝐵 ↔
∩ 𝑧 ⊆ 𝐵)) |
| 38 | 37 | 3ad2ant3 1136 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → (∩ 𝑧
∈ 𝒫 𝐵 ↔
∩ 𝑧 ⊆ 𝐵)) |
| 39 | 34, 38 | mpbird 257 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → ∩ 𝑧
∈ 𝒫 𝐵) |
| 40 | 39 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥 ∈ 𝑧) → ∩ 𝑧 ∈ 𝒫 𝐵) |
| 41 | | ismrcd.m |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥) → (𝐹‘𝑦) ⊆ (𝐹‘𝑥)) |
| 42 | 41 | 3expib 1123 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥) → (𝐹‘𝑦) ⊆ (𝐹‘𝑥))) |
| 43 | 42 | alrimiv 1927 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑦((𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥) → (𝐹‘𝑦) ⊆ (𝐹‘𝑥))) |
| 44 | 43 | 3ad2ant1 1134 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → ∀𝑦((𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥) → (𝐹‘𝑦) ⊆ (𝐹‘𝑥))) |
| 45 | 44 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥 ∈ 𝑧) → ∀𝑦((𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥) → (𝐹‘𝑦) ⊆ (𝐹‘𝑥))) |
| 46 | 29 | sselda 3983 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥 ∈ 𝑧) → 𝑥 ∈ 𝒫 𝐵) |
| 47 | 46 | elpwid 4609 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥 ∈ 𝑧) → 𝑥 ⊆ 𝐵) |
| 48 | | intss1 4963 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝑧 → ∩ 𝑧 ⊆ 𝑥) |
| 49 | 48 | adantl 481 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥 ∈ 𝑧) → ∩ 𝑧 ⊆ 𝑥) |
| 50 | 47, 49 | jca 511 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥 ∈ 𝑧) → (𝑥 ⊆ 𝐵 ∧ ∩ 𝑧 ⊆ 𝑥)) |
| 51 | | sseq1 4009 |
. . . . . . . . . . 11
⊢ (𝑦 = ∩
𝑧 → (𝑦 ⊆ 𝑥 ↔ ∩ 𝑧 ⊆ 𝑥)) |
| 52 | 51 | anbi2d 630 |
. . . . . . . . . 10
⊢ (𝑦 = ∩
𝑧 → ((𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥) ↔ (𝑥 ⊆ 𝐵 ∧ ∩ 𝑧 ⊆ 𝑥))) |
| 53 | | fveq2 6906 |
. . . . . . . . . . 11
⊢ (𝑦 = ∩
𝑧 → (𝐹‘𝑦) = (𝐹‘∩ 𝑧)) |
| 54 | 53 | sseq1d 4015 |
. . . . . . . . . 10
⊢ (𝑦 = ∩
𝑧 → ((𝐹‘𝑦) ⊆ (𝐹‘𝑥) ↔ (𝐹‘∩ 𝑧) ⊆ (𝐹‘𝑥))) |
| 55 | 52, 54 | imbi12d 344 |
. . . . . . . . 9
⊢ (𝑦 = ∩
𝑧 → (((𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥) → (𝐹‘𝑦) ⊆ (𝐹‘𝑥)) ↔ ((𝑥 ⊆ 𝐵 ∧ ∩ 𝑧 ⊆ 𝑥) → (𝐹‘∩ 𝑧) ⊆ (𝐹‘𝑥)))) |
| 56 | 55 | spcgv 3596 |
. . . . . . . 8
⊢ (∩ 𝑧
∈ 𝒫 𝐵 →
(∀𝑦((𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥) → (𝐹‘𝑦) ⊆ (𝐹‘𝑥)) → ((𝑥 ⊆ 𝐵 ∧ ∩ 𝑧 ⊆ 𝑥) → (𝐹‘∩ 𝑧) ⊆ (𝐹‘𝑥)))) |
| 57 | 40, 45, 50, 56 | syl3c 66 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥 ∈ 𝑧) → (𝐹‘∩ 𝑧) ⊆ (𝐹‘𝑥)) |
| 58 | 27 | sselda 3983 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥 ∈ 𝑧) → 𝑥 ∈ dom (𝐹 ∩ I )) |
| 59 | 23 | 3ad2ant1 1134 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → 𝐹 Fn 𝒫 𝐵) |
| 60 | 59 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥 ∈ 𝑧) → 𝐹 Fn 𝒫 𝐵) |
| 61 | | fnelfp 7195 |
. . . . . . . . 9
⊢ ((𝐹 Fn 𝒫 𝐵 ∧ 𝑥 ∈ 𝒫 𝐵) → (𝑥 ∈ dom (𝐹 ∩ I ) ↔ (𝐹‘𝑥) = 𝑥)) |
| 62 | 60, 46, 61 | syl2anc 584 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥 ∈ 𝑧) → (𝑥 ∈ dom (𝐹 ∩ I ) ↔ (𝐹‘𝑥) = 𝑥)) |
| 63 | 58, 62 | mpbid 232 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥 ∈ 𝑧) → (𝐹‘𝑥) = 𝑥) |
| 64 | 57, 63 | sseqtrd 4020 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥 ∈ 𝑧) → (𝐹‘∩ 𝑧) ⊆ 𝑥) |
| 65 | 64 | ralrimiva 3146 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → ∀𝑥 ∈ 𝑧 (𝐹‘∩ 𝑧) ⊆ 𝑥) |
| 66 | | ssint 4964 |
. . . . 5
⊢ ((𝐹‘∩ 𝑧)
⊆ ∩ 𝑧 ↔ ∀𝑥 ∈ 𝑧 (𝐹‘∩ 𝑧) ⊆ 𝑥) |
| 67 | 65, 66 | sylibr 234 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → (𝐹‘∩ 𝑧) ⊆ ∩ 𝑧) |
| 68 | 16 | 3ad2ant1 1134 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → ∀𝑥 ∈ 𝒫 𝐵𝑥 ⊆ (𝐹‘𝑥)) |
| 69 | | id 22 |
. . . . . . 7
⊢ (𝑥 = ∩
𝑧 → 𝑥 = ∩ 𝑧) |
| 70 | | fveq2 6906 |
. . . . . . 7
⊢ (𝑥 = ∩
𝑧 → (𝐹‘𝑥) = (𝐹‘∩ 𝑧)) |
| 71 | 69, 70 | sseq12d 4017 |
. . . . . 6
⊢ (𝑥 = ∩
𝑧 → (𝑥 ⊆ (𝐹‘𝑥) ↔ ∩ 𝑧 ⊆ (𝐹‘∩ 𝑧))) |
| 72 | 71 | rspcva 3620 |
. . . . 5
⊢ ((∩ 𝑧
∈ 𝒫 𝐵 ∧
∀𝑥 ∈ 𝒫
𝐵𝑥 ⊆ (𝐹‘𝑥)) → ∩ 𝑧 ⊆ (𝐹‘∩ 𝑧)) |
| 73 | 39, 68, 72 | syl2anc 584 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → ∩ 𝑧
⊆ (𝐹‘∩ 𝑧)) |
| 74 | 67, 73 | eqssd 4001 |
. . 3
⊢ ((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → (𝐹‘∩ 𝑧) = ∩
𝑧) |
| 75 | | fnelfp 7195 |
. . . 4
⊢ ((𝐹 Fn 𝒫 𝐵 ∧ ∩ 𝑧 ∈ 𝒫 𝐵) → (∩ 𝑧
∈ dom (𝐹 ∩ I )
↔ (𝐹‘∩ 𝑧) =
∩ 𝑧)) |
| 76 | 59, 39, 75 | syl2anc 584 |
. . 3
⊢ ((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → (∩ 𝑧
∈ dom (𝐹 ∩ I )
↔ (𝐹‘∩ 𝑧) =
∩ 𝑧)) |
| 77 | 74, 76 | mpbird 257 |
. 2
⊢ ((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → ∩ 𝑧
∈ dom (𝐹 ∩ I
)) |
| 78 | 5, 26, 77 | ismred 17645 |
1
⊢ (𝜑 → dom (𝐹 ∩ I ) ∈ (Moore‘𝐵)) |