Step | Hyp | Ref
| Expression |
1 | | inss1 3795 |
. . . 4
⊢ (𝐹 ∩ I ) ⊆ 𝐹 |
2 | | dmss 5245 |
. . . 4
⊢ ((𝐹 ∩ I ) ⊆ 𝐹 → dom (𝐹 ∩ I ) ⊆ dom 𝐹) |
3 | 1, 2 | ax-mp 5 |
. . 3
⊢ dom
(𝐹 ∩ I ) ⊆ dom
𝐹 |
4 | | ismrcd.f |
. . . 4
⊢ (𝜑 → 𝐹:𝒫 𝐵⟶𝒫 𝐵) |
5 | | fdm 5964 |
. . . 4
⊢ (𝐹:𝒫 𝐵⟶𝒫 𝐵 → dom 𝐹 = 𝒫 𝐵) |
6 | 4, 5 | syl 17 |
. . 3
⊢ (𝜑 → dom 𝐹 = 𝒫 𝐵) |
7 | 3, 6 | syl5sseq 3616 |
. 2
⊢ (𝜑 → dom (𝐹 ∩ I ) ⊆ 𝒫 𝐵) |
8 | | ssid 3587 |
. . . . . . 7
⊢ 𝐵 ⊆ 𝐵 |
9 | | ismrcd.b |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ 𝑉) |
10 | | elpwg 4116 |
. . . . . . . 8
⊢ (𝐵 ∈ 𝑉 → (𝐵 ∈ 𝒫 𝐵 ↔ 𝐵 ⊆ 𝐵)) |
11 | 9, 10 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝐵 ∈ 𝒫 𝐵 ↔ 𝐵 ⊆ 𝐵)) |
12 | 8, 11 | mpbiri 247 |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ 𝒫 𝐵) |
13 | 4, 12 | ffvelrnd 6268 |
. . . . 5
⊢ (𝜑 → (𝐹‘𝐵) ∈ 𝒫 𝐵) |
14 | 13 | elpwid 4118 |
. . . 4
⊢ (𝜑 → (𝐹‘𝐵) ⊆ 𝐵) |
15 | | selpw 4115 |
. . . . . . 7
⊢ (𝑥 ∈ 𝒫 𝐵 ↔ 𝑥 ⊆ 𝐵) |
16 | | ismrcd.e |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵) → 𝑥 ⊆ (𝐹‘𝑥)) |
17 | 15, 16 | sylan2b 491 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 𝐵) → 𝑥 ⊆ (𝐹‘𝑥)) |
18 | 17 | ralrimiva 2949 |
. . . . 5
⊢ (𝜑 → ∀𝑥 ∈ 𝒫 𝐵𝑥 ⊆ (𝐹‘𝑥)) |
19 | | id 22 |
. . . . . . 7
⊢ (𝑥 = 𝐵 → 𝑥 = 𝐵) |
20 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑥 = 𝐵 → (𝐹‘𝑥) = (𝐹‘𝐵)) |
21 | 19, 20 | sseq12d 3597 |
. . . . . 6
⊢ (𝑥 = 𝐵 → (𝑥 ⊆ (𝐹‘𝑥) ↔ 𝐵 ⊆ (𝐹‘𝐵))) |
22 | 21 | rspcva 3280 |
. . . . 5
⊢ ((𝐵 ∈ 𝒫 𝐵 ∧ ∀𝑥 ∈ 𝒫 𝐵𝑥 ⊆ (𝐹‘𝑥)) → 𝐵 ⊆ (𝐹‘𝐵)) |
23 | 12, 18, 22 | syl2anc 691 |
. . . 4
⊢ (𝜑 → 𝐵 ⊆ (𝐹‘𝐵)) |
24 | 14, 23 | eqssd 3585 |
. . 3
⊢ (𝜑 → (𝐹‘𝐵) = 𝐵) |
25 | | ffn 5958 |
. . . . 5
⊢ (𝐹:𝒫 𝐵⟶𝒫 𝐵 → 𝐹 Fn 𝒫 𝐵) |
26 | 4, 25 | syl 17 |
. . . 4
⊢ (𝜑 → 𝐹 Fn 𝒫 𝐵) |
27 | | fnelfp 6346 |
. . . 4
⊢ ((𝐹 Fn 𝒫 𝐵 ∧ 𝐵 ∈ 𝒫 𝐵) → (𝐵 ∈ dom (𝐹 ∩ I ) ↔ (𝐹‘𝐵) = 𝐵)) |
28 | 26, 12, 27 | syl2anc 691 |
. . 3
⊢ (𝜑 → (𝐵 ∈ dom (𝐹 ∩ I ) ↔ (𝐹‘𝐵) = 𝐵)) |
29 | 24, 28 | mpbird 246 |
. 2
⊢ (𝜑 → 𝐵 ∈ dom (𝐹 ∩ I )) |
30 | | simp2 1055 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → 𝑧 ⊆ dom (𝐹 ∩ I )) |
31 | 7 | 3ad2ant1 1075 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → dom (𝐹 ∩ I ) ⊆ 𝒫 𝐵) |
32 | 30, 31 | sstrd 3578 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → 𝑧 ⊆ 𝒫 𝐵) |
33 | | simp3 1056 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → 𝑧 ≠ ∅) |
34 | | intssuni2 4437 |
. . . . . . . . . . . 12
⊢ ((𝑧 ⊆ 𝒫 𝐵 ∧ 𝑧 ≠ ∅) → ∩ 𝑧
⊆ ∪ 𝒫 𝐵) |
35 | 32, 33, 34 | syl2anc 691 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → ∩ 𝑧
⊆ ∪ 𝒫 𝐵) |
36 | | unipw 4845 |
. . . . . . . . . . 11
⊢ ∪ 𝒫 𝐵 = 𝐵 |
37 | 35, 36 | syl6sseq 3614 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → ∩ 𝑧
⊆ 𝐵) |
38 | | intex 4747 |
. . . . . . . . . . . 12
⊢ (𝑧 ≠ ∅ ↔ ∩ 𝑧
∈ V) |
39 | | elpwg 4116 |
. . . . . . . . . . . 12
⊢ (∩ 𝑧
∈ V → (∩ 𝑧 ∈ 𝒫 𝐵 ↔ ∩ 𝑧 ⊆ 𝐵)) |
40 | 38, 39 | sylbi 206 |
. . . . . . . . . . 11
⊢ (𝑧 ≠ ∅ → (∩ 𝑧
∈ 𝒫 𝐵 ↔
∩ 𝑧 ⊆ 𝐵)) |
41 | 40 | 3ad2ant3 1077 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → (∩ 𝑧
∈ 𝒫 𝐵 ↔
∩ 𝑧 ⊆ 𝐵)) |
42 | 37, 41 | mpbird 246 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → ∩ 𝑧
∈ 𝒫 𝐵) |
43 | 42 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥 ∈ 𝑧) → ∩ 𝑧 ∈ 𝒫 𝐵) |
44 | | ismrcd.m |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥) → (𝐹‘𝑦) ⊆ (𝐹‘𝑥)) |
45 | 44 | 3expib 1260 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥) → (𝐹‘𝑦) ⊆ (𝐹‘𝑥))) |
46 | 45 | alrimiv 1842 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑦((𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥) → (𝐹‘𝑦) ⊆ (𝐹‘𝑥))) |
47 | 46 | 3ad2ant1 1075 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → ∀𝑦((𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥) → (𝐹‘𝑦) ⊆ (𝐹‘𝑥))) |
48 | 47 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥 ∈ 𝑧) → ∀𝑦((𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥) → (𝐹‘𝑦) ⊆ (𝐹‘𝑥))) |
49 | 32 | sselda 3568 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥 ∈ 𝑧) → 𝑥 ∈ 𝒫 𝐵) |
50 | 49 | elpwid 4118 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥 ∈ 𝑧) → 𝑥 ⊆ 𝐵) |
51 | | intss1 4427 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝑧 → ∩ 𝑧 ⊆ 𝑥) |
52 | 51 | adantl 481 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥 ∈ 𝑧) → ∩ 𝑧 ⊆ 𝑥) |
53 | 50, 52 | jca 553 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥 ∈ 𝑧) → (𝑥 ⊆ 𝐵 ∧ ∩ 𝑧 ⊆ 𝑥)) |
54 | | sseq1 3589 |
. . . . . . . . . . 11
⊢ (𝑦 = ∩
𝑧 → (𝑦 ⊆ 𝑥 ↔ ∩ 𝑧 ⊆ 𝑥)) |
55 | 54 | anbi2d 736 |
. . . . . . . . . 10
⊢ (𝑦 = ∩
𝑧 → ((𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥) ↔ (𝑥 ⊆ 𝐵 ∧ ∩ 𝑧 ⊆ 𝑥))) |
56 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑦 = ∩
𝑧 → (𝐹‘𝑦) = (𝐹‘∩ 𝑧)) |
57 | 56 | sseq1d 3595 |
. . . . . . . . . 10
⊢ (𝑦 = ∩
𝑧 → ((𝐹‘𝑦) ⊆ (𝐹‘𝑥) ↔ (𝐹‘∩ 𝑧) ⊆ (𝐹‘𝑥))) |
58 | 55, 57 | imbi12d 333 |
. . . . . . . . 9
⊢ (𝑦 = ∩
𝑧 → (((𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥) → (𝐹‘𝑦) ⊆ (𝐹‘𝑥)) ↔ ((𝑥 ⊆ 𝐵 ∧ ∩ 𝑧 ⊆ 𝑥) → (𝐹‘∩ 𝑧) ⊆ (𝐹‘𝑥)))) |
59 | 58 | spcgv 3266 |
. . . . . . . 8
⊢ (∩ 𝑧
∈ 𝒫 𝐵 →
(∀𝑦((𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥) → (𝐹‘𝑦) ⊆ (𝐹‘𝑥)) → ((𝑥 ⊆ 𝐵 ∧ ∩ 𝑧 ⊆ 𝑥) → (𝐹‘∩ 𝑧) ⊆ (𝐹‘𝑥)))) |
60 | 43, 48, 53, 59 | syl3c 64 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥 ∈ 𝑧) → (𝐹‘∩ 𝑧) ⊆ (𝐹‘𝑥)) |
61 | 30 | sselda 3568 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥 ∈ 𝑧) → 𝑥 ∈ dom (𝐹 ∩ I )) |
62 | 26 | 3ad2ant1 1075 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → 𝐹 Fn 𝒫 𝐵) |
63 | 62 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥 ∈ 𝑧) → 𝐹 Fn 𝒫 𝐵) |
64 | | fnelfp 6346 |
. . . . . . . . 9
⊢ ((𝐹 Fn 𝒫 𝐵 ∧ 𝑥 ∈ 𝒫 𝐵) → (𝑥 ∈ dom (𝐹 ∩ I ) ↔ (𝐹‘𝑥) = 𝑥)) |
65 | 63, 49, 64 | syl2anc 691 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥 ∈ 𝑧) → (𝑥 ∈ dom (𝐹 ∩ I ) ↔ (𝐹‘𝑥) = 𝑥)) |
66 | 61, 65 | mpbid 221 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥 ∈ 𝑧) → (𝐹‘𝑥) = 𝑥) |
67 | 60, 66 | sseqtrd 3604 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥 ∈ 𝑧) → (𝐹‘∩ 𝑧) ⊆ 𝑥) |
68 | 67 | ralrimiva 2949 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → ∀𝑥 ∈ 𝑧 (𝐹‘∩ 𝑧) ⊆ 𝑥) |
69 | | ssint 4428 |
. . . . 5
⊢ ((𝐹‘∩ 𝑧)
⊆ ∩ 𝑧 ↔ ∀𝑥 ∈ 𝑧 (𝐹‘∩ 𝑧) ⊆ 𝑥) |
70 | 68, 69 | sylibr 223 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → (𝐹‘∩ 𝑧) ⊆ ∩ 𝑧) |
71 | 18 | 3ad2ant1 1075 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → ∀𝑥 ∈ 𝒫 𝐵𝑥 ⊆ (𝐹‘𝑥)) |
72 | | id 22 |
. . . . . . 7
⊢ (𝑥 = ∩
𝑧 → 𝑥 = ∩ 𝑧) |
73 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑥 = ∩
𝑧 → (𝐹‘𝑥) = (𝐹‘∩ 𝑧)) |
74 | 72, 73 | sseq12d 3597 |
. . . . . 6
⊢ (𝑥 = ∩
𝑧 → (𝑥 ⊆ (𝐹‘𝑥) ↔ ∩ 𝑧 ⊆ (𝐹‘∩ 𝑧))) |
75 | 74 | rspcva 3280 |
. . . . 5
⊢ ((∩ 𝑧
∈ 𝒫 𝐵 ∧
∀𝑥 ∈ 𝒫
𝐵𝑥 ⊆ (𝐹‘𝑥)) → ∩ 𝑧 ⊆ (𝐹‘∩ 𝑧)) |
76 | 42, 71, 75 | syl2anc 691 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → ∩ 𝑧
⊆ (𝐹‘∩ 𝑧)) |
77 | 70, 76 | eqssd 3585 |
. . 3
⊢ ((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → (𝐹‘∩ 𝑧) = ∩
𝑧) |
78 | | fnelfp 6346 |
. . . 4
⊢ ((𝐹 Fn 𝒫 𝐵 ∧ ∩ 𝑧 ∈ 𝒫 𝐵) → (∩ 𝑧
∈ dom (𝐹 ∩ I )
↔ (𝐹‘∩ 𝑧) =
∩ 𝑧)) |
79 | 62, 42, 78 | syl2anc 691 |
. . 3
⊢ ((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → (∩ 𝑧
∈ dom (𝐹 ∩ I )
↔ (𝐹‘∩ 𝑧) =
∩ 𝑧)) |
80 | 77, 79 | mpbird 246 |
. 2
⊢ ((𝜑 ∧ 𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → ∩ 𝑧
∈ dom (𝐹 ∩ I
)) |
81 | 7, 29, 80 | ismred 16085 |
1
⊢ (𝜑 → dom (𝐹 ∩ I ) ∈ (Moore‘𝐵)) |