Step | Hyp | Ref
| Expression |
1 | | cantnfs.s |
. . 3
โข ๐ = dom (๐ด CNF ๐ต) |
2 | | cantnfs.a |
. . 3
โข (๐ โ ๐ด โ On) |
3 | | cantnfs.b |
. . 3
โข (๐ โ ๐ต โ On) |
4 | | eqid 2733 |
. . 3
โข OrdIso( E
, ((๐ต ร {โ
})
supp โ
)) = OrdIso( E , ((๐ต ร {โ
}) supp
โ
)) |
5 | | cantnf0.a |
. . . . 5
โข (๐ โ โ
โ ๐ด) |
6 | | fconst6g 6735 |
. . . . 5
โข (โ
โ ๐ด โ (๐ต ร {โ
}):๐ตโถ๐ด) |
7 | 5, 6 | syl 17 |
. . . 4
โข (๐ โ (๐ต ร {โ
}):๐ตโถ๐ด) |
8 | 3, 5 | fczfsuppd 9331 |
. . . 4
โข (๐ โ (๐ต ร {โ
}) finSupp
โ
) |
9 | 1, 2, 3 | cantnfs 9610 |
. . . 4
โข (๐ โ ((๐ต ร {โ
}) โ ๐ โ ((๐ต ร {โ
}):๐ตโถ๐ด โง (๐ต ร {โ
}) finSupp
โ
))) |
10 | 7, 8, 9 | mpbir2and 712 |
. . 3
โข (๐ โ (๐ต ร {โ
}) โ ๐) |
11 | | eqid 2733 |
. . 3
โข
seqฯ((๐ โ V, ๐ง โ V โฆ (((๐ด โo (OrdIso( E , ((๐ต ร {โ
}) supp
โ
))โ๐))
ยทo ((๐ต
ร {โ
})โ(OrdIso( E , ((๐ต ร {โ
}) supp
โ
))โ๐)))
+o ๐ง)), โ
)
= seqฯ((๐
โ V, ๐ง โ V
โฆ (((๐ด
โo (OrdIso( E , ((๐ต ร {โ
}) supp
โ
))โ๐))
ยทo ((๐ต
ร {โ
})โ(OrdIso( E , ((๐ต ร {โ
}) supp
โ
))โ๐)))
+o ๐ง)),
โ
) |
12 | 1, 2, 3, 4, 10, 11 | cantnfval 9612 |
. 2
โข (๐ โ ((๐ด CNF ๐ต)โ(๐ต ร {โ
})) =
(seqฯ((๐
โ V, ๐ง โ V
โฆ (((๐ด
โo (OrdIso( E , ((๐ต ร {โ
}) supp
โ
))โ๐))
ยทo ((๐ต
ร {โ
})โ(OrdIso( E , ((๐ต ร {โ
}) supp
โ
))โ๐)))
+o ๐ง)),
โ
)โdom OrdIso( E , ((๐ต ร {โ
}) supp
โ
)))) |
13 | | eqidd 2734 |
. . . . . . 7
โข (๐ โ (๐ต ร {โ
}) = (๐ต ร {โ
})) |
14 | | 0ex 5268 |
. . . . . . . . 9
โข โ
โ V |
15 | | fnconstg 6734 |
. . . . . . . . 9
โข (โ
โ V โ (๐ต ร
{โ
}) Fn ๐ต) |
16 | 14, 15 | mp1i 13 |
. . . . . . . 8
โข (๐ โ (๐ต ร {โ
}) Fn ๐ต) |
17 | 14 | a1i 11 |
. . . . . . . 8
โข (๐ โ โ
โ
V) |
18 | | fnsuppeq0 8127 |
. . . . . . . 8
โข (((๐ต ร {โ
}) Fn ๐ต โง ๐ต โ On โง โ
โ V) โ
(((๐ต ร {โ
})
supp โ
) = โ
โ (๐ต ร {โ
}) = (๐ต ร {โ
}))) |
19 | 16, 3, 17, 18 | syl3anc 1372 |
. . . . . . 7
โข (๐ โ (((๐ต ร {โ
}) supp โ
) = โ
โ (๐ต ร
{โ
}) = (๐ต ร
{โ
}))) |
20 | 13, 19 | mpbird 257 |
. . . . . 6
โข (๐ โ ((๐ต ร {โ
}) supp โ
) =
โ
) |
21 | | oieq2 9457 |
. . . . . 6
โข (((๐ต ร {โ
}) supp
โ
) = โ
โ OrdIso( E , ((๐ต ร {โ
}) supp โ
)) = OrdIso(
E , โ
)) |
22 | 20, 21 | syl 17 |
. . . . 5
โข (๐ โ OrdIso( E , ((๐ต ร {โ
}) supp
โ
)) = OrdIso( E , โ
)) |
23 | 22 | dmeqd 5865 |
. . . 4
โข (๐ โ dom OrdIso( E , ((๐ต ร {โ
}) supp
โ
)) = dom OrdIso( E , โ
)) |
24 | | we0 5632 |
. . . . . 6
โข E We
โ
|
25 | | eqid 2733 |
. . . . . . 7
โข OrdIso( E
, โ
) = OrdIso( E , โ
) |
26 | 25 | oien 9482 |
. . . . . 6
โข ((โ
โ V โง E We โ
) โ dom OrdIso( E , โ
) โ
โ
) |
27 | 14, 24, 26 | mp2an 691 |
. . . . 5
โข dom
OrdIso( E , โ
) โ โ
|
28 | | en0 8963 |
. . . . 5
โข (dom
OrdIso( E , โ
) โ โ
โ dom OrdIso( E , โ
) =
โ
) |
29 | 27, 28 | mpbi 229 |
. . . 4
โข dom
OrdIso( E , โ
) = โ
|
30 | 23, 29 | eqtrdi 2789 |
. . 3
โข (๐ โ dom OrdIso( E , ((๐ต ร {โ
}) supp
โ
)) = โ
) |
31 | 30 | fveq2d 6850 |
. 2
โข (๐ โ
(seqฯ((๐
โ V, ๐ง โ V
โฆ (((๐ด
โo (OrdIso( E , ((๐ต ร {โ
}) supp
โ
))โ๐))
ยทo ((๐ต
ร {โ
})โ(OrdIso( E , ((๐ต ร {โ
}) supp
โ
))โ๐)))
+o ๐ง)),
โ
)โdom OrdIso( E , ((๐ต ร {โ
}) supp โ
))) =
(seqฯ((๐
โ V, ๐ง โ V
โฆ (((๐ด
โo (OrdIso( E , ((๐ต ร {โ
}) supp
โ
))โ๐))
ยทo ((๐ต
ร {โ
})โ(OrdIso( E , ((๐ต ร {โ
}) supp
โ
))โ๐)))
+o ๐ง)),
โ
)โโ
)) |
32 | 11 | seqom0g 8406 |
. . 3
โข (โ
โ V โ (seqฯ((๐ โ V, ๐ง โ V โฆ (((๐ด โo (OrdIso( E , ((๐ต ร {โ
}) supp
โ
))โ๐))
ยทo ((๐ต
ร {โ
})โ(OrdIso( E , ((๐ต ร {โ
}) supp
โ
))โ๐)))
+o ๐ง)),
โ
)โโ
) = โ
) |
33 | 14, 32 | mp1i 13 |
. 2
โข (๐ โ
(seqฯ((๐
โ V, ๐ง โ V
โฆ (((๐ด
โo (OrdIso( E , ((๐ต ร {โ
}) supp
โ
))โ๐))
ยทo ((๐ต
ร {โ
})โ(OrdIso( E , ((๐ต ร {โ
}) supp
โ
))โ๐)))
+o ๐ง)),
โ
)โโ
) = โ
) |
34 | 12, 31, 33 | 3eqtrd 2777 |
1
โข (๐ โ ((๐ด CNF ๐ต)โ(๐ต ร {โ
})) =
โ
) |