Step | Hyp | Ref
| Expression |
1 | | ismrcd.f |
. . 3
⊢ (𝜑 → 𝐹:𝒫 𝐵⟶𝒫 𝐵) |
2 | | ffn 6045 |
. . 3
⊢ (𝐹:𝒫 𝐵⟶𝒫 𝐵 → 𝐹 Fn 𝒫 𝐵) |
3 | 1, 2 | syl 17 |
. 2
⊢ (𝜑 → 𝐹 Fn 𝒫 𝐵) |
4 | | ismrcd.b |
. . . 4
⊢ (𝜑 → 𝐵 ∈ 𝑉) |
5 | | ismrcd.e |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵) → 𝑥 ⊆ (𝐹‘𝑥)) |
6 | | ismrcd.m |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥) → (𝐹‘𝑦) ⊆ (𝐹‘𝑥)) |
7 | | ismrcd.i |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵) → (𝐹‘(𝐹‘𝑥)) = (𝐹‘𝑥)) |
8 | 4, 1, 5, 6, 7 | ismrcd1 37261 |
. . 3
⊢ (𝜑 → dom (𝐹 ∩ I ) ∈ (Moore‘𝐵)) |
9 | | eqid 2622 |
. . . 4
⊢
(mrCls‘dom (𝐹
∩ I )) = (mrCls‘dom (𝐹 ∩ I )) |
10 | 9 | mrcf 16269 |
. . 3
⊢ (dom
(𝐹 ∩ I ) ∈
(Moore‘𝐵) →
(mrCls‘dom (𝐹 ∩ I
)):𝒫 𝐵⟶dom
(𝐹 ∩ I
)) |
11 | | ffn 6045 |
. . 3
⊢
((mrCls‘dom (𝐹
∩ I )):𝒫 𝐵⟶dom (𝐹 ∩ I ) → (mrCls‘dom (𝐹 ∩ I )) Fn 𝒫 𝐵) |
12 | 8, 10, 11 | 3syl 18 |
. 2
⊢ (𝜑 → (mrCls‘dom (𝐹 ∩ I )) Fn 𝒫 𝐵) |
13 | 8, 9 | mrcssvd 16283 |
. . . . . 6
⊢ (𝜑 → ((mrCls‘dom (𝐹 ∩ I ))‘𝑧) ⊆ 𝐵) |
14 | 13 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ 𝒫 𝐵) → ((mrCls‘dom (𝐹 ∩ I ))‘𝑧) ⊆ 𝐵) |
15 | | elpwi 4168 |
. . . . . 6
⊢ (𝑧 ∈ 𝒫 𝐵 → 𝑧 ⊆ 𝐵) |
16 | 9 | mrcssid 16277 |
. . . . . 6
⊢ ((dom
(𝐹 ∩ I ) ∈
(Moore‘𝐵) ∧ 𝑧 ⊆ 𝐵) → 𝑧 ⊆ ((mrCls‘dom (𝐹 ∩ I ))‘𝑧)) |
17 | 8, 15, 16 | syl2an 494 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ 𝒫 𝐵) → 𝑧 ⊆ ((mrCls‘dom (𝐹 ∩ I ))‘𝑧)) |
18 | 6 | 3expib 1268 |
. . . . . . . 8
⊢ (𝜑 → ((𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥) → (𝐹‘𝑦) ⊆ (𝐹‘𝑥))) |
19 | 18 | alrimivv 1856 |
. . . . . . 7
⊢ (𝜑 → ∀𝑦∀𝑥((𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥) → (𝐹‘𝑦) ⊆ (𝐹‘𝑥))) |
20 | | vex 3203 |
. . . . . . . 8
⊢ 𝑧 ∈ V |
21 | | fvex 6201 |
. . . . . . . 8
⊢
((mrCls‘dom (𝐹
∩ I ))‘𝑧) ∈
V |
22 | | sseq1 3626 |
. . . . . . . . . . . 12
⊢ (𝑥 = ((mrCls‘dom (𝐹 ∩ I ))‘𝑧) → (𝑥 ⊆ 𝐵 ↔ ((mrCls‘dom (𝐹 ∩ I ))‘𝑧) ⊆ 𝐵)) |
23 | 22 | adantl 482 |
. . . . . . . . . . 11
⊢ ((𝑦 = 𝑧 ∧ 𝑥 = ((mrCls‘dom (𝐹 ∩ I ))‘𝑧)) → (𝑥 ⊆ 𝐵 ↔ ((mrCls‘dom (𝐹 ∩ I ))‘𝑧) ⊆ 𝐵)) |
24 | | sseq12 3628 |
. . . . . . . . . . 11
⊢ ((𝑦 = 𝑧 ∧ 𝑥 = ((mrCls‘dom (𝐹 ∩ I ))‘𝑧)) → (𝑦 ⊆ 𝑥 ↔ 𝑧 ⊆ ((mrCls‘dom (𝐹 ∩ I ))‘𝑧))) |
25 | 23, 24 | anbi12d 747 |
. . . . . . . . . 10
⊢ ((𝑦 = 𝑧 ∧ 𝑥 = ((mrCls‘dom (𝐹 ∩ I ))‘𝑧)) → ((𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥) ↔ (((mrCls‘dom (𝐹 ∩ I ))‘𝑧) ⊆ 𝐵 ∧ 𝑧 ⊆ ((mrCls‘dom (𝐹 ∩ I ))‘𝑧)))) |
26 | | fveq2 6191 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑧 → (𝐹‘𝑦) = (𝐹‘𝑧)) |
27 | | fveq2 6191 |
. . . . . . . . . . 11
⊢ (𝑥 = ((mrCls‘dom (𝐹 ∩ I ))‘𝑧) → (𝐹‘𝑥) = (𝐹‘((mrCls‘dom (𝐹 ∩ I ))‘𝑧))) |
28 | | sseq12 3628 |
. . . . . . . . . . 11
⊢ (((𝐹‘𝑦) = (𝐹‘𝑧) ∧ (𝐹‘𝑥) = (𝐹‘((mrCls‘dom (𝐹 ∩ I ))‘𝑧))) → ((𝐹‘𝑦) ⊆ (𝐹‘𝑥) ↔ (𝐹‘𝑧) ⊆ (𝐹‘((mrCls‘dom (𝐹 ∩ I ))‘𝑧)))) |
29 | 26, 27, 28 | syl2an 494 |
. . . . . . . . . 10
⊢ ((𝑦 = 𝑧 ∧ 𝑥 = ((mrCls‘dom (𝐹 ∩ I ))‘𝑧)) → ((𝐹‘𝑦) ⊆ (𝐹‘𝑥) ↔ (𝐹‘𝑧) ⊆ (𝐹‘((mrCls‘dom (𝐹 ∩ I ))‘𝑧)))) |
30 | 25, 29 | imbi12d 334 |
. . . . . . . . 9
⊢ ((𝑦 = 𝑧 ∧ 𝑥 = ((mrCls‘dom (𝐹 ∩ I ))‘𝑧)) → (((𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥) → (𝐹‘𝑦) ⊆ (𝐹‘𝑥)) ↔ ((((mrCls‘dom (𝐹 ∩ I ))‘𝑧) ⊆ 𝐵 ∧ 𝑧 ⊆ ((mrCls‘dom (𝐹 ∩ I ))‘𝑧)) → (𝐹‘𝑧) ⊆ (𝐹‘((mrCls‘dom (𝐹 ∩ I ))‘𝑧))))) |
31 | 30 | spc2gv 3296 |
. . . . . . . 8
⊢ ((𝑧 ∈ V ∧
((mrCls‘dom (𝐹 ∩
I ))‘𝑧) ∈ V)
→ (∀𝑦∀𝑥((𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥) → (𝐹‘𝑦) ⊆ (𝐹‘𝑥)) → ((((mrCls‘dom (𝐹 ∩ I ))‘𝑧) ⊆ 𝐵 ∧ 𝑧 ⊆ ((mrCls‘dom (𝐹 ∩ I ))‘𝑧)) → (𝐹‘𝑧) ⊆ (𝐹‘((mrCls‘dom (𝐹 ∩ I ))‘𝑧))))) |
32 | 20, 21, 31 | mp2an 708 |
. . . . . . 7
⊢
(∀𝑦∀𝑥((𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥) → (𝐹‘𝑦) ⊆ (𝐹‘𝑥)) → ((((mrCls‘dom (𝐹 ∩ I ))‘𝑧) ⊆ 𝐵 ∧ 𝑧 ⊆ ((mrCls‘dom (𝐹 ∩ I ))‘𝑧)) → (𝐹‘𝑧) ⊆ (𝐹‘((mrCls‘dom (𝐹 ∩ I ))‘𝑧)))) |
33 | 19, 32 | syl 17 |
. . . . . 6
⊢ (𝜑 → ((((mrCls‘dom (𝐹 ∩ I ))‘𝑧) ⊆ 𝐵 ∧ 𝑧 ⊆ ((mrCls‘dom (𝐹 ∩ I ))‘𝑧)) → (𝐹‘𝑧) ⊆ (𝐹‘((mrCls‘dom (𝐹 ∩ I ))‘𝑧)))) |
34 | 33 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ 𝒫 𝐵) → ((((mrCls‘dom (𝐹 ∩ I ))‘𝑧) ⊆ 𝐵 ∧ 𝑧 ⊆ ((mrCls‘dom (𝐹 ∩ I ))‘𝑧)) → (𝐹‘𝑧) ⊆ (𝐹‘((mrCls‘dom (𝐹 ∩ I ))‘𝑧)))) |
35 | 14, 17, 34 | mp2and 715 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ 𝒫 𝐵) → (𝐹‘𝑧) ⊆ (𝐹‘((mrCls‘dom (𝐹 ∩ I ))‘𝑧))) |
36 | 9 | mrccl 16271 |
. . . . . 6
⊢ ((dom
(𝐹 ∩ I ) ∈
(Moore‘𝐵) ∧ 𝑧 ⊆ 𝐵) → ((mrCls‘dom (𝐹 ∩ I ))‘𝑧) ∈ dom (𝐹 ∩ I )) |
37 | 8, 15, 36 | syl2an 494 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ 𝒫 𝐵) → ((mrCls‘dom (𝐹 ∩ I ))‘𝑧) ∈ dom (𝐹 ∩ I )) |
38 | 3 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ 𝒫 𝐵) → 𝐹 Fn 𝒫 𝐵) |
39 | 21 | elpw 4164 |
. . . . . . . 8
⊢
(((mrCls‘dom (𝐹 ∩ I ))‘𝑧) ∈ 𝒫 𝐵 ↔ ((mrCls‘dom (𝐹 ∩ I ))‘𝑧) ⊆ 𝐵) |
40 | 13, 39 | sylibr 224 |
. . . . . . 7
⊢ (𝜑 → ((mrCls‘dom (𝐹 ∩ I ))‘𝑧) ∈ 𝒫 𝐵) |
41 | 40 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ 𝒫 𝐵) → ((mrCls‘dom (𝐹 ∩ I ))‘𝑧) ∈ 𝒫 𝐵) |
42 | | fnelfp 6441 |
. . . . . 6
⊢ ((𝐹 Fn 𝒫 𝐵 ∧ ((mrCls‘dom (𝐹 ∩ I ))‘𝑧) ∈ 𝒫 𝐵) → (((mrCls‘dom (𝐹 ∩ I ))‘𝑧) ∈ dom (𝐹 ∩ I ) ↔ (𝐹‘((mrCls‘dom (𝐹 ∩ I ))‘𝑧)) = ((mrCls‘dom (𝐹 ∩ I ))‘𝑧))) |
43 | 38, 41, 42 | syl2anc 693 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ 𝒫 𝐵) → (((mrCls‘dom (𝐹 ∩ I ))‘𝑧) ∈ dom (𝐹 ∩ I ) ↔ (𝐹‘((mrCls‘dom (𝐹 ∩ I ))‘𝑧)) = ((mrCls‘dom (𝐹 ∩ I ))‘𝑧))) |
44 | 37, 43 | mpbid 222 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ 𝒫 𝐵) → (𝐹‘((mrCls‘dom (𝐹 ∩ I ))‘𝑧)) = ((mrCls‘dom (𝐹 ∩ I ))‘𝑧)) |
45 | 35, 44 | sseqtrd 3641 |
. . 3
⊢ ((𝜑 ∧ 𝑧 ∈ 𝒫 𝐵) → (𝐹‘𝑧) ⊆ ((mrCls‘dom (𝐹 ∩ I ))‘𝑧)) |
46 | 8 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ 𝒫 𝐵) → dom (𝐹 ∩ I ) ∈ (Moore‘𝐵)) |
47 | | sseq1 3626 |
. . . . . . . 8
⊢ (𝑥 = 𝑧 → (𝑥 ⊆ 𝐵 ↔ 𝑧 ⊆ 𝐵)) |
48 | 47 | anbi2d 740 |
. . . . . . 7
⊢ (𝑥 = 𝑧 → ((𝜑 ∧ 𝑥 ⊆ 𝐵) ↔ (𝜑 ∧ 𝑧 ⊆ 𝐵))) |
49 | | id 22 |
. . . . . . . 8
⊢ (𝑥 = 𝑧 → 𝑥 = 𝑧) |
50 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑥 = 𝑧 → (𝐹‘𝑥) = (𝐹‘𝑧)) |
51 | 49, 50 | sseq12d 3634 |
. . . . . . 7
⊢ (𝑥 = 𝑧 → (𝑥 ⊆ (𝐹‘𝑥) ↔ 𝑧 ⊆ (𝐹‘𝑧))) |
52 | 48, 51 | imbi12d 334 |
. . . . . 6
⊢ (𝑥 = 𝑧 → (((𝜑 ∧ 𝑥 ⊆ 𝐵) → 𝑥 ⊆ (𝐹‘𝑥)) ↔ ((𝜑 ∧ 𝑧 ⊆ 𝐵) → 𝑧 ⊆ (𝐹‘𝑧)))) |
53 | 52, 5 | chvarv 2263 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ⊆ 𝐵) → 𝑧 ⊆ (𝐹‘𝑧)) |
54 | 15, 53 | sylan2 491 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ 𝒫 𝐵) → 𝑧 ⊆ (𝐹‘𝑧)) |
55 | 50 | fveq2d 6195 |
. . . . . . . . 9
⊢ (𝑥 = 𝑧 → (𝐹‘(𝐹‘𝑥)) = (𝐹‘(𝐹‘𝑧))) |
56 | 55, 50 | eqeq12d 2637 |
. . . . . . . 8
⊢ (𝑥 = 𝑧 → ((𝐹‘(𝐹‘𝑥)) = (𝐹‘𝑥) ↔ (𝐹‘(𝐹‘𝑧)) = (𝐹‘𝑧))) |
57 | 48, 56 | imbi12d 334 |
. . . . . . 7
⊢ (𝑥 = 𝑧 → (((𝜑 ∧ 𝑥 ⊆ 𝐵) → (𝐹‘(𝐹‘𝑥)) = (𝐹‘𝑥)) ↔ ((𝜑 ∧ 𝑧 ⊆ 𝐵) → (𝐹‘(𝐹‘𝑧)) = (𝐹‘𝑧)))) |
58 | 57, 7 | chvarv 2263 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ⊆ 𝐵) → (𝐹‘(𝐹‘𝑧)) = (𝐹‘𝑧)) |
59 | 15, 58 | sylan2 491 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ 𝒫 𝐵) → (𝐹‘(𝐹‘𝑧)) = (𝐹‘𝑧)) |
60 | 1 | ffvelrnda 6359 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ 𝒫 𝐵) → (𝐹‘𝑧) ∈ 𝒫 𝐵) |
61 | | fnelfp 6441 |
. . . . . 6
⊢ ((𝐹 Fn 𝒫 𝐵 ∧ (𝐹‘𝑧) ∈ 𝒫 𝐵) → ((𝐹‘𝑧) ∈ dom (𝐹 ∩ I ) ↔ (𝐹‘(𝐹‘𝑧)) = (𝐹‘𝑧))) |
62 | 38, 60, 61 | syl2anc 693 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ 𝒫 𝐵) → ((𝐹‘𝑧) ∈ dom (𝐹 ∩ I ) ↔ (𝐹‘(𝐹‘𝑧)) = (𝐹‘𝑧))) |
63 | 59, 62 | mpbird 247 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ 𝒫 𝐵) → (𝐹‘𝑧) ∈ dom (𝐹 ∩ I )) |
64 | 9 | mrcsscl 16280 |
. . . 4
⊢ ((dom
(𝐹 ∩ I ) ∈
(Moore‘𝐵) ∧ 𝑧 ⊆ (𝐹‘𝑧) ∧ (𝐹‘𝑧) ∈ dom (𝐹 ∩ I )) → ((mrCls‘dom (𝐹 ∩ I ))‘𝑧) ⊆ (𝐹‘𝑧)) |
65 | 46, 54, 63, 64 | syl3anc 1326 |
. . 3
⊢ ((𝜑 ∧ 𝑧 ∈ 𝒫 𝐵) → ((mrCls‘dom (𝐹 ∩ I ))‘𝑧) ⊆ (𝐹‘𝑧)) |
66 | 45, 65 | eqssd 3620 |
. 2
⊢ ((𝜑 ∧ 𝑧 ∈ 𝒫 𝐵) → (𝐹‘𝑧) = ((mrCls‘dom (𝐹 ∩ I ))‘𝑧)) |
67 | 3, 12, 66 | eqfnfvd 6314 |
1
⊢ (𝜑 → 𝐹 = (mrCls‘dom (𝐹 ∩ I ))) |