Step | Hyp | Ref
| Expression |
1 | | cantnfrescl.d |
. . . . . . . . . . . . 13
โข (๐ โ ๐ท โ On) |
2 | | cantnfrescl.b |
. . . . . . . . . . . . 13
โข (๐ โ ๐ต โ ๐ท) |
3 | | cantnfrescl.x |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ (๐ท โ ๐ต)) โ ๐ = โ
) |
4 | 1, 2, 3 | extmptsuppeq 8123 |
. . . . . . . . . . . 12
โข (๐ โ ((๐ โ ๐ต โฆ ๐) supp โ
) = ((๐ โ ๐ท โฆ ๐) supp โ
)) |
5 | | oieq2 9457 |
. . . . . . . . . . . 12
โข (((๐ โ ๐ต โฆ ๐) supp โ
) = ((๐ โ ๐ท โฆ ๐) supp โ
) โ OrdIso( E , ((๐ โ ๐ต โฆ ๐) supp โ
)) = OrdIso( E , ((๐ โ ๐ท โฆ ๐) supp โ
))) |
6 | 4, 5 | syl 17 |
. . . . . . . . . . 11
โข (๐ โ OrdIso( E , ((๐ โ ๐ต โฆ ๐) supp โ
)) = OrdIso( E , ((๐ โ ๐ท โฆ ๐) supp โ
))) |
7 | 6 | fveq1d 6848 |
. . . . . . . . . 10
โข (๐ โ (OrdIso( E , ((๐ โ ๐ต โฆ ๐) supp โ
))โ๐) = (OrdIso( E , ((๐ โ ๐ท โฆ ๐) supp โ
))โ๐)) |
8 | 7 | 3ad2ant1 1134 |
. . . . . . . . 9
โข ((๐ โง ๐ โ dom OrdIso( E , ((๐ โ ๐ต โฆ ๐) supp โ
)) โง ๐ง โ On) โ (OrdIso( E , ((๐ โ ๐ต โฆ ๐) supp โ
))โ๐) = (OrdIso( E , ((๐ โ ๐ท โฆ ๐) supp โ
))โ๐)) |
9 | 8 | oveq2d 7377 |
. . . . . . . 8
โข ((๐ โง ๐ โ dom OrdIso( E , ((๐ โ ๐ต โฆ ๐) supp โ
)) โง ๐ง โ On) โ (๐ด โo (OrdIso( E , ((๐ โ ๐ต โฆ ๐) supp โ
))โ๐)) = (๐ด โo (OrdIso( E , ((๐ โ ๐ท โฆ ๐) supp โ
))โ๐))) |
10 | | suppssdm 8112 |
. . . . . . . . . . . . 13
โข ((๐ โ ๐ต โฆ ๐) supp โ
) โ dom (๐ โ ๐ต โฆ ๐) |
11 | | eqid 2733 |
. . . . . . . . . . . . . . 15
โข (๐ โ ๐ต โฆ ๐) = (๐ โ ๐ต โฆ ๐) |
12 | 11 | dmmptss 6197 |
. . . . . . . . . . . . . 14
โข dom
(๐ โ ๐ต โฆ ๐) โ ๐ต |
13 | 12 | a1i 11 |
. . . . . . . . . . . . 13
โข (๐ โ dom (๐ โ ๐ต โฆ ๐) โ ๐ต) |
14 | 10, 13 | sstrid 3959 |
. . . . . . . . . . . 12
โข (๐ โ ((๐ โ ๐ต โฆ ๐) supp โ
) โ ๐ต) |
15 | 14 | 3ad2ant1 1134 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ dom OrdIso( E , ((๐ โ ๐ต โฆ ๐) supp โ
)) โง ๐ง โ On) โ ((๐ โ ๐ต โฆ ๐) supp โ
) โ ๐ต) |
16 | | eqid 2733 |
. . . . . . . . . . . . . 14
โข OrdIso( E
, ((๐ โ ๐ต โฆ ๐) supp โ
)) = OrdIso( E , ((๐ โ ๐ต โฆ ๐) supp โ
)) |
17 | 16 | oif 9474 |
. . . . . . . . . . . . 13
โข OrdIso( E
, ((๐ โ ๐ต โฆ ๐) supp โ
)):dom OrdIso( E , ((๐ โ ๐ต โฆ ๐) supp โ
))โถ((๐ โ ๐ต โฆ ๐) supp โ
) |
18 | 17 | ffvelcdmi 7038 |
. . . . . . . . . . . 12
โข (๐ โ dom OrdIso( E , ((๐ โ ๐ต โฆ ๐) supp โ
)) โ (OrdIso( E , ((๐ โ ๐ต โฆ ๐) supp โ
))โ๐) โ ((๐ โ ๐ต โฆ ๐) supp โ
)) |
19 | 18 | 3ad2ant2 1135 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ dom OrdIso( E , ((๐ โ ๐ต โฆ ๐) supp โ
)) โง ๐ง โ On) โ (OrdIso( E , ((๐ โ ๐ต โฆ ๐) supp โ
))โ๐) โ ((๐ โ ๐ต โฆ ๐) supp โ
)) |
20 | 15, 19 | sseldd 3949 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ dom OrdIso( E , ((๐ โ ๐ต โฆ ๐) supp โ
)) โง ๐ง โ On) โ (OrdIso( E , ((๐ โ ๐ต โฆ ๐) supp โ
))โ๐) โ ๐ต) |
21 | 20 | fvresd 6866 |
. . . . . . . . 9
โข ((๐ โง ๐ โ dom OrdIso( E , ((๐ โ ๐ต โฆ ๐) supp โ
)) โง ๐ง โ On) โ (((๐ โ ๐ท โฆ ๐) โพ ๐ต)โ(OrdIso( E , ((๐ โ ๐ต โฆ ๐) supp โ
))โ๐)) = ((๐ โ ๐ท โฆ ๐)โ(OrdIso( E , ((๐ โ ๐ต โฆ ๐) supp โ
))โ๐))) |
22 | 2 | 3ad2ant1 1134 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ dom OrdIso( E , ((๐ โ ๐ต โฆ ๐) supp โ
)) โง ๐ง โ On) โ ๐ต โ ๐ท) |
23 | 22 | resmptd 5998 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ dom OrdIso( E , ((๐ โ ๐ต โฆ ๐) supp โ
)) โง ๐ง โ On) โ ((๐ โ ๐ท โฆ ๐) โพ ๐ต) = (๐ โ ๐ต โฆ ๐)) |
24 | 23 | fveq1d 6848 |
. . . . . . . . 9
โข ((๐ โง ๐ โ dom OrdIso( E , ((๐ โ ๐ต โฆ ๐) supp โ
)) โง ๐ง โ On) โ (((๐ โ ๐ท โฆ ๐) โพ ๐ต)โ(OrdIso( E , ((๐ โ ๐ต โฆ ๐) supp โ
))โ๐)) = ((๐ โ ๐ต โฆ ๐)โ(OrdIso( E , ((๐ โ ๐ต โฆ ๐) supp โ
))โ๐))) |
25 | 8 | fveq2d 6850 |
. . . . . . . . 9
โข ((๐ โง ๐ โ dom OrdIso( E , ((๐ โ ๐ต โฆ ๐) supp โ
)) โง ๐ง โ On) โ ((๐ โ ๐ท โฆ ๐)โ(OrdIso( E , ((๐ โ ๐ต โฆ ๐) supp โ
))โ๐)) = ((๐ โ ๐ท โฆ ๐)โ(OrdIso( E , ((๐ โ ๐ท โฆ ๐) supp โ
))โ๐))) |
26 | 21, 24, 25 | 3eqtr3d 2781 |
. . . . . . . 8
โข ((๐ โง ๐ โ dom OrdIso( E , ((๐ โ ๐ต โฆ ๐) supp โ
)) โง ๐ง โ On) โ ((๐ โ ๐ต โฆ ๐)โ(OrdIso( E , ((๐ โ ๐ต โฆ ๐) supp โ
))โ๐)) = ((๐ โ ๐ท โฆ ๐)โ(OrdIso( E , ((๐ โ ๐ท โฆ ๐) supp โ
))โ๐))) |
27 | 9, 26 | oveq12d 7379 |
. . . . . . 7
โข ((๐ โง ๐ โ dom OrdIso( E , ((๐ โ ๐ต โฆ ๐) supp โ
)) โง ๐ง โ On) โ ((๐ด โo (OrdIso( E , ((๐ โ ๐ต โฆ ๐) supp โ
))โ๐)) ยทo ((๐ โ ๐ต โฆ ๐)โ(OrdIso( E , ((๐ โ ๐ต โฆ ๐) supp โ
))โ๐))) = ((๐ด โo (OrdIso( E , ((๐ โ ๐ท โฆ ๐) supp โ
))โ๐)) ยทo ((๐ โ ๐ท โฆ ๐)โ(OrdIso( E , ((๐ โ ๐ท โฆ ๐) supp โ
))โ๐)))) |
28 | 27 | oveq1d 7376 |
. . . . . 6
โข ((๐ โง ๐ โ dom OrdIso( E , ((๐ โ ๐ต โฆ ๐) supp โ
)) โง ๐ง โ On) โ (((๐ด โo (OrdIso( E , ((๐ โ ๐ต โฆ ๐) supp โ
))โ๐)) ยทo ((๐ โ ๐ต โฆ ๐)โ(OrdIso( E , ((๐ โ ๐ต โฆ ๐) supp โ
))โ๐))) +o ๐ง) = (((๐ด โo (OrdIso( E , ((๐ โ ๐ท โฆ ๐) supp โ
))โ๐)) ยทo ((๐ โ ๐ท โฆ ๐)โ(OrdIso( E , ((๐ โ ๐ท โฆ ๐) supp โ
))โ๐))) +o ๐ง)) |
29 | 28 | mpoeq3dva 7438 |
. . . . 5
โข (๐ โ (๐ โ dom OrdIso( E , ((๐ โ ๐ต โฆ ๐) supp โ
)), ๐ง โ On โฆ (((๐ด โo (OrdIso( E , ((๐ โ ๐ต โฆ ๐) supp โ
))โ๐)) ยทo ((๐ โ ๐ต โฆ ๐)โ(OrdIso( E , ((๐ โ ๐ต โฆ ๐) supp โ
))โ๐))) +o ๐ง)) = (๐ โ dom OrdIso( E , ((๐ โ ๐ต โฆ ๐) supp โ
)), ๐ง โ On โฆ (((๐ด โo (OrdIso( E , ((๐ โ ๐ท โฆ ๐) supp โ
))โ๐)) ยทo ((๐ โ ๐ท โฆ ๐)โ(OrdIso( E , ((๐ โ ๐ท โฆ ๐) supp โ
))โ๐))) +o ๐ง))) |
30 | 6 | dmeqd 5865 |
. . . . . 6
โข (๐ โ dom OrdIso( E , ((๐ โ ๐ต โฆ ๐) supp โ
)) = dom OrdIso( E , ((๐ โ ๐ท โฆ ๐) supp โ
))) |
31 | | eqid 2733 |
. . . . . 6
โข On =
On |
32 | | mpoeq12 7434 |
. . . . . 6
โข ((dom
OrdIso( E , ((๐ โ
๐ต โฆ ๐) supp โ
)) = dom OrdIso( E , ((๐ โ ๐ท โฆ ๐) supp โ
)) โง On = On) โ
(๐ โ dom OrdIso( E ,
((๐ โ ๐ต โฆ ๐) supp โ
)), ๐ง โ On โฆ (((๐ด โo (OrdIso( E , ((๐ โ ๐ท โฆ ๐) supp โ
))โ๐)) ยทo ((๐ โ ๐ท โฆ ๐)โ(OrdIso( E , ((๐ โ ๐ท โฆ ๐) supp โ
))โ๐))) +o ๐ง)) = (๐ โ dom OrdIso( E , ((๐ โ ๐ท โฆ ๐) supp โ
)), ๐ง โ On โฆ (((๐ด โo (OrdIso( E , ((๐ โ ๐ท โฆ ๐) supp โ
))โ๐)) ยทo ((๐ โ ๐ท โฆ ๐)โ(OrdIso( E , ((๐ โ ๐ท โฆ ๐) supp โ
))โ๐))) +o ๐ง))) |
33 | 30, 31, 32 | sylancl 587 |
. . . . 5
โข (๐ โ (๐ โ dom OrdIso( E , ((๐ โ ๐ต โฆ ๐) supp โ
)), ๐ง โ On โฆ (((๐ด โo (OrdIso( E , ((๐ โ ๐ท โฆ ๐) supp โ
))โ๐)) ยทo ((๐ โ ๐ท โฆ ๐)โ(OrdIso( E , ((๐ โ ๐ท โฆ ๐) supp โ
))โ๐))) +o ๐ง)) = (๐ โ dom OrdIso( E , ((๐ โ ๐ท โฆ ๐) supp โ
)), ๐ง โ On โฆ (((๐ด โo (OrdIso( E , ((๐ โ ๐ท โฆ ๐) supp โ
))โ๐)) ยทo ((๐ โ ๐ท โฆ ๐)โ(OrdIso( E , ((๐ โ ๐ท โฆ ๐) supp โ
))โ๐))) +o ๐ง))) |
34 | 29, 33 | eqtrd 2773 |
. . . 4
โข (๐ โ (๐ โ dom OrdIso( E , ((๐ โ ๐ต โฆ ๐) supp โ
)), ๐ง โ On โฆ (((๐ด โo (OrdIso( E , ((๐ โ ๐ต โฆ ๐) supp โ
))โ๐)) ยทo ((๐ โ ๐ต โฆ ๐)โ(OrdIso( E , ((๐ โ ๐ต โฆ ๐) supp โ
))โ๐))) +o ๐ง)) = (๐ โ dom OrdIso( E , ((๐ โ ๐ท โฆ ๐) supp โ
)), ๐ง โ On โฆ (((๐ด โo (OrdIso( E , ((๐ โ ๐ท โฆ ๐) supp โ
))โ๐)) ยทo ((๐ โ ๐ท โฆ ๐)โ(OrdIso( E , ((๐ โ ๐ท โฆ ๐) supp โ
))โ๐))) +o ๐ง))) |
35 | | eqid 2733 |
. . . 4
โข โ
=
โ
|
36 | | seqomeq12 8404 |
. . . 4
โข (((๐ โ dom OrdIso( E , ((๐ โ ๐ต โฆ ๐) supp โ
)), ๐ง โ On โฆ (((๐ด โo (OrdIso( E , ((๐ โ ๐ต โฆ ๐) supp โ
))โ๐)) ยทo ((๐ โ ๐ต โฆ ๐)โ(OrdIso( E , ((๐ โ ๐ต โฆ ๐) supp โ
))โ๐))) +o ๐ง)) = (๐ โ dom OrdIso( E , ((๐ โ ๐ท โฆ ๐) supp โ
)), ๐ง โ On โฆ (((๐ด โo (OrdIso( E , ((๐ โ ๐ท โฆ ๐) supp โ
))โ๐)) ยทo ((๐ โ ๐ท โฆ ๐)โ(OrdIso( E , ((๐ โ ๐ท โฆ ๐) supp โ
))โ๐))) +o ๐ง)) โง โ
= โ
) โ
seqฯ((๐
โ dom OrdIso( E , ((๐
โ ๐ต โฆ ๐) supp โ
)), ๐ง โ On โฆ (((๐ด โo (OrdIso( E ,
((๐ โ ๐ต โฆ ๐) supp โ
))โ๐)) ยทo ((๐ โ ๐ต โฆ ๐)โ(OrdIso( E , ((๐ โ ๐ต โฆ ๐) supp โ
))โ๐))) +o ๐ง)), โ
) = seqฯ((๐ โ dom OrdIso( E , ((๐ โ ๐ท โฆ ๐) supp โ
)), ๐ง โ On โฆ (((๐ด โo (OrdIso( E , ((๐ โ ๐ท โฆ ๐) supp โ
))โ๐)) ยทo ((๐ โ ๐ท โฆ ๐)โ(OrdIso( E , ((๐ โ ๐ท โฆ ๐) supp โ
))โ๐))) +o ๐ง)), โ
)) |
37 | 34, 35, 36 | sylancl 587 |
. . 3
โข (๐ โ
seqฯ((๐
โ dom OrdIso( E , ((๐
โ ๐ต โฆ ๐) supp โ
)), ๐ง โ On โฆ (((๐ด โo (OrdIso( E ,
((๐ โ ๐ต โฆ ๐) supp โ
))โ๐)) ยทo ((๐ โ ๐ต โฆ ๐)โ(OrdIso( E , ((๐ โ ๐ต โฆ ๐) supp โ
))โ๐))) +o ๐ง)), โ
) = seqฯ((๐ โ dom OrdIso( E , ((๐ โ ๐ท โฆ ๐) supp โ
)), ๐ง โ On โฆ (((๐ด โo (OrdIso( E , ((๐ โ ๐ท โฆ ๐) supp โ
))โ๐)) ยทo ((๐ โ ๐ท โฆ ๐)โ(OrdIso( E , ((๐ โ ๐ท โฆ ๐) supp โ
))โ๐))) +o ๐ง)), โ
)) |
38 | 37, 30 | fveq12d 6853 |
. 2
โข (๐ โ
(seqฯ((๐
โ dom OrdIso( E , ((๐
โ ๐ต โฆ ๐) supp โ
)), ๐ง โ On โฆ (((๐ด โo (OrdIso( E ,
((๐ โ ๐ต โฆ ๐) supp โ
))โ๐)) ยทo ((๐ โ ๐ต โฆ ๐)โ(OrdIso( E , ((๐ โ ๐ต โฆ ๐) supp โ
))โ๐))) +o ๐ง)), โ
)โdom OrdIso( E , ((๐ โ ๐ต โฆ ๐) supp โ
))) =
(seqฯ((๐
โ dom OrdIso( E , ((๐
โ ๐ท โฆ ๐) supp โ
)), ๐ง โ On โฆ (((๐ด โo (OrdIso( E ,
((๐ โ ๐ท โฆ ๐) supp โ
))โ๐)) ยทo ((๐ โ ๐ท โฆ ๐)โ(OrdIso( E , ((๐ โ ๐ท โฆ ๐) supp โ
))โ๐))) +o ๐ง)), โ
)โdom OrdIso( E , ((๐ โ ๐ท โฆ ๐) supp โ
)))) |
39 | | cantnfs.s |
. . 3
โข ๐ = dom (๐ด CNF ๐ต) |
40 | | cantnfs.a |
. . 3
โข (๐ โ ๐ด โ On) |
41 | | cantnfs.b |
. . 3
โข (๐ โ ๐ต โ On) |
42 | | cantnfres.m |
. . 3
โข (๐ โ (๐ โ ๐ต โฆ ๐) โ ๐) |
43 | | 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 ๐ง)), โ
) |
44 | 39, 40, 41, 16, 42, 43 | cantnfval2 9613 |
. 2
โข (๐ โ ((๐ด CNF ๐ต)โ(๐ โ ๐ต โฆ ๐)) = (seqฯ((๐ โ dom OrdIso( E , ((๐ โ ๐ต โฆ ๐) supp โ
)), ๐ง โ On โฆ (((๐ด โo (OrdIso( E , ((๐ โ ๐ต โฆ ๐) supp โ
))โ๐)) ยทo ((๐ โ ๐ต โฆ ๐)โ(OrdIso( E , ((๐ โ ๐ต โฆ ๐) supp โ
))โ๐))) +o ๐ง)), โ
)โdom OrdIso( E , ((๐ โ ๐ต โฆ ๐) supp โ
)))) |
45 | | cantnfrescl.t |
. . 3
โข ๐ = dom (๐ด CNF ๐ท) |
46 | | eqid 2733 |
. . 3
โข OrdIso( E
, ((๐ โ ๐ท โฆ ๐) supp โ
)) = OrdIso( E , ((๐ โ ๐ท โฆ ๐) supp โ
)) |
47 | | cantnfrescl.a |
. . . . 5
โข (๐ โ โ
โ ๐ด) |
48 | 39, 40, 41, 1, 2, 3,
47, 45 | cantnfrescl 9620 |
. . . 4
โข (๐ โ ((๐ โ ๐ต โฆ ๐) โ ๐ โ (๐ โ ๐ท โฆ ๐) โ ๐)) |
49 | 42, 48 | mpbid 231 |
. . 3
โข (๐ โ (๐ โ ๐ท โฆ ๐) โ ๐) |
50 | | 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 ๐ง)), โ
) |
51 | 45, 40, 1, 46, 49, 50 | cantnfval2 9613 |
. 2
โข (๐ โ ((๐ด CNF ๐ท)โ(๐ โ ๐ท โฆ ๐)) = (seqฯ((๐ โ dom OrdIso( E , ((๐ โ ๐ท โฆ ๐) supp โ
)), ๐ง โ On โฆ (((๐ด โo (OrdIso( E , ((๐ โ ๐ท โฆ ๐) supp โ
))โ๐)) ยทo ((๐ โ ๐ท โฆ ๐)โ(OrdIso( E , ((๐ โ ๐ท โฆ ๐) supp โ
))โ๐))) +o ๐ง)), โ
)โdom OrdIso( E , ((๐ โ ๐ท โฆ ๐) supp โ
)))) |
52 | 38, 44, 51 | 3eqtr4d 2783 |
1
โข (๐ โ ((๐ด CNF ๐ต)โ(๐ โ ๐ต โฆ ๐)) = ((๐ด CNF ๐ท)โ(๐ โ ๐ท โฆ ๐))) |