Step | Hyp | Ref
| Expression |
1 | | inss1 4157 |
. . . 4
⊢ (𝐹 ∩ I ) ⊆ 𝐹 |
2 | | dmss 5785 |
. . . 4
⊢ ((𝐹 ∩ I ) ⊆ 𝐹 → dom (𝐹 ∩ I ) ⊆ dom 𝐹) |
3 | 1, 2 | ax-mp 5 |
. . 3
⊢ dom
(𝐹 ∩ I ) ⊆ dom
𝐹 |
4 | | ismrcd.f |
. . 3
⊢ (𝜑 → 𝐹:𝒫 𝐵⟶𝒫 𝐵) |
5 | 3, 4 | fssdm 6583 |
. 2
⊢ (𝜑 → dom (𝐹 ∩ I ) ⊆ 𝒫 𝐵) |
6 | | ssid 3937 |
. . . . . . 7
⊢ 𝐵 ⊆ 𝐵 |
7 | | ismrcd.b |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ 𝑉) |
8 | | elpwg 4530 |
. . . . . . . 8
⊢ (𝐵 ∈ 𝑉 → (𝐵 ∈ 𝒫 𝐵 ↔ 𝐵 ⊆ 𝐵)) |
9 | 7, 8 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝐵 ∈ 𝒫 𝐵 ↔ 𝐵 ⊆ 𝐵)) |
10 | 6, 9 | mpbiri 261 |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ 𝒫 𝐵) |
11 | 4, 10 | ffvelrnd 6923 |
. . . . 5
⊢ (𝜑 → (𝐹‘𝐵) ∈ 𝒫 𝐵) |
12 | 11 | elpwid 4538 |
. . . 4
⊢ (𝜑 → (𝐹‘𝐵) ⊆ 𝐵) |
13 | | velpw 4532 |
. . . . . . 7
⊢ (𝑥 ∈ 𝒫 𝐵 ↔ 𝑥 ⊆ 𝐵) |
14 | | ismrcd.e |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵) → 𝑥 ⊆ (𝐹‘𝑥)) |
15 | 13, 14 | sylan2b 597 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 𝐵) → 𝑥 ⊆ (𝐹‘𝑥)) |
16 | 15 | ralrimiva 3106 |
. . . . 5
⊢ (𝜑 → ∀𝑥 ∈ 𝒫 𝐵𝑥 ⊆ (𝐹‘𝑥)) |
17 | | id 22 |
. . . . . . 7
⊢ (𝑥 = 𝐵 → 𝑥 = 𝐵) |
18 | | fveq2 6735 |
. . . . . . 7
⊢ (𝑥 = 𝐵 → (𝐹‘𝑥) = (𝐹‘𝐵)) |
19 | 17, 18 | sseq12d 3948 |
. . . . . 6
⊢ (𝑥 = 𝐵 → (𝑥 ⊆ (𝐹‘𝑥) ↔ 𝐵 ⊆ (𝐹‘𝐵))) |
20 | 19 | rspcva 3547 |
. . . . 5
⊢ ((𝐵 ∈ 𝒫 𝐵 ∧ ∀𝑥 ∈ 𝒫 𝐵𝑥 ⊆ (𝐹‘𝑥)) → 𝐵 ⊆ (𝐹‘𝐵)) |
21 | 10, 16, 20 | syl2anc 587 |
. . . 4
⊢ (𝜑 → 𝐵 ⊆ (𝐹‘𝐵)) |
22 | 12, 21 | eqssd 3932 |
. . 3
⊢ (𝜑 → (𝐹‘𝐵) = 𝐵) |
23 | 4 | ffnd 6564 |
. . . 4
⊢ (𝜑 → 𝐹 Fn 𝒫 𝐵) |
24 | | fnelfp 7008 |
. . . 4
⊢ ((𝐹 Fn 𝒫 𝐵 ∧ 𝐵 ∈ 𝒫 𝐵) → (𝐵 ∈ dom (𝐹 ∩ I ) ↔ (𝐹‘𝐵) = 𝐵)) |
25 | 23, 10, 24 | syl2anc 587 |
. . 3
⊢ (𝜑 → (𝐵 ∈ dom (𝐹 ∩ I ) ↔ (𝐹‘𝐵) = 𝐵)) |
26 | 22, 25 | mpbird 260 |
. 2
⊢ (𝜑 → 𝐵 ∈ dom (𝐹 ∩ I )) |
27 | | simp2 1139 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → 𝑧 ⊆ dom (𝐹 ∩ I )) |
28 | 5 | 3ad2ant1 1135 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → dom (𝐹 ∩ I ) ⊆ 𝒫 𝐵) |
29 | 27, 28 | sstrd 3925 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → 𝑧 ⊆ 𝒫 𝐵) |
30 | | simp3 1140 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → 𝑧 ≠ ∅) |
31 | | intssuni2 4898 |
. . . . . . . . . . . 12
⊢ ((𝑧 ⊆ 𝒫 𝐵 ∧ 𝑧 ≠ ∅) → ∩ 𝑧
⊆ ∪ 𝒫 𝐵) |
32 | 29, 30, 31 | syl2anc 587 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → ∩ 𝑧
⊆ ∪ 𝒫 𝐵) |
33 | | unipw 5349 |
. . . . . . . . . . 11
⊢ ∪ 𝒫 𝐵 = 𝐵 |
34 | 32, 33 | sseqtrdi 3965 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → ∩ 𝑧
⊆ 𝐵) |
35 | | intex 5244 |
. . . . . . . . . . . 12
⊢ (𝑧 ≠ ∅ ↔ ∩ 𝑧
∈ V) |
36 | | elpwg 4530 |
. . . . . . . . . . . 12
⊢ (∩ 𝑧
∈ V → (∩ 𝑧 ∈ 𝒫 𝐵 ↔ ∩ 𝑧 ⊆ 𝐵)) |
37 | 35, 36 | sylbi 220 |
. . . . . . . . . . 11
⊢ (𝑧 ≠ ∅ → (∩ 𝑧
∈ 𝒫 𝐵 ↔
∩ 𝑧 ⊆ 𝐵)) |
38 | 37 | 3ad2ant3 1137 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → (∩ 𝑧
∈ 𝒫 𝐵 ↔
∩ 𝑧 ⊆ 𝐵)) |
39 | 34, 38 | mpbird 260 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → ∩ 𝑧
∈ 𝒫 𝐵) |
40 | 39 | adantr 484 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥 ∈ 𝑧) → ∩ 𝑧 ∈ 𝒫 𝐵) |
41 | | ismrcd.m |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥) → (𝐹‘𝑦) ⊆ (𝐹‘𝑥)) |
42 | 41 | 3expib 1124 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥) → (𝐹‘𝑦) ⊆ (𝐹‘𝑥))) |
43 | 42 | alrimiv 1935 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑦((𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥) → (𝐹‘𝑦) ⊆ (𝐹‘𝑥))) |
44 | 43 | 3ad2ant1 1135 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → ∀𝑦((𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥) → (𝐹‘𝑦) ⊆ (𝐹‘𝑥))) |
45 | 44 | adantr 484 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥 ∈ 𝑧) → ∀𝑦((𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥) → (𝐹‘𝑦) ⊆ (𝐹‘𝑥))) |
46 | 29 | sselda 3915 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥 ∈ 𝑧) → 𝑥 ∈ 𝒫 𝐵) |
47 | 46 | elpwid 4538 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥 ∈ 𝑧) → 𝑥 ⊆ 𝐵) |
48 | | intss1 4888 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝑧 → ∩ 𝑧 ⊆ 𝑥) |
49 | 48 | adantl 485 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥 ∈ 𝑧) → ∩ 𝑧 ⊆ 𝑥) |
50 | 47, 49 | jca 515 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥 ∈ 𝑧) → (𝑥 ⊆ 𝐵 ∧ ∩ 𝑧 ⊆ 𝑥)) |
51 | | sseq1 3940 |
. . . . . . . . . . 11
⊢ (𝑦 = ∩
𝑧 → (𝑦 ⊆ 𝑥 ↔ ∩ 𝑧 ⊆ 𝑥)) |
52 | 51 | anbi2d 632 |
. . . . . . . . . 10
⊢ (𝑦 = ∩
𝑧 → ((𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥) ↔ (𝑥 ⊆ 𝐵 ∧ ∩ 𝑧 ⊆ 𝑥))) |
53 | | fveq2 6735 |
. . . . . . . . . . 11
⊢ (𝑦 = ∩
𝑧 → (𝐹‘𝑦) = (𝐹‘∩ 𝑧)) |
54 | 53 | sseq1d 3946 |
. . . . . . . . . 10
⊢ (𝑦 = ∩
𝑧 → ((𝐹‘𝑦) ⊆ (𝐹‘𝑥) ↔ (𝐹‘∩ 𝑧) ⊆ (𝐹‘𝑥))) |
55 | 52, 54 | imbi12d 348 |
. . . . . . . . 9
⊢ (𝑦 = ∩
𝑧 → (((𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥) → (𝐹‘𝑦) ⊆ (𝐹‘𝑥)) ↔ ((𝑥 ⊆ 𝐵 ∧ ∩ 𝑧 ⊆ 𝑥) → (𝐹‘∩ 𝑧) ⊆ (𝐹‘𝑥)))) |
56 | 55 | spcgv 3523 |
. . . . . . . 8
⊢ (∩ 𝑧
∈ 𝒫 𝐵 →
(∀𝑦((𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥) → (𝐹‘𝑦) ⊆ (𝐹‘𝑥)) → ((𝑥 ⊆ 𝐵 ∧ ∩ 𝑧 ⊆ 𝑥) → (𝐹‘∩ 𝑧) ⊆ (𝐹‘𝑥)))) |
57 | 40, 45, 50, 56 | syl3c 66 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥 ∈ 𝑧) → (𝐹‘∩ 𝑧) ⊆ (𝐹‘𝑥)) |
58 | 27 | sselda 3915 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥 ∈ 𝑧) → 𝑥 ∈ dom (𝐹 ∩ I )) |
59 | 23 | 3ad2ant1 1135 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → 𝐹 Fn 𝒫 𝐵) |
60 | 59 | adantr 484 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥 ∈ 𝑧) → 𝐹 Fn 𝒫 𝐵) |
61 | | fnelfp 7008 |
. . . . . . . . 9
⊢ ((𝐹 Fn 𝒫 𝐵 ∧ 𝑥 ∈ 𝒫 𝐵) → (𝑥 ∈ dom (𝐹 ∩ I ) ↔ (𝐹‘𝑥) = 𝑥)) |
62 | 60, 46, 61 | syl2anc 587 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥 ∈ 𝑧) → (𝑥 ∈ dom (𝐹 ∩ I ) ↔ (𝐹‘𝑥) = 𝑥)) |
63 | 58, 62 | mpbid 235 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥 ∈ 𝑧) → (𝐹‘𝑥) = 𝑥) |
64 | 57, 63 | sseqtrd 3955 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥 ∈ 𝑧) → (𝐹‘∩ 𝑧) ⊆ 𝑥) |
65 | 64 | ralrimiva 3106 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → ∀𝑥 ∈ 𝑧 (𝐹‘∩ 𝑧) ⊆ 𝑥) |
66 | | ssint 4889 |
. . . . 5
⊢ ((𝐹‘∩ 𝑧)
⊆ ∩ 𝑧 ↔ ∀𝑥 ∈ 𝑧 (𝐹‘∩ 𝑧) ⊆ 𝑥) |
67 | 65, 66 | sylibr 237 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → (𝐹‘∩ 𝑧) ⊆ ∩ 𝑧) |
68 | 16 | 3ad2ant1 1135 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → ∀𝑥 ∈ 𝒫 𝐵𝑥 ⊆ (𝐹‘𝑥)) |
69 | | id 22 |
. . . . . . 7
⊢ (𝑥 = ∩
𝑧 → 𝑥 = ∩ 𝑧) |
70 | | fveq2 6735 |
. . . . . . 7
⊢ (𝑥 = ∩
𝑧 → (𝐹‘𝑥) = (𝐹‘∩ 𝑧)) |
71 | 69, 70 | sseq12d 3948 |
. . . . . 6
⊢ (𝑥 = ∩
𝑧 → (𝑥 ⊆ (𝐹‘𝑥) ↔ ∩ 𝑧 ⊆ (𝐹‘∩ 𝑧))) |
72 | 71 | rspcva 3547 |
. . . . 5
⊢ ((∩ 𝑧
∈ 𝒫 𝐵 ∧
∀𝑥 ∈ 𝒫
𝐵𝑥 ⊆ (𝐹‘𝑥)) → ∩ 𝑧 ⊆ (𝐹‘∩ 𝑧)) |
73 | 39, 68, 72 | syl2anc 587 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → ∩ 𝑧
⊆ (𝐹‘∩ 𝑧)) |
74 | 67, 73 | eqssd 3932 |
. . 3
⊢ ((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → (𝐹‘∩ 𝑧) = ∩
𝑧) |
75 | | fnelfp 7008 |
. . . 4
⊢ ((𝐹 Fn 𝒫 𝐵 ∧ ∩ 𝑧 ∈ 𝒫 𝐵) → (∩ 𝑧
∈ dom (𝐹 ∩ I )
↔ (𝐹‘∩ 𝑧) =
∩ 𝑧)) |
76 | 59, 39, 75 | syl2anc 587 |
. . 3
⊢ ((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → (∩ 𝑧
∈ dom (𝐹 ∩ I )
↔ (𝐹‘∩ 𝑧) =
∩ 𝑧)) |
77 | 74, 76 | mpbird 260 |
. 2
⊢ ((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → ∩ 𝑧
∈ dom (𝐹 ∩ I
)) |
78 | 5, 26, 77 | ismred 17129 |
1
⊢ (𝜑 → dom (𝐹 ∩ I ) ∈ (Moore‘𝐵)) |